PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget_iff_two_prime_reciprocal_forces
plain-language theorem explainer
Equivalence of two formulations of the prime-calibration reciprocal constraint: once the orbit-2 axis sits on the reciprocal branch, forbidding any native prime axis from remaining identity-oriented is the same as forcing every native prime axis onto the reciprocal branch. Native-cost uniqueness certificates cite this bridge. The proof is a pure term pairing of the two one-direction implications.
Claim. The following are equivalent. (A) For every ratio character $\chi$ that is prime-direction calibrated: if the orbit-$2$ prime axis is reciprocal-oriented, then no native prime axis of $\chi$ remains identity-oriented. (B) For every such $\chi$: if the orbit-$2$ prime axis is reciprocal-oriented, then every native prime axis of $\chi$ is reciprocal-oriented.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits encoding how multiplicative structure is read by the recognition cost. Prime-direction calibration fixes the orientation of distinguished prime axes relative to the native cost; the orbit-$2$ axis is the distinguished even prime that anchors the reciprocal-versus-identity branch choice.
Two target propositions package the globalization of that branch choice. The exclusion target asserts: if calibration puts orbit $2$ on the reciprocal branch, then no native prime axis may stay identity-oriented. The forces target asserts the positive dual: every native prime axis must then lie on the reciprocal branch. Both are universal statements over calibrated ratio characters.
This module develops native-cost uniqueness for PRC characters. The two targets are intermediate Prop interfaces used to discharge reciprocal-branch constraints before the uniqueness blocker certificate is assembled.
proof idea
Term-mode biconditional: the proof is the pair constructor $\langle\cdot,\cdot\rangle$ applied to the two already-proved one-way maps.
Left-to-right applies the lemma that turns the exclusion target into the forces target (via the local character-level implication from excluding prime identity to forcing prime reciprocal). Right-to-left applies the converse lemma that turns the forces target into the exclusion target (via the character-level implication from forcing prime reciprocal to excluding prime identity). No extra hypotheses or rewriting are needed; the iff is pure packaging of those two arrows.
why it matters
Native-cost uniqueness in PRC needs a clean statement that reciprocal orientation on the distinguished orbit-$2$ axis globalizes to all native primes. Packaging exclusion and forcing as equivalent targets lets downstream certificates pick whichever polarity is convenient without re-proving transport.
The native-cost uniqueness blocker certificate consumes this bridge among its reciprocal-branch obligations. The universal-foundation conditional certificate sits further downstream in the same foundation stack. In the broader Recognition Science forcing chain, this sits under T5 J-uniqueness: the native cost is the unique J-type functional compatible with the Recognition Composition Law, and reciprocal-branch rigidity on prime axes is part of locking that uniqueness for discrete characters.
No open scaffold remains here; both directions are already closed theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.