PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter
plain-language theorem explainer
Names the existence of a prime-calibrated ratio character that still exhibits a non-two composite J-cost defect with mixed identity and reciprocal two-prime orientation. Cost-uniqueness and mixed-prime exclusion arguments cite it as the Pass-95 blocker in cost-visible form. The body is a pure existential packaging of three character predicates; no proof work.
Claim. There exists a map $\chi$ on rational ratio-orbits that is a ratio character, is prime-direction calibrated (its induced cost agrees with canonical $J$-cost on every native prime orbit), and carries a two-prime reciprocal/identity non-two composite cost defect.
background
In the Primitive Recognition Calculus, ratio-orbits are integer-numerator / nonzero-denominator displays of rational recognition ratios. A ratio character $\chi$ is a structure-preserving self-map of those orbits; cost is recovered from $\chi$ via costFromCharacter and compared to the canonical $J$-cost on orbits.
Prime-direction calibration means that on every native prime orbit the character-induced cost matches the canonical $J$-cost (cross-equality of orbits). The third conjunct packages a mixed two-prime witness: identity orientation on one prime direction and reciprocal orientation on another, together with a visible composite $J$-cost failure off the two-primary locus.
The module develops native-cost uniqueness for PRC characters. This definition is the cost-visible form of the calibrated mixed-prime composite-defect model (Pass 95 blocker), exposing the actual composite $J$-cost failure rather than only an abstract orientation defect.
proof idea
Definitional packaging only: the proposition is the existential
$\exists,\chi$, with three conjuncts PRCRatioCharacter, PRCCharacterPrimeDirectionCalibrated, and PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeCostDefect. No tactics, no lemmas applied at this site. Downstream theorems unpack the witness by rcases and reassemble the non-cost or cost forms.
why it matters
This is the cost-visible Pass-95 blocker used throughout native-cost uniqueness. Downstream, it is proved equivalent to the non-cost composite-defect character (...DefectCharacter_iff_cost_defect), implied by two-three local orientation failure, and shown absurd under mixed-composite cost consistency.
The forcing targets cite it directly: prime calibration forcing prime-identity and two-prime identity is equivalent to nonexistence of this character; mixed-composite consistency is equivalent to its absence. In the Recognition chain this sits under T5 $J$-uniqueness and the Recognition Composition Law: a calibrated character that still fails composite $J$-cost would obstruct uniqueness of the native cost, so closing the blocker is part of forcing $J(x)=(x+x^{-1})/2-1$ as the only admissible cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.