PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_iff_no_composite_cost_defect_character
plain-language theorem explainer
Prime-calibration consistency on mixed-orientation composites 2·p is equivalent to the nonexistence of a calibrated ratio character that exhibits a composite J-cost defect. Anyone closing the Pass-95 cost-visible blocker or assembling the PRC universal-foundation certificate cites this bridge. The proof is a two-constructor term packaging the already-proved forward absurdity and converse forcing lemmas.
Claim. The universal target that every prime-calibrated ratio character sending the orbit of $2$ to its reciprocal and a distinct native prime $p$ to the identity must still cost-calibrate the composite direction $2\cdot p$ holds if and only if there is no prime-calibrated ratio character that realizes a two-prime reciprocal/identity composite cost defect.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that preserves the multiplicative structure used to read native cost. Prime-direction calibration requires $\chi$ to act as the identity (up to the orbit equivalence) on every native prime direction. The mixed-orientation data of interest sends the orbit of $2$ to its reciprocal while sending a distinct native prime $p$ to the identity; the composite direction $2\cdot p$ is then the cost-visible test case.
The consistency target asserts that every such calibrated character still satisfies the cross-equality that forces cost calibration on $2\cdot p$. The opposing defect character is an existential model: some calibrated $\chi$ that carries both the mixed two-prime orientation data and a genuine composite J-cost failure. That defect model is the calibrated, cost-visible form of the Pass-95 blocker.
Locally this sits in the native-cost uniqueness development, where uniqueness of the PRC cost functional is reduced to ruling out composite cost defects under prime calibration.
proof idea
Term-mode biconditional: the proof is the pair of the two already-established implications. Left-to-right applies the absurdity lemma: assuming the universal mixed-composite consistency target, any purported calibrated composite-defect character is contradictory. Right-to-left applies the forcing lemma: assuming no such defect character exists, every prime-calibrated character with the mixed two-reciprocal / $p$-identity data is forced to cost-calibrate $2\cdot p$. No further case analysis is performed here.
why it matters
This iff is the clean logical hinge between the universal consistency target and the nonexistence of the calibrated composite-defect witness. Downstream, the negated form of the same equivalence is recorded explicitly, and the universal-foundation conditional certificate consumes the surrounding uniqueness package. In the Recognition forcing chain the point is cost uniqueness for the native J-cost (the T5 landmark $J(x)=(x+x^{-1})/2-1$), under prime calibration and mixed orientation: composite directions must not open a cost defect once primes are fixed. Closing or discharging the defect side is what lets the PRC native-cost story feed the broader foundation certificate rather than remain a Pass-95 blocker.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.