PRCCharacterPrimeReciprocalWitnessGlobalizes_iff_split
plain-language theorem explainer
Equates two formulations of reciprocal-witness globalization for a ratio-orbit character: the direct “one reciprocal prime forces all primes reciprocal” property, and its split form that routes through the distinguished prime axis 2. Anyone tracking prime no-mixing or native-cost uniqueness cites this bridge. The proof is a pure Iff pair of the two already-proved one-direction lemmas.
Claim. Let $\chi$ be a map on rational orbits. The following are equivalent: (i) if any native prime axis is reciprocal-oriented under $\chi$, then every native prime axis is reciprocal-oriented; (ii) reciprocal orientation of any prime forces reciprocal orientation of the prime axis $2$, and reciprocal orientation of axis $2$ forces reciprocal orientation of every native prime.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. A character $\chi$ acts on these orbits. Reciprocal orientation means $\chi$ sends a prime direction to its reciprocal (cross-equality with the reciprocal orbit).
Prime no-mixing on the reciprocal branch says that reciprocal orientation cannot appear on one native prime axis without appearing on all of them. The direct globalization predicate packages that implication. The split form factors it through the distinguished prime axis $2$: any prime reciprocal forces axis-$2$ reciprocal, and axis-$2$ reciprocal forces every prime reciprocal.
This module develops uniqueness of the native cost (the J-cost of Recognition Science) from character and trace hypotheses. The two globalization predicates are intermediate Prop-level interfaces used when transporting reciprocal branch data along prime axes.
proof idea
Term-mode Iff constructor. The forward direction applies PRCCharacterPrimeReciprocalWitnessGlobalizesSplit_of_reciprocal_witness_globalizes, which builds the conjunction of the two split factors from the global implication. The reverse applies PRCCharacterPrimeReciprocalWitnessGlobalizes_of_split, which chains the two split factors: from a reciprocal witness at $p$, force reciprocal at $2$, then force reciprocal at the target prime $r$. No extra tactics or algebraic work.
why it matters
Native cost uniqueness in PRC is the local avatar of T5 J-uniqueness: the cost functional is forced to be $J(x)=(x+x^{-1})/2-1$. Reciprocal-branch prime no-mixing is one of the structural constraints that keep admissible characters from mixing identity and reciprocal orientations across prime axes.
This equivalence lets downstream certificates switch freely between the compact global form and the split form that is easier to discharge stepwise. It is consumed by prc_native_cost_uniqueness_blocker_certificate (the uniqueness blocker package) and by prc_universal_foundation_conditional_certificate in UniversalFoundation. Without the bridge, the split lemmas and the global predicate would remain two parallel APIs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.