PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter_iff_non_two
plain-language theorem explainer
Equivalence of two calibrated mixed-character models on ratio orbits: the exact mixed-prime form versus the sharpened form with orbit 2 reciprocal and a non-2 native prime identity-oriented. Character-rigidity and native-cost uniqueness arguments cite it to swap formulations. Proof is the pair of one-way implication theorems packaged as a biconditional.
Claim. There exists a prime-direction-calibrated ratio character $\chi$ with a mixed two-prime reciprocal/identity signature if and only if there exists such a $\chi$ in which the orbit of $2$ is reciprocal and some non-$2$ native prime witness is identity-oriented.
background
In the Primitive Recognition Calculus, ratio characters are maps $\chi$ on ratio orbits that encode how multiplicative structure is read by the native cost. Prime-direction calibration fixes the character's action along prime axes so that cost uniqueness arguments can compare candidate costs against the J-cost forced by the Recognition Composition Law.
The two propositions equated here are existential models of a "mixed" character: one side is the exact calibrated mixed-character model whose nonexistence is the orbit-2 mixed-witness exclusion target; the other sharpens the mix so that orbit 2 is reciprocal while a non-2 native prime is identity-oriented. Constructing either model would refute the current character-rigidity route to native cost uniqueness.
The local module develops uniqueness of the native cost from character and doubled-trace hypotheses; these mixed-character props are the obstruction objects that rigidity aims to rule out.
proof idea
Term-mode biconditional: the forward direction is the existing implication from the exact mixed model to the sharpened non-2 mixed model; the reverse is the implication from the sharpened model back to the exact mixed model. No new algebra is performed; the proof is exactly the pair of those one-way theorems as the two halves of $\leftrightarrow$.
why it matters
Native cost uniqueness in PRC depends on excluding mixed characters that would break rigidity of the cost-from-character reconstruction. This iff lets later certificates treat the exact mixed model and the sharpened "orbit 2 reciprocal, non-2 identity" model as interchangeable obstruction statements.
It is consumed by prc_universal_foundation_conditional_certificate in UniversalFoundation, which assembles kernel, real-complete ordered field, and trace-logic certificates into the conditional universal foundation package. In the broader RS chain this sits under the J-uniqueness / native-cost branch (T5 and the RCL), where character rigidity is the route that pins the cost to $J(x)=(x+x^{-1})/2-1$.
The open pressure point remains: nonexistence of these models is the exclusion target; the iff only identifies the two formulations, it does not discharge them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.