PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget
plain-language theorem explainer
Packages the universal target that every prime-calibrated ratio character on rational orbits obeys two-prime reciprocal exclusion: if the orbit-2 axis is reciprocal-oriented, no native prime axis may be identity-oriented. Downstream uniqueness certificates and branch-equivalence theorems cite this Prop as a named forcing goal. The body is a pure quantifier wrapper, not a proof.
Claim. For every map $\chi$ from ratio orbits to ratio orbits that is a ratio character and is calibrated on every native prime direction (its generated cost matches canonical $J$-cost on each prime orbit), the following holds: if $\chi$ sends the distinguished orbit-$2$ prime axis to its reciprocal, then for every native prime $p$, $\chi$ does not fix the corresponding prime direction (no identity-oriented native prime witness).
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed integer numerator over a nonzero distinction-nat denominator. A ratio character $\chi$ is an endomorphism of that orbit type used to manufacture a native cost via costFromCharacter.
Prime-direction calibration means that on every native prime orbit the character-generated cost agrees with the canonical $J$-cost (cross-equality of orbits). The reciprocal automorphism swaps an event with its inverse-ratio partner; the identity event sits at the $J$-minimum $x=1$.
The local predicate being forced is the contrapositive branch normal form: if $\chi$ places the distinguished orbit-$2$ prime axis on the reciprocal branch, then no native prime axis may remain identity-oriented. This module packages native-cost uniqueness obstacles as exact Lean targets rather than informal gaps.
proof idea
Definitional packaging only. The declaration is a Prop abbreviation whose body is the universal quantification
$\forall\chi,;\mathrm{PRCRatioCharacter},\chi\to\mathrm{PrimeDirectionCalibrated},\chi\to\mathrm{TwoPrimeReciprocalExcludesPrimeIdentity},\chi$.
No tactics or lemmas are applied; the mathematical content lives in the three named predicates it composes.
why it matters
This target is one exact split of the still-open native cost uniqueness problem. The Pass-25 blocker certificate records that uniqueness is not closed and lists this (and sibling) targets as the missing mathematics.
It is definitionally interchangeable with the dual branch "prime identity forces two-prime identity" and with "two-prime reciprocal forces prime reciprocal," via the module's iff theorems. Those equivalences let the forcing chain choose whichever orientation is convenient when transporting calibration from the orbit-2 axis to all native primes.
In the broader Recognition Science chain this sits under T5 $J$-uniqueness: native cost must collapse to $J(x)=(x+x^{-1})/2-1$. Ruling out mixed identity/reciprocal prime witnesses is a necessary step before the character is forced onto a single global branch compatible with the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.