PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_non_two_mixed_character
plain-language theorem explainer
The orbit-2 reciprocal exclusion target (no identity-oriented native prime witness when the 2-axis is reciprocal) is equivalent to nonexistence of a calibrated mixed character with reciprocal 2 and identity orientation on some other prime. Researchers tracking character rigidity for native cost uniqueness cite this bridge. The proof is a short bidirectional reduction through intermediate mixed-character absurdity lemmas.
Claim. The two-specific mixed-witness exclusion target holds if and only if there is no calibrated ratio character in which orbit $2$ is reciprocal-oriented while some non-$2$ native prime witness is identity-oriented. Equivalently: whenever every prime-direction-calibrated ratio character with reciprocal orbit-$2$ axis excludes identity-oriented native prime witnesses, that property is equivalent to the nonexistence of a sharpened mixed model with reciprocal $2$ and a non-$2$ identity prime.
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio characters are maps $\chi$ on ratio orbits that encode orientation data used to build a native cost. Prime-direction calibration restricts how $\chi$ may act on prime axes. The two-specific exclusion target asserts: if the orbit-$2$ prime axis is reciprocal-oriented, then no identity-oriented native prime witness is allowed.
The sharpened mixed-character model is the concrete obstruction: a calibrated $\chi$ with reciprocal orbit $2$ and at least one non-$2$ native prime that is identity-oriented. Doc-comment on that model: "Constructing this model would refute the current character-rigidity route." A coarser mixed model (any identity prime, not necessarily non-$2$) sits between the two sides and is used as an intermediate.
Local setting is the PRC native-cost uniqueness module, which ties character rigidity on prime axes to uniqueness of the native cost (the J-cost side of the forcing chain).
proof idea
Term-mode constructor on the biconditional.
Forward: from the exclusion target and a non-$2$ mixed model, promote the non-$2$ mixed model to the coarser prime-mixed model via ...PrimeMixedCharacter_of_non_two_mixed, then apply ...PrimeMixedCharacter_absurd_of_witness_excludes to obtain a contradiction.
Backward: from nonexistence of the non-$2$ mixed model, first deduce nonexistence of the coarser prime-mixed model by contraposing ...NonTwoPrimeMixedCharacter_of_mixed. Feed that into ...ExcludesPrimeIdentityWitnessTarget_of_no_mixed_character, which rebuilds the universal exclusion target characterwise.
why it matters
This iff is a rigidity hinge in the native-cost uniqueness stack: it converts a universal exclusion statement about calibrated characters into a single nonexistence claim about a sharpened mixed model (reciprocal $2$, identity on a non-$2$ prime). Downstream, it is composed into further equivalences: prime-identity forces two-prime-identity iff no non-$2$ mixed character; two-prime mixed composite cost-consistency iff the same nonexistence; and a parallel bridge to no composite-defect character.
It is also consumed by prc_universal_foundation_conditional_certificate in UniversalFoundation, so the character-rigidity branch feeds the conditional universal-foundation certificate. In framework terms this supports the J-uniqueness route (T5): native cost must match the unique J satisfying the Recognition Composition Law, and mixed prime orientations are the residual obstruction class being ruled out.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.