PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_of_split
plain-language theorem explainer
Under the split reciprocal-globalization hypothesis (prime-to-two plus two-to-all transport), prime calibration forces full reciprocal-witness globalization: one reciprocal-oriented native prime witness implies reciprocal orientation on every native prime axis. Native-cost uniqueness and the universal-foundation certificate cite this packaging. Proof is a short term that feeds both split halves into the character-level split lemma.
Claim. Assume the split target: under prime calibration, reciprocal orientation transports from an arbitrary native prime to the orbit-$2$ axis, and from orbit-$2$ to every native prime. Then the unsplit target holds: for every ratio character $\chi$ that is prime-direction calibrated, if some native prime axis is reciprocal-oriented, every native prime axis is reciprocal-oriented.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits encoding how recognition cost orients along multiplicative axes. Prime-direction calibration means $\chi$ is fixed on the distinguished prime axes in the native sense used by the cost uniqueness program.
Reciprocal-witness globalization says that a single reciprocal-oriented native prime witness forces reciprocal orientation on all native prime axes. The module splits that demand into two transport legs: arbitrary prime $\to$ orbit-$2$, then orbit-$2$ $\to$ all primes. The split target is exactly the conjunction of those two forced-transport propositions under prime calibration.
Upstream, the character-level lemma already packages the same split for a fixed $\chi$: given both transport halves for that character, full reciprocal-witness globalization follows by composing them.
proof idea
Term-mode packaging. Introduce the character $\chi$ and the two hypotheses (ratio character, prime-direction calibration). Apply the character-level split lemma PRCCharacterPrimeReciprocalWitnessGlobalizes_of_split, supplying the pair whose first component is the prime-to-two half of the global split target at $\chi$ and whose second is the two-to-all half at $\chi$. No further case analysis.
why it matters
This is the split-to-unsplit direction of the reciprocal-witness globalization target under prime calibration. It pairs with the converse to give the iff that equates the unsplit target with the two-leg split, so later certificates can discharge either form.
Downstream it feeds prc_native_cost_uniqueness_blocker_certificate and, via the foundation layer, prc_universal_foundation_conditional_certificate. In the Recognition chain this sits inside native $J$-cost uniqueness for PRC characters: reciprocal orientation must globalize once a prime axis is calibrated, consistent with the RCL/$J$-uniqueness forcing (T5) that pins the cost functional before $\phi$ and the eight-tick structure appear.
It does not itself close cost uniqueness; it only collapses the split packaging so the remaining transport legs can be attacked separately.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.