PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget_of_two_prime_reciprocal_excludes
plain-language theorem explainer
Assuming the two-reciprocal exclusion target (orbit-2 reciprocal forbids any identity-oriented native prime), the distinguished-axis reciprocal globalization target follows: every native prime axis is forced reciprocal. Native-cost uniqueness and the universal-foundation certificate cite this bridge. The proof is a short term application of the character-level local-exclusion lemma plus the already-proved local prime-orientation target.
Claim. If, for every ratio-orbit character $\chi$ that is prime-direction calibrated, orbit-$2$ reciprocal orientation excludes any identity-oriented native prime axis, then for every such $\chi$, orbit-$2$ reciprocal orientation forces every native prime axis onto the reciprocal branch.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ maps ratio orbits to ratio orbits and encodes how cost-relevant axes are oriented. Prime-direction calibration fixes how native prime axes sit relative to the distinguished orbit-$2$ axis. Axes may lie on the identity branch or the reciprocal branch.
Two named targets organize the globalization step. The exclusion target says: if calibration puts orbit $2$ on the reciprocal branch, then no native prime axis may remain identity-oriented. The forces target is stronger in form: the same hypothesis forces every native prime axis onto the reciprocal branch.
Upstream, local prime orientation under calibration is already proved, and a character-level lemma converts local orientation plus two-reciprocal exclusion into full reciprocal forcing on all native primes. This declaration lifts that character lemma to the calibrated target level.
proof idea
Term-mode proof. Introduce a calibrated ratio character $\chi$. Apply the character-level lemma PRCCharacterTwoPrimeReciprocalForcesPrimeReciprocal_of_local_excludes_prime_identity, feeding two facts: the proved local prime-orientation target specialized to $\chi$, and the assumed exclusion target specialized to $\chi$. No further casework.
why it matters
This is one direction of the equivalence between the two-reciprocal exclusion target and the two-reciprocal forces target, so either formulation may be used in the native-cost uniqueness chain. It is also the bridge used when identity-forces-two is reduced to the reciprocal forces target.
Downstream it appears in the native-cost uniqueness blocker certificate and in the conditional universal-foundation certificate. Within Recognition Science this sits in the foundation layer that pins the native cost character before J-uniqueness (T5) and the RCL are applied at the continuum level: without reciprocal globalization on prime axes, the native cost would not be forced unique on the prime lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.