PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_iff_no_non_two_mixed_character
plain-language theorem explainer
Prime calibration forces cost-consistency on every mixed composite direction 2·p if and only if no calibrated ratio character can send the 2-orbit reciprocal while keeping a distinct native prime identity-oriented. Cost-uniqueness and rigidity arguments cite this bridge to swap between the universal blocker and the non-existence of mixed characters. The proof is a two-step Iff chain through the reciprocal-exclusion intermediate.
Claim. The following are equivalent: (i) every prime-direction-calibrated ratio character $\chi$ that sends the $2$-orbit to its reciprocal also satisfies $\chi(2\cdot p)\sim\mathrm{recip}(2\cdot p)$ for every native prime $p\neq 2$; (ii) there is no prime-calibrated ratio character that is reciprocal on the $2$-orbit and identity-oriented on some native prime $p\neq 2$.
background
In the Primitive Recognition Calculus, ratio characters $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ record orientation data on multiplicative orbits. Prime-direction calibration requires that each native prime orbit is sent either to itself or to its reciprocal in a controlled way. The mixed model of interest orients the $2$-orbit reciprocally while leaving some other native prime $p$ identity-oriented.
The left-hand target is the cost-visible blocker: under that mixed orientation, prime calibration must still force consistency on the composite direction $2\cdot p$ (cross-equality with the reciprocal). The right-hand side is simply the non-existence of any such calibrated mixed character.
Two prior equivalences already relate both sides to a common intermediate: the target that two-prime reciprocal data excludes any prime-identity witness. Those lemmas supply the links used here.
proof idea
Term-mode composition of two existing Iff theorems. First apply the symmetric form of the equivalence between the reciprocal-exclusion target and the mixed-composite cost-consistency target. Then transitively compose with the equivalence between that same reciprocal-exclusion target and the non-existence of a non-two mixed character. No new case analysis is introduced.
why it matters
This bridge lets later arguments choose whichever face of the blocker is convenient: either assert the universal mixed-composite cost-consistency target, or deny existence of a calibrated two-reciprocal / non-two-identity character. Downstream, it feeds the absurdity of the two-adic axis-twist character under mixed-composite consistency, the dual not-Iff form, and the conditional universal-foundation certificate in UniversalFoundation.
In the Recognition forcing picture this sits inside native cost uniqueness for the J-cost (T5), ruling out orientation pathologies before the self-similar fixed point $\varphi$ and the eight-tick structure are forced. It closes a bookkeeping gap rather than a physical open question: once mixed characters are excluded, cost rigidity proceeds on a single calibrated branch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.