PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter_of_non_two_mixed
plain-language theorem explainer
A prime-calibrated ratio-orbit character with reciprocal action on the 2-orbit and identity orientation on some non-2 native prime yields the exact calibrated mixed-character model (2 reciprocal, some prime identity). Cited when collapsing the sharpened non-2 mixed witness into the orbit-2 mixed-witness exclusion target. Proof unpacks the existential witness and applies the pointwise character implication that drops the non-2 constraint.
Claim. If there exists a prime-direction-calibrated ratio-orbit character $\chi$ such that the orbit of $2$ is reciprocal under $\chi$ and some native prime $p\neq 2$ is identity-oriented under $\chi$, then there exists a prime-direction-calibrated ratio-orbit character with reciprocal $2$-orbit and at least one prime identity-oriented (the exact calibrated mixed-character model).
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio-orbit characters $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ encode how multiplicative orbits act under the recognition cost. Prime-direction calibration fixes the character's orientation on native prime orbits. Two mixed-character models are compared here.
The sharpened model asserts: orbit $2$ is reciprocal, while some non-$2$ native prime is identity-oriented. The exact calibrated mixed-character model asserts the same reciprocal $2$-orbit together with identity orientation on some (unrestricted) prime. Its nonexistence is equivalent to the orbit-$2$ mixed-witness exclusion target; constructing either model would refute the current character-rigidity route.
Upstream, the pointwise lemma already shows that any character satisfying the non-$2$ mixed condition satisfies the (weaker) prime-mixed condition, by discarding the $p\neq 2$ conjunct.
proof idea
Term-mode existential transport. Destruct hmix to obtain a witness character $\chi$ together with the ratio-character, prime-calibration, and non-$2$ mixed hypotheses. Reassemble the exact mixed-character package with the same $\chi$, same calibration data, and the mixed conjunct replaced by PRCCharacterTwoPrimeReciprocalIdentityPrimeMixed_of_non_two_mixed applied to the non-$2$ mixed hypothesis. That upstream lemma simply drops the $p\neq 2$ field from the mixed witness tuple.
why it matters
One direction of the equivalence between the exact calibrated mixed-character model and its sharpened non-$2$ form (...PrimeMixedCharacter_iff_non_two). That equivalence lets the exclusion target PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget be rewritten as nonexistence of the non-$2$ mixed character, tightening the character-rigidity branch of native-cost uniqueness.
Downstream the same package feeds prc_universal_foundation_conditional_certificate in UniversalFoundation, so the mixed-character collapse sits on the conditional certificate path for the PRC universal foundation. Within the Recognition forcing chain this is local scaffolding around native J-cost uniqueness (T5 landmark), not a direct T0–T8 step; it polices which ratio characters can coexist with prime calibration before the cost is forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.