PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeCostDefect
plain-language theorem explainer
Predicate on a ratio-orbit map χ packing the cost-visible mixed composite defect: χ sends the 2-direction to its reciprocal, fixes some other prime direction p, images the composite 2·p as recip(2)·p, yet the induced cost fails native J-cost calibration on that composite orbit. Uniqueness and prime-calibration arguments cite it as the blocker that must be ruled out. Pure definitional Prop; no proof content.
Claim. A map $\chi$ on ratio orbits has the cost-visible two-prime mixed composite defect when $\chi$ sends the direction of $2$ to its reciprocal, and there exists a prime orbit $p\neq 2$ such that $\chi$ fixes the direction of $p$, $\chi$ sends the composite direction $2\cdot p$ to $\mathrm{recip}(2)\cdot p$, and the cost induced by $\chi$ at $2\cdot p$ is not cross-equal to the native cost on that orbit.
background
In the Primitive Recognition Calculus, ratio orbits are the multiplicative skeleton on which characters act. A ratio character $\chi$ reorients directions; the two-prime direction and other native prime directions generate composites under orbit multiplication. Reciprocal orientation swaps a direction with its inverse orbit.
Native cost on an orbit is the J-cost calibration (the unique cost forced by the Recognition Composition Law and T5 J-uniqueness, $J(x)=(x+x^{-1})/2-1$). The sibling costFromCharacter lifts a character to an induced cost on orbits; crossEq is equality of orbits up to the native cross identification.
This module isolates uniqueness of that native cost. The mixed pattern (orbit 2 reciprocal, a distinct prime $p$ identity) is the critical orientation data: the composite $2\cdot p$ can look character-consistent while still failing cost calibration. The doc-comment states the meaning directly: the mixed composite image is not J-cost calibrated at $2\cdot p$.
proof idea
Definitional packaging only: the body is the conjunction of (i) cross-equality of $\chi(2)$ with $\mathrm{recip}(2)$, (ii) existence of a prime orbit $p\neq 2$ fixed by $\chi$, (iii) cross-equality of $\chi(2\cdot p)$ with $\mathrm{recip}(2)\cdot p$, and (iv) failure of cross-equality between costFromCharacter $\chi$ at $2\cdot p$ and the native cost on that orbit. No tactics or lemmas.
why it matters
This is the cost-visible form of the Pass-95-style composite blocker. Downstream, it is equivalent to the non-cost mixed defect (...Defect_iff_cost_defect and the two one-way bridges), so ruling out either form rules out both. It is the defect clause inside PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter, the calibrated model that exposes actual composite J-cost failure.
Negating the calibrated existence yields PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget: prime calibration must still calibrate $2\cdot p$ under mixed orientation data. The universal foundation open-target ledger also references this family. Framework-wise it sits under T5 J-uniqueness and RCL: composite directions cannot evade the unique native cost even when characters mix reciprocal and identity on prime generators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.