PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget
plain-language theorem explainer
Names the distinguished-axis reciprocal target: any prime-calibrated ratio character for which the orbit-2 axis sits on the reciprocal branch must place every native prime axis on that same branch. Downstream reciprocal-globalization splits and the native-cost uniqueness blocker certificate cite it as one half of the split. Pure Prop packaging of a universal quantification; no proof obligations discharged here.
Claim. For every map $\chi$ from ratio orbits to ratio orbits that is a ratio character and is prime-direction calibrated (its generated cost agrees with canonical $J$-cost on each prime orbit), the two-prime reciprocal forces every native prime onto the reciprocal branch.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. The distinguished orbit 2 is the ratio with numerator the two-orbit and denominator one. A ratio character $\chi$ is a map on these orbits; the generated cost is compared to the canonical $J$-cost (the unique cost from the Recognition Composition Law and T5) via cross-equality of ratio orbits.
Prime-direction calibration means that for every native prime orbit $p$, the cost induced by $\chi$ on the prime direction agrees with the on-orbit $J$-cost. The reciprocal branch is the automorphism that sends a recognition event to its inverse-ratio reverse (source and target swapped). The local module packages native-cost uniqueness into exact Lean targets rather than a single closed theorem.
Upstream, calibration is the predicate that cost-from-character matches $J$ on every prime direction; the two-prime-reciprocal-forces-prime-reciprocal predicate is the concrete forcing statement this target universally quantifies.
proof idea
Definitional Prop abbreviating a three-hypothesis universal quantifier: for all $\chi$, if $\chi$ is a ratio character and is prime-direction calibrated, then the two-prime-reciprocal-forces-prime-reciprocal property holds of $\chi$. No tactics, no lemmas applied; the body is the target statement itself.
why it matters
This is the second conjunct of the reciprocal-globalization split target (prime-to-two transport plus two-to-all transport). Downstream theorems show the full split is equivalent to this single target, and that assuming it yields the prime-identity-forces-two-prime-identity target and related exclusions of the identity branch.
It feeds the Pass-25 native-cost uniqueness blocker certificate, which records that uniqueness is not closed but is now split into exact Lean obligations. In the broader RS chain this sits under T5 $J$-uniqueness: once calibration locks primes to $J$, the reciprocal versus identity branch choice on the distinguished axis 2 must globalize to all primes, or native cost cannot be unique.
Open work remains to discharge the target itself (prove the forcing), not merely name it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.