PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesSplitTarget_of_two_prime_reciprocal_forces
plain-language theorem explainer
If prime calibration already forces every native prime axis onto the reciprocal branch once the orbit-2 axis is reciprocal, then the full reciprocal-globalization split holds: both prime-to-two and two-to-all reciprocal transport. Native-cost uniqueness and the universal-foundation certificate cite this reduction. The proof builds the conjunction by deriving the missing prime-to-two leg from a short exclusion-to-identity chain, then reusing the given two-to-all force.
Claim. Assume that whenever a ratio-orbit character is prime-direction calibrated and the orbit-$2$ prime axis lies on the reciprocal branch, every native prime axis is reciprocal. Then the reciprocal-globalization split target holds: prime calibration forces both (i) reciprocal transport from an arbitrary calibrated prime axis to the orbit-$2$ axis and (ii) reciprocal transport from orbit-$2$ to every native prime axis.
background
In the Primitive Recognition Calculus, ratio-orbit characters assign each ratio orbit an orientation (identity or reciprocal). Prime-direction calibration fixes how those orientations sit on native prime axes. The distinguished orbit-$2$ prime axis is the pivot for globalization arguments.
The two-to-all reciprocal target says: once calibration puts orbit-$2$ on the reciprocal branch, every native prime axis must be reciprocal. The split target packages that with the converse transport leg (arbitrary calibrated prime reciprocal implies orbit-$2$ reciprocal). Together they assert that a single reciprocal witness on any calibrated prime globalizes across the prime lattice.
Upstream, exclusion of residual identity when orbit-$2$ is reciprocal is derived from the two-to-all force, and that exclusion yields the one-sided identity-forces-two target, which in turn yields the prime-to-two reciprocal leg.
proof idea
Tactic proof by constructor on the split conjunction.
Left conjunct (prime-to-two reciprocal): from the given two-to-all reciprocal force, apply the lemma that produces the two-reciprocal-excludes-prime-identity target; feed that exclusion into the lemma producing the prime-identity-forces-two-identity target; finally apply the lemma that turns identity-forces-two into prime-reciprocal-forces-two-reciprocal.
Right conjunct: immediate from the hypothesis (exact hforces).
why it matters
This is the one-direction half of the iff equating the reciprocal-globalization split with the two-to-all reciprocal force alone. Downstream, that iff and the native-cost uniqueness blocker certificate consume it; the universal-foundation conditional certificate also depends on this uniqueness stack.
In the Recognition framework the native cost is forced toward the unique $J$-cost of T5 ($J(x)=(x+x^{-1})/2-1$), via the Recognition Composition Law. Closing reciprocal globalization on calibrated prime axes removes a branch-choice obstruction in that uniqueness argument: characters cannot mix identity and reciprocal orientations across primes once one reciprocal witness is fixed.
It does not finish uniqueness by itself; it discharges one structured split target inside the PRC native-cost uniqueness development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.