PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_of_no_mixed_prime_orientation
plain-language theorem explainer
Under prime-direction calibration of a ratio character, forbidding mixed identity/reciprocal choices across prime axes already forces reciprocal orientation to globalize from any single native prime witness. Cost-uniqueness and foundation-certificate authors cite this as one direction of the no-mixing ↔ reciprocal-globalization equivalence. The proof is a short application of the local-orientation theorem plus the character-level globalization lemma.
Claim. Assume that every ratio character $\chi$ that is prime-direction calibrated has no mixed prime orientation (identity vs reciprocal cannot be chosen independently on different prime axes). Then every such $\chi$ also satisfies reciprocal-witness globalization: if any native prime axis is reciprocal-oriented, every native prime axis is reciprocal-oriented.
background
In the Primitive Recognition Calculus, ratio characters $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ encode how multiplicative ratio data are read before a native cost is attached. Prime-direction calibration restricts $\chi$ on the distinguished prime axes that generate the free abelian skeleton of positive rationals.
Two related targets appear in the native-cost uniqueness development. The no-mixing target demands that calibration forbid independent identity/reciprocal choices on different prime axes: once orientation is fixed on one prime, it cannot flip on another. The reciprocal-witness globalization target is the existential form: a single reciprocal-oriented native prime witness forces reciprocal orientation on every native prime axis.
Upstream, local prime orientation under calibration is already proved unconditionally. Separately, at the character level, local orientation plus no-mixing implies reciprocal-witness globalization. This declaration lifts that character lemma to the calibration-target layer.
proof idea
Fix a ratio character $\chi$ that is prime-direction calibrated. The already-proved local-orientation target supplies local prime orientation for $\chi$. The assumed no-mixing target supplies no mixed prime orientation for the same $\chi$. Feed both into the character-level lemma that local orientation plus no-mixing yields reciprocal-witness globalization. The resulting universal quantification is exactly the reciprocal-witness globalization target.
why it matters
Native cost uniqueness in PRC needs a rigid orientation story on prime axes: mixed identity/reciprocal choices would spawn non-unique cost factorizations. This theorem shows that the no-mixing calibration target already implies full reciprocal-witness globalization, so the two packaging forms are not independent obligations.
It is one half of the iff equating the two targets, and it feeds the native-cost uniqueness blocker certificate and the conditional universal-foundation certificate. In the broader Recognition chain, locking prime-axis orientation is part of forcing a unique native cost compatible with the J-cost structure (T5) before phi and the octave constraints enter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.