PRCCharacterPrimeReciprocalWitnessGlobalizes_of_split
plain-language theorem explainer
If a ratio-orbit character satisfies the two-step split (any prime reciprocal forces the orbit-2 reciprocal, and orbit-2 reciprocal forces every prime reciprocal), then reciprocal orientation globalizes across all native prime axes. Cited when reducing prime no-mixing to a distinguished-axis transport through 2. The proof is a two-line composition of the split conjuncts.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose (i) whenever any native prime axis is reciprocal-oriented under $\chi$, the orbit-$2$ prime axis is reciprocal-oriented, and (ii) whenever the orbit-$2$ prime axis is reciprocal-oriented, every native prime axis is reciprocal-oriented. Then: if any native prime witness is reciprocal-oriented under $\chi$, every native prime axis is reciprocal-oriented.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed numerator over a nonzero distinction-natural denominator. Characters $\chi$ act on these orbits; reciprocal orientation means $\chi$ sends a prime direction to its reciprocal (cross-equality with the reciprocal orbit).
PRCCharacterPrimeReciprocalWitnessGlobalizes is the global no-mixing statement on the positive reciprocal branch: existence of one reciprocal-oriented native prime forces every native prime axis to be reciprocal-oriented.
The split form factors that claim through the distinguished axis $2$: first push any prime reciprocal witness onto orbit $2$, then push orbit-$2$ reciprocity out to every prime. This module develops native-cost uniqueness for PRC characters; the split is the bookkeeping device that makes prime-axis transport checkable in two shorter lemmas.
proof idea
Term proof by composing the two conjuncts of the split hypothesis. Unpack an existential reciprocal witness at some prime $p$. Apply the first conjunct to obtain reciprocal orientation at the orbit-$2$ prime axis. Feed that into the second conjunct at the target prime $r$. No further lemmas are invoked.
why it matters
One direction of the equivalence PRCCharacterPrimeReciprocalWitnessGlobalizes_iff_split, which lets the development switch freely between the global form and the $2$-axis split. Downstream, PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_of_split reuses this arrow to lift a calibrated split target to the global globalization target. The same fact appears in the native-cost uniqueness blocker certificate chain, where reciprocal-branch prime no-mixing is part of forcing the unique native cost (the $J$-cost of the forcing chain, T5). Without globalization, mixed reciprocal/identity orientations on distinct primes would block uniqueness of the cost character.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.