PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter_iff_cost_defect
plain-language theorem explainer
Equivalence of two calibrated composite-defect models for ratio characters: one exposing the forced image χ(2p)=p/2, and one exposing the matching composite J-cost failure. Cited by anyone closing the non-two mixed-prime / Pass 95 blocker path in native cost uniqueness. Proof is a pure bidirectional wrapper from the two already-proved one-way implications.
Claim. There exists a prime-direction-calibrated ratio character $\chi$ carrying a two-prime reciprocal-identity non-two composite defect if and only if there exists such a $\chi$ carrying the corresponding composite $J$-cost defect.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how multiplicative structure is read by the recognition cost. Prime-direction calibration forces the character on primes into a fixed normal form. The composite-defect model packages a witness that, for mixed primes other than the distinguished two-prime case, the forced image $\chi(2p)=p/2$ appears, matching the non-two mixed-prime blocker.
The cost-defect sibling replaces that orbit-level composite failure by the actual failure of the native $J$-cost on the same composite. Both models sit inside the native-cost uniqueness development: they are calibrated existential packages used to show that any character obeying the reciprocal-identity and prime-calibration constraints cannot hide a composite defect without also breaking $J$.
The two one-way theorems already convert a composite-defect witness into a cost-defect witness and conversely, by unpacking the same $\chi$ and re-wrapping the defect predicate.
proof idea
Term-mode Iff introduction. The forward arrow is the existing theorem that turns a calibrated composite-defect character into a calibrated cost-defect character. The reverse arrow is the dual theorem that recovers the composite-defect package from a cost-defect package. No new algebraic work: the proof is exactly the pair of those two implications.
why it matters
Closes the logical gap between the orbit-level composite blocker and the cost-visible Pass 95 blocker under prime calibration. Downstream, the universal foundation conditional certificate consumes this equivalence when assembling the PRC kernel, real-complete ordered field, and trace-logic bundle: it needs a single, interchangeable defect language rather than two parallel formulations.
In the broader Recognition chain this sits under native $J$-cost uniqueness (the T5 landmark $J(x)=(x+x^{-1})/2-1$). Showing composite defects and $J$-cost defects are interchangeable for calibrated characters is a necessary bookkeeping step before claiming that the recognition cost is forced uniquely on the ratio lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.