P02 preregistration: cross-context factorial masking and repair replication

[fraware]

Status at preregistration

This protocol is frozen while GitHub Actions smoke run 33115975625 is still in progress and before any smoke case outcome has been inspected or used to modify the scientific design.

• Evidence branch at smoke start: science/p02-mathai-cross-context-20260827
• Smoke-run head SHA: 736ce4c4faf9cf5ad89148047af755fc2fa62f53
• Pinned MathEvidence project SHA: 946d2f7b14840837a5b641150c9df9008c4be9eb
• Lean toolchain: leanprover/lean4:v4.14.0
• Frozen hardened classifier blob: 75d0599c277806007b1f31db451dbbe1bec3962e
• Smoke generator blob: 08d63c123f0a209e1dce6517ab76699904055cac

The smoke campaign is a feasibility gate only. Its raw bundle is not publication-claim eligible and contains no compound states or repairs.

Frozen contexts

All three contexts are retained regardless of favorable or unfavorable outcomes:

1. CX1_RATIONAL_EQUALITY_CONTRACT — MathEvidence.Assurance.RationalEquality
2. CX2_CALCULUS_REFERENCE_EQUALITY — MathEvidence.Assurance.Calculus
3. CX3_LINEAR_ALGEBRA_INVERSE — MathEvidence.Assurance.LinearAlgebra

No context may be removed because of a smoke or full-campaign result.

Frozen perturbation families

The cross-context extension transfers exactly the four native-active perturbations from P02 native-v2:

1. SOURCE_CORRUPTION
2. INVALID_PROOF
3. PROHIBITED_PLACEHOLDER
4. WRONG_TARGET

No perturbation family may be added, removed, renamed, or redefined based on observed outcomes.

Strict singleton-transfer hypothesis

The preregistered strict transfer prediction is:

• clean -> TOOLCHAIN_ACCEPT_TARGET_MATCH
• SOURCE_CORRUPTION -> FRONTEND_REJECT
• INVALID_PROOF -> ENVIRONMENT_OR_ELAB_REJECT
• PROHIBITED_PLACEHOLDER -> TOOLCHAIN_ACCEPT_POLICY_REJECT
• WRONG_TARGET -> TOOLCHAIN_ACCEPT_TARGET_MISMATCH

This prediction is evaluated separately in each context. A mismatch is retained as a mismatch; the classifier, context, perturbation, or expected ordering is not modified to recover agreement.

Feasibility decision rule fixed before smoke outcomes

The full factorial campaign is permitted only if, for all three contexts:

1. the clean control is TOOLCHAIN_ACCEPT_TARGET_MATCH;
2. all four singleton perturbations receive a class in the already-frozen ordered pipeline
   FRONTEND_REJECT < ENVIRONMENT_OR_ELAB_REJECT < TOOLCHAIN_ACCEPT_POLICY_REJECT < TOOLCHAIN_ACCEPT_TARGET_MISMATCH < TOOLCHAIN_ACCEPT_TARGET_MATCH;
3. there is no timeout, spawn failure, environment mismatch, or UNKNOWN / SOURCE_EMPTY singleton classification.

Exact singleton-class disagreement with the strict transfer prediction does not permit dropping or modifying a context. If all observations remain within the ordered pipeline, the full campaign may still execute, but the strict transferred-signature hypothesis is recorded as falsified for that context. Any subsequent composition analysis must then be described as context-conditioned and derived from the frozen singleton signatures, not as confirmation of the original signature transfer.

If any context fails the feasibility conditions above, the aggregate full campaign remains blocked. The failed smoke observation is retained and reported; no classifier hardening based on these smoke outcomes is allowed before that result is recorded.

Full factorial state campaign

For each of the three contexts, execute every subset of the four perturbations exactly once under the same pinned native observation pipeline:

• 2^4 = 16 states per context;
• 48 states total.

Raw execution records candidate, declaration-probe, and target-probe observations using the existing native-v2 collection path. Construction metadata remains physically separate from raw observations. No class is assigned during raw execution.

Derived classification uses only the frozen hardened classifier named above. Construction labels are not a diagnostic oracle.

Composition prediction

For strict transfer, the predicted visible class of a nonempty perturbation subset is the earliest class under the frozen pipeline ordering among its transferred singleton signatures; the empty subset predicts TOOLCHAIN_ACCEPT_TARGET_MATCH.

A secondary context-conditioned composition analysis is permitted only under the feasibility rule above and derives each perturbation signature from that context's frozen singleton observation. This secondary analysis must be clearly separated from the strict transfer test.

Counterfactual repair campaign

For every nonempty factorial state, execute one counterfactual repair for each perturbation present in that state, removing exactly that perturbation while preserving all others.

For four perturbations this gives

• 4 * 2^(4-1) = 32 one-perturbation repair edges per context;
• 96 one-perturbation repair edges total.

Each repair implementation must be local to the declared perturbation site, and the resulting source must be asserted byte-for-byte equal to the independently rendered source for the remaining perturbation subset. Pairwise repair commutativity must be checked before execution.

For each edge, compare the reverified observation with both (i) the source state's observation and (ii) the independently executed factorial state having the same remaining perturbation set. Raw repair observations are classified only downstream with the same frozen classifier.

Primary repair categories are determined only after classification from the frozen singleton signatures:

• visible-blocker repair;
• co-visible-blocker repair, if tied signatures occur;
• masked-later repair.

The key test is whether repair/recheck transitions match the preregistered ordered composition model. A repaired latent defect may be scientifically genuine even when the visible class is unchanged; such a transition is recorded as observationally silent, not as a failed source repair.

Cumulative repair trajectories

Start from the all-four-perturbation state in each context and repair in this fixed transferred order:

1. SOURCE_CORRUPTION
2. INVALID_PROOF
3. PROHIBITED_PLACEHOLDER
4. WRONG_TARGET

Reverify after every step. This produces four cumulative transition steps per context, 12 total. The order will not be changed based on singleton, factorial, or repair outcomes.

Analysis separation and fail-closed rules

1. Raw observations are immutable and stored separately from construction/repair metadata.
2. Classification is a downstream derived artifact using the frozen classifier; raw bundles are never rewritten by classification.
3. Construction metadata is joined only after classification.
4. UNKNOWN remains a first-class conservative outcome. It is never coerced into a neighboring class to improve agreement.
5. Exact counts, mismatches, and denominators are reported; no failed context or edge is omitted.
6. Strict transferred-signature results and any context-conditioned secondary analysis are reported separately.
7. No cross-context publication claim is made from the smoke gate alone.
8. The historical native-v2 corpus and this cross-context campaign are separate evidence sets and are not pooled as if independently sampled natural data.

Intended scientific question

The extension tests whether the P02 first-failure masking / repair-recheck phenomenon survives changes in theorem shape and imported mathematical context under native Lean verification, and whether a single verifier observation remains a lossy representation of the latent defect set available to a verifier-guided mathematical repair agent.