PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_composite_defect_character
plain-language theorem explainer
The orbit-2 reciprocal mixed-witness exclusion target is equivalent to nonexistence of a prime-calibrated composite-defect character with forced image χ(2·p)=p/2. Native-cost uniqueness and character-rigidity arguments cite this bridge. The proof is a short biconditional that routes both directions through the already-proved mixed-character equivalence and the two conversion lemmas between mixed and composite-defect models.
Claim. The following are equivalent: (i) every prime-direction-calibrated ratio character $\chi$ that is reciprocal on the orbit-$2$ prime axis admits no identity-oriented native prime witness; (ii) there is no prime-calibrated ratio character realizing the composite defect $\chi(2\cdot p)=p/2$ for some odd prime $p$.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits compatible with the multiplicative structure used to build the native cost. Prime-direction calibration fixes how $\chi$ orients prime axes (identity versus reciprocal). The exclusion target asserts: if the orbit-$2$ axis is reciprocal-oriented, then no identity-oriented native prime witness may exist on any other prime.
The composite-defect model is an exact calibrated counter-model: a prime-calibrated character that is reciprocal on $2$, identity on some odd prime $p$, and forces the composite image $\chi(2\cdot p)=p/2$. Its doc-comment records that this model is equivalent to the non-two mixed-prime blocker, with the composite image exposed. Constructing such a $\chi$ would refute the character-rigidity route to native-cost uniqueness.
Upstream, the same exclusion target is already known equivalent to nonexistence of the non-two mixed character, and two conversion theorems identify the mixed model with the composite-defect model in both directions.
proof idea
Term-mode constructor on the biconditional.
Forward: from the exclusion hypothesis and a composite-defect witness, apply PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_composite_defect to obtain a non-two mixed character, then feed that into the mixed-side equivalence ..._iff_no_non_two_mixed_character.mp to derive a contradiction.
Reverse: from nonexistence of composite defect, reduce via ..._iff_no_non_two_mixed_character.mpr. The inner goal (no mixed character) is discharged by converting any mixed witness back to a composite-defect witness with PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter_of_non_two_mixed and applying the outer negation.
No new arithmetic: pure Prop-level transport along the two model-conversion lemmas and the prior mixed equivalence.
why it matters
This lemma rephrases the orbit-2 mixed-witness exclusion target as nonexistence of the composite-defect character, the form needed when the rigidity argument tracks forced composite images rather than mixed prime orientations alone.
Downstream it is composed into PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_iff_no_non_two_composite_defect_character (via a short trans), and into the cost-visible variant ..._iff_no_composite_cost_defect_character. It also appears among the ingredients of prc_universal_foundation_conditional_certificate in UniversalFoundation.
In the Recognition forcing chain this sits inside native J-cost uniqueness for the PRC kernel (the T5 J-uniqueness / RCL layer): ruling out composite-defect characters is part of forcing the unique cost functional before phi, the eight-tick octave, and D=3 are installed. The open residual is whether any such calibrated composite-defect $\chi$ can still be built; this theorem only equates that residual to the exclusion target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.