PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter_of_cost_defect
plain-language theorem explainer
If a prime-calibrated ratio character witnesses a two-prime reciprocal/identity composite cost defect (non-two mixed primes), then it also witnesses the corresponding composite defect with forced image χ(2p)=p/2. Native-cost uniqueness and Pass-95 blocker arguments cite this direction. The proof unpacks the existential and applies the pointwise cost-defect-to-defect implication.
Claim. Suppose there exists a ratio-orbit character $\chi$ that is prime-direction calibrated and carries a two-prime reciprocal/identity non-two composite $J$-cost defect. Then there exists such a $\chi$ that is prime-direction calibrated and carries the corresponding composite defect with forced image $\chi(2p)=p/2$.
background
In the Primitive Recognition Calculus, ratio characters are maps $\chi$ on ratio orbits that encode how multiplicative structure is recognized. Prime-direction calibration restricts how $\chi$ acts on prime generators. The composite-defect models package a mixed-prime pathology: an identity-oriented prime witness together with a reciprocal-oriented prime witness on a non-two prime $p$, forcing a bad composite image at $2p$.
Two calibrated models sit side by side. The cost-visible version exposes an actual composite $J$-cost failure (the Pass 95 blocker in cost language). The plain defect version exposes the forced image $\chi(2p)=p/2$ without requiring the cost inequality in the outer package. Both are existential propositions over characters that are ratio characters and prime-direction calibrated.
Upstream, the pointwise lemma already converts a cost defect on a fixed $\chi$ into the plain composite defect on that same $\chi$, by discarding the cost conjunct after unpacking the reciprocal and identity witnesses.
proof idea
Term-mode existential transport. Unpack the cost-defect character hypothesis to obtain $\chi$ together with the ratio-character, prime-calibration, and pointwise cost-defect facts. Re-pack the same $\chi$ and the first two facts, replacing the cost-defect conjunct by the conclusion of PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeDefect_of_cost_defect applied to that conjunct. No new arithmetic is done at this layer.
why it matters
This is one direction of the calibrated equivalence between the cost-visible composite-defect model and the forced-image defect model. The immediate parent is the biconditional that identifies the two character propositions, which then feeds the bridge from prime-calibration forcing (excluding a prime-identity witness target) to nonexistence of the cost-defect character.
Further downstream, the universal foundation conditional certificate consumes this uniqueness/blocker stack. In Recognition Science terms the lemma sits inside native-cost uniqueness for the Primitive Recognition Calculus: ruling out mixed-prime composite defects supports uniqueness of the native $J$-cost (the T5 cost $J(x)=(x+x^{-1})/2-1$) under the recognition composition law, rather than allowing exotic characters that break composite cost accounting.
It does not by itself close the full uniqueness theorem; it only moves between two presentations of the same calibrated blocker.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.