PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter
plain-language theorem explainer
Packages the existence of a ratio-orbit map that is a genuine ratio character, prime-direction calibrated to canonical J-cost, and carries a non-two composite defect under the two-prime reciprocal identity (forcing the image χ(2p)=p/2). Native-cost uniqueness and Pass-95 blocker arguments cite it as the character-level composite-defect model. The body is a pure existential conjunction of three named character properties.
Claim. There exists a map $\chi$ on rational orbits such that $\chi$ is a ratio character, $\chi$ is prime-direction calibrated (its induced cost agrees with canonical $J$-cost on every prime orbit), and $\chi$ exhibits a non-two composite defect under the two-prime reciprocal identity (with forced composite image $\chi(2p)=p/2$).
background
In the Primitive Recognition Calculus, ratio orbits are rational displays: a signed-orbit numerator over a nonzero distinction-nat denominator. A ratio character is a map on those orbits used to induce a recognition cost via the character-to-cost construction. Prime-direction calibration demands that this induced cost match the canonical $J$-cost on every native prime orbit (cross-equality of cost-from-character against the on-orbit $J$ value).
The ambient module develops uniqueness of the native recognition cost. Recognition cost is the doubled $J$-cost (equivalently the defect functional, which equals $J$ on positive reals). The two-prime reciprocal identity constrains how a character may act on products involving the prime $2$; a non-two composite defect is a failure of that identity on composites built from primes other than $2$, exposed here by forcing $\chi(2p)=p/2$.
Upstream, prime-direction calibration is the agreement condition on prime orbits; the composite-defect conjunct is the character-level packaging of the Pass-95 non-two mixed-prime blocker with the forced composite image made explicit.
proof idea
Definitional packaging only: the proposition is the existential statement that some orbit map $\chi$ simultaneously satisfies the three conjuncts (ratio character, prime-direction calibration, and two-prime reciprocal-identity non-two composite defect). No tactics or lemmas are applied; downstream theorems unpack the witness by rcases and reassemble related defect or mixed-character forms.
why it matters
This is the character-level composite-defect model used throughout the native-cost uniqueness development. Downstream it is shown equivalent to the cost-visible composite-defect character (bidirectional conversion theorems) and to the non-two mixed-prime character (again by iff). It is the target of the two-three local orientation-failure character implication and appears in the calibration-forces-prime-identity chain as the negated blocker: prime calibration forcing prime identity and two-prime identity is equivalent to absence of this non-two composite defect character.
In framework terms it sits inside the PRC attack on uniqueness of the $J$-cost (T5 landmark: $J(x)=(x+x^{-1})/2-1$). Exposing $\chi(2p)=p/2$ makes the composite $J$-cost failure concrete rather than purely mixed-prime abstract, closing the Pass-95 blocker at the character layer so cost-level uniqueness arguments can discharge it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.