PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget_of_two_prime_reciprocal_forces
plain-language theorem explainer
If prime-direction calibration puts the orbit-2 axis on the reciprocal branch and that forces every native prime axis onto the reciprocal branch, then no native prime axis may stay on the identity branch. Native-cost uniqueness certificates and reciprocal-globalization splits cite this implication. The proof is a one-line specialization of the character-level exclusion lemma under the calibrated hypotheses.
Claim. Assume that for every ratio character $\chi$ that is prime-direction calibrated, placing the orbit-$2$ prime axis on the reciprocal branch forces every native prime axis onto the reciprocal branch. Then, under the same calibration hypotheses, placing the orbit-$2$ axis on the reciprocal branch excludes any native prime axis from remaining on the identity branch.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how multiplicative structure is read as cost. Prime-direction calibration fixes the orientation of each native prime axis: identity (direct) versus reciprocal. The orbit-$2$ axis is the distinguished generator used to seed branch choice.
Two target propositions organize the globalization step. The forces-reciprocal target says: once calibration puts orbit-$2$ on the reciprocal branch, every native prime axis is forced reciprocal. The excludes-identity target says: under the same calibration, no native prime axis may remain identity-oriented. At the single-character level, the upstream lemma already shows that the forces-reciprocal property implies the excludes-identity property, by applying the force map to a putative identity witness and obtaining a contradiction with branch exclusivity.
This declaration lifts that character-level implication to the quantified target props used by the native-cost uniqueness certificate chain.
proof idea
One-line wrapper. Introduce a ratio character $\chi$ together with the ratio-character and prime-calibration hypotheses. Specialize the assumed forces-reciprocal target at $(\chi,h_\chi,h_{\mathrm{prime}})$ to obtain the character-level forces-reciprocal fact. Feed that fact into the upstream character lemma, which concludes the character-level excludes-identity property. That is exactly the body of the excludes-identity target.
why it matters
Closes one direction of the equivalence between the forces-reciprocal target and the excludes-identity target, so either formulation may be used interchangeably in the uniqueness pipeline. Downstream, it feeds the identity-forces-two-identity target, the reciprocal-witness globalization split, and the native-cost uniqueness blocker certificate. It also appears in the conditional universal-foundation certificate, tying prime-axis branch discipline into the broader PRC foundation stack that supports J-cost uniqueness (forcing chain T5) and the Recognition Composition Law. Without this lift, character-level exclusion would not discharge the quantified targets the certificate interface demands.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.