PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget_of_reciprocal_witness_globalizes
plain-language theorem explainer
If prime calibration globalizes one reciprocal-oriented native prime witness to every native prime axis, then placing the orbit-2 prime axis on the reciprocal branch forces every native prime axis onto that branch. Native-cost uniqueness certificates and the universal-foundation conditional certificate cite this implication. The proof is a one-line wrapper that feeds the globalized witness into the character-level transport lemma.
Claim. Assume that for every ratio character that is prime-direction calibrated, a single reciprocal-oriented native prime witness forces reciprocal orientation on every native prime axis. Then, for every such calibrated ratio character, if the orbit-$2$ prime axis lies on the reciprocal branch, every native prime axis lies on the reciprocal branch.
background
In the Primitive Recognition Calculus, a ratio character is a map on ratio orbits that encodes how recognition cost orients along multiplicative axes. Native prime axes are the prime orbits in that lattice; the orbit-$2$ axis is the distinguished binary axis. Prime-direction calibration fixes how the character sits relative to those axes.
Two target propositions organize the reciprocal branch. The reciprocal-witness globalization target says: if calibration admits even one reciprocal-oriented native prime witness, then reciprocal orientation holds on every native prime axis. The distinguished-axis target says the converse half for transport: once the orbit-$2$ axis is on the reciprocal branch, every native prime axis must be as well.
At character level, the upstream lemma already shows that a globalized reciprocal witness implies the two-to-all reciprocal force. This declaration lifts that character fact to the quantified target propositions used by the uniqueness certificates.
proof idea
Term-mode one-line wrapper. Introduce a ratio character $\chi$ together with the ratio-character and prime-calibration hypotheses. Apply the globalized-witness target hypothesis to obtain reciprocal-witness globalization for $\chi$. Feed that witness into the character-level lemma, which turns a reciprocal orientation of the orbit-$2$ axis into reciprocal orientation of an arbitrary native prime axis. No extra algebraic work; the quantification is pure specialization.
why it matters
Native cost uniqueness in PRC needs reciprocal orientation to be forced uniformly once calibration and a single reciprocal witness are present. This implication is one half of the split globalization target: it is packaged immediately into the split-target theorem that pairs prime-to-two transport with two-to-all transport.
Downstream, the native-cost uniqueness blocker certificate and the universal-foundation conditional certificate both depend on this chain. In the broader Recognition Science forcing picture, uniform reciprocal orientation on prime axes is part of locking the native cost to the unique $J$-cost shape (T5: $J(x)=(x+x^{-1})/2-1$), before $\phi$ and the eight-tick structure are forced. The declaration does not close uniqueness alone; it discharges the distinguished-axis half under the globalization hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.