PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter_of_composite_defect
plain-language theorem explainer
A prime-calibrated ratio character that already carries a mixed-prime composite defect (identity on one odd prime, reciprocal on 2, with forced image χ(2p)=p/2) automatically carries the corresponding composite J-cost defect. Anyone proving equivalence of the Pass-95 blocker with its cost-visible form cites this. The proof unpacks the existential witness and applies the character-level cost-defect lift.
Claim. If there exists a ratio-orbit character $\chi$ that is prime-direction calibrated and satisfies the two-prime reciprocal/identity non-two composite defect (forced image $\chi(2p)=p/2$ for some odd prime $p$), then the same $\chi$ witnesses the calibrated cost-visible composite defect: the composite $J$-cost failure on that mixed-prime product.
background
In the Primitive Recognition Calculus, ratio characters are maps $\chi$ on ratio orbits that encode orientation data for multiplicative generators. Prime-direction calibration forces the character to treat primes in a fixed directional convention. The composite-defect model packages a mixed-prime witness: reciprocal orientation on the prime 2, identity orientation on some odd prime $p\neq 2$, together with the forced composite image $\chi(2p)=p/2$.
The cost-visible sibling replaces that algebraic composite image by the actual failure of the native $J$-cost on the composite. Here $J$ is the unique cost from the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$. The module develops native-cost uniqueness by showing that calibrated characters cannot hide composite cost failures once the mixed-prime blocker is present.
Upstream, the character-level theorem already lifts a plain composite defect on a fixed $\chi$ to the corresponding cost defect on that same $\chi$. The calibrated character props simply existentially quantify over prime-calibrated ratio characters carrying those defects.
proof idea
Term-mode unpacking of the existential. From the hypothesis, obtain a witness $\chi$ together with proofs that it is a ratio character, prime-direction calibrated, and carries the composite defect. Re-pack the same $\chi$ and the same calibration data, replacing the composite-defect conjunct by the conclusion of the character-level lift PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeCostDefect_of_composite_defect applied to that conjunct. No new arithmetic is performed at this layer.
why it matters
This is the forward half of the iff equating the calibrated composite-defect character with its cost-visible twin, and it feeds the exclusion target that says prime calibration forces the two-prime reciprocal law precisely when no composite cost-defect character exists. Downstream it is also the bridge from two-three local orientation failure into the cost-defect character, and it appears in the conditional universal-foundation certificate chain.
In framework terms it tightens the native-cost uniqueness story around T5 ($J$-uniqueness) and the Recognition Composition Law: once mixed-prime orientation data are calibrated, composite $J$-cost failure is not an independent hypothesis but a forced readout of the algebraic defect. That keeps the Pass-95 blocker aligned with the cost that later pins $\phi$ and the rung ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.