PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_not_iff_non_two_mixed_character
plain-language theorem explainer
Negation of the two-prime mixed composite cost-consistency target is equivalent to existence of a prime-calibrated ratio character that orients orbit 2 reciprocally while keeping some other native prime identity-oriented. Researchers tracking the character-rigidity branch of native cost uniqueness cite this dual packaging. The proof is a short classical flip of the already-proved positive equivalence.
Claim. The universal cost-consistency target fails if and only if a mixed calibrated character exists: that is, $\neg$(every prime-calibrated ratio character $\chi$ with $\chi(2)$ reciprocal forces composite $2\cdot p$ calibration for every distinct native prime $p$) is equivalent to $\exists\,\chi$ prime-calibrated with orbit $2$ reciprocal and some non-$2$ native prime identity-oriented.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ act on ratio orbits and encode orientation data (identity versus reciprocal) along prime directions. Prime-direction calibration requires that each native prime orbit is sent to a calibrated axis. The two-orbit is special: mixed models can twist it to reciprocal while leaving a distinct prime $p$ identity-oriented.
The cost-consistency target asserts that, even under that mixed orientation, prime calibration still forces the composite direction $2\cdot p$ to match the expected cross-equality. Its failure is therefore exactly the existence of a sharpened mixed character (orbit $2$ reciprocal, some non-$2$ prime identity). The sibling theorem already records the positive packaging: target holds iff no such mixed character exists.
This module sits inside native cost uniqueness for PRC, where character rigidity is the route that would force the unique J-cost shape from calibration hypotheses alone.
proof idea
Pure logical dual of the sibling biconditional. constructor splits the desired $\neg\mathrm{Target}\leftrightarrow\mathrm{Mixed}$.
Left-to-right: assume $\neg\mathrm{Target}$; by_contra the non-existence of a mixed character; feed that into the sibling's mpr arm to obtain $\mathrm{Target}$, contradicting the assumption.
Right-to-left: assume a mixed character and the target; the sibling's mp arm turns the target into $\neg\mathrm{Mixed}$, which immediately kills the assumed witness.
No new analytic content: only classical rearrangement of
PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_iff_no_non_two_mixed_character.
why it matters
Supplies the negated packaging of the cost-visible blocker used when the universal foundation certificate assembles its conditional kernel. Downstream, prc_universal_foundation_conditional_certificate consumes this family of equivalences while wiring kernel, ordered-field, and trace-logic certificates together.
In the broader Recognition chain, native cost uniqueness is the PRC-side route toward T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$). The mixed two-prime character is the concrete obstruction: if such a $\chi$ can be built, the present target fails and the rigidity branch must close by another path (valuation or doubled-trace d'Alembert constraints). Recording both polarities of the equivalence keeps later certificates free to case-split on existence versus exclusion of the mixed model without re-proving classical logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.