PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_of_no_mixed_character
plain-language theorem explainer
Assuming no prime-calibrated ratio character mixes a reciprocal orbit-2 axis with an identity-oriented native prime witness, every prime-calibrated ratio character with reciprocal orbit 2 excludes identity-oriented prime witnesses. Character-rigidity and native-cost uniqueness arguments cite this bridge. The proof unpacks the universal target and applies the pointwise non-mixed exclusion lemma by packaging any mixed witness into the forbidden existential model.
Claim. If there is no ratio character $\chi$ that is prime-direction calibrated and simultaneously reciprocal on the orbit-$2$ prime axis while identity-oriented on some native prime witness, then for every prime-direction calibrated ratio character, reciprocal orientation of orbit $2$ excludes any identity-oriented native prime witness.
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio characters are maps on ratio orbits that encode orientation data used to build native cost functionals. Prime-direction calibration fixes how prime axes are oriented relative to the reciprocal/identity dichotomy.
The target proposition asserts a two-specific mixed-witness exclusion: whenever the orbit-$2$ prime axis is reciprocal-oriented, no identity-oriented native prime witness is allowed. The mixed-character model is the existential dual: some calibrated ratio character that is reciprocal at orbit $2$ and identity-oriented at a native prime. Its doc-comment states that constructing such a model "would refute the current character-rigidity route."
Upstream, the pointwise lemma already shows that for a fixed character, denying the mixed pair (reciprocal orbit $2$ together with an identity prime witness) yields the exclusion property for that character. This declaration lifts that pointwise fact to the calibrated universal target under global nonexistence of any mixed model.
proof idea
Short tactic proof. Introduce an arbitrary ratio character $\chi$ with the ratio-character and prime-calibration hypotheses required by the target. Apply the pointwise theorem that non-mixedness implies exclusion for $\chi$. Discharge the non-mixed hypothesis by contradiction: any mixed pair on $\chi$ would package with the standing hypotheses into an inhabitant of the calibrated mixed-character existential, contradicting the global assumption.
why it matters
This is one direction of the equivalence between the orbit-$2$ mixed-witness exclusion target and nonexistence of the calibrated mixed-character model; the sibling iff theorem cites it directly as the right-to-left arrow. A parallel iff with the non-$2$ mixed model also depends on it.
Downstream it feeds the native-cost uniqueness blocker certificate and, through the Universal Foundation layer, the conditional universal-foundation certificate. In the Recognition Science forcing picture this is local character-rigidity scaffolding toward unique native cost (the J-cost route of T5), not yet a closed uniqueness theorem: the mixed model remains the explicit obstruction whose absence this implication converts into the exclusion target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.