PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_iff_no_mixed_prime_orientation
plain-language theorem explainer
Under prime cost calibration, reciprocal-witness globalization is equivalent to forbidding mixed identity/reciprocal orientations across prime axes. Cost-uniqueness arguments cite this to collapse two blocker targets into one. The proof is a pure Iff constructor from the two already-proved implication directions.
Claim. The following are equivalent for ratio characters that are prime-direction calibrated: (i) if any native prime axis is reciprocal-oriented, then every native prime axis is reciprocal-oriented; (ii) independent mixed identity/reciprocal choices on different prime axes are forbidden.
background
In the Primitive Recognition Calculus, a ratio character is a map on ratio orbits that encodes how multiplicative structure is read as cost. Prime-direction calibration restricts that character on native prime axes so each axis is oriented either as the identity branch or as the reciprocal branch.
Two global targets package what calibration is supposed to force. The reciprocal-witness globalization target says: if calibration admits even one reciprocal-oriented native prime witness, reciprocal orientation must hold on every native prime axis. The no-mixing target says: calibration must forbid independent mixed identity/reciprocal choices on different prime axes.
Both targets are quantified over the same class of prime-calibrated ratio characters. This module develops native-cost uniqueness by showing which of those targets survive and which are refuted, feeding the broader J-cost uniqueness story (T5) in the forcing chain.
proof idea
Term-mode Iff introduction. The forward direction applies the already-proved implication from reciprocal-witness globalization to no-mixed orientation (introduces a calibrated character and invokes the local no-mix lemma from globalization). The reverse applies the already-proved implication from no-mixed orientation to reciprocal-witness globalization (routes through the proved local prime-orientation target, then lifts local no-mix to reciprocal globalization). No new arithmetic is done here.
why it matters
This equivalence is the hinge that lets the module treat reciprocal globalization and no-mix as a single obstruction. Downstream, the reciprocal-globalization target is refuted by transporting the no-mix refutation across this Iff, and the same bridge chains into the identity-witness-excludes-reciprocal form. Those refutations feed the native-cost uniqueness blocker certificate and appear in the conditional universal-foundation certificate.
In framework terms, the result is bookkeeping inside the uniqueness path for the native recognition cost that eventually forces the J-cost of T5. It does not itself force J or phi; it collapses two prime-orientation targets so the later refutation can strike once.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.