PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesSplitTarget_iff_two_prime_reciprocal_forces
plain-language theorem explainer
The split reciprocal-globalization target is equivalent to its second conjunct alone: once prime calibration forces the orbit-2 axis onto the reciprocal branch, every native prime axis follows. Anyone tracking the native-cost uniqueness blockers cites this reduction. The proof is a two-constructor term pairing the projection and the reverse reconstruction lemmas.
Claim. The split reciprocal-globalization target (arbitrary prime-to-two reciprocal transport conjoined with two-to-all reciprocal transport) holds if and only if the distinguished-axis target holds: for every ratio character $\chi$ that is prime-direction calibrated, placing the orbit-$2$ prime axis on the reciprocal branch forces every native prime axis onto the reciprocal branch.
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio characters $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ encode multiplicative structure on ratio orbits. Prime-direction calibration pins how $\chi$ acts on prime axes. Reciprocal-branch membership records whether an axis is sent to its multiplicative inverse orientation.
Two Prop targets organize the remaining globalization work. The distinguished-axis target asserts that, after calibration, reciprocal placement of the orbit-$2$ prime axis forces reciprocal placement of every native prime axis. The split target is the conjunction of that statement with a prime-to-two reciprocal transport clause.
The local module closes uniqueness of the native cost functional built from doubled-trace and d'Alembert data; these targets sit inside the reciprocal-coherence half of that program.
proof idea
Term-mode biconditional: the forward map is PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget_of_split, which projects the second conjunct of the split. The reverse map is PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesSplitTarget_of_two_prime_reciprocal_forces, which rebuilds the full conjunction from the distinguished-axis target alone (constructor plus an exclusion step that discharges the prime-to-two half). No further tactics.
why it matters
This equivalence collapses the split globalization target to a single Prop, so refutations and certificates need only attack the two-to-all reciprocal force. Downstream, PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesSplitTarget_refuted applies the forward direction to push a negation through the iff. The same name appears in the native-cost uniqueness blocker certificate and feeds the conditional universal-foundation certificate in UniversalFoundation.
Inside Recognition Science this is bookkeeping on the J-cost uniqueness path (T5 in the forcing chain): reciprocal coherence of calibrated prime axes is part of forcing the native cost to the unique $J(x)=(x+x^{-1})/2-1$ shape. It does not itself prove uniqueness; it trims the target surface that uniqueness blockers and refutations act on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.