PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesSplitTarget_refuted
plain-language theorem explainer
The split reciprocal-globalization target is false: prime calibration does not force both prime-to-two and two-to-all reciprocal transport. Anyone tracking native-cost uniqueness blockers cites this. The proof reduces the split via an equivalence to the already-refuted two-to-all half and discharges it in one step.
Claim. It is not the case that prime calibration forces the split reciprocal-globalization package (arbitrary prime-to-two reciprocal transport together with two-to-all reciprocal transport).
background
In the Primitive Recognition Calculus native-cost uniqueness development, reciprocal globalization asks whether calibration at primes forces reciprocal transport of cost data across prime axes. The split target packages two obligations: prime-to-two reciprocal transport, and two-to-all reciprocal transport.
An upstream equivalence shows the full split is logically equivalent to its second conjunct alone: the two-to-all reciprocal force. That second conjunct has already been refuted by reduction to a still earlier identity-force failure (prime identity does not force two-prime identity).
The local setting is the PRC native-cost uniqueness module, which systematically proves or refutes candidate forcing targets that would pin a unique native cost character from prime calibration data.
proof idea
Term-mode reduction. Assume the split target. Apply the equivalence ...SplitTarget_iff_two_prime_reciprocal_forces (left-to-right) to extract the two-to-all reciprocal force. Feed that into the already-proved refutation ...TwoPrimeReciprocalForcesPrimeReciprocalTarget_refuted, which itself reduces further to the identity-force refutation. Contradiction.
why it matters
Closes one branch of the reciprocal-globalization forcing tree: the split package cannot hold. Downstream, prc_native_cost_uniqueness_blocker_certificate aggregates such refutations into the uniqueness-blocker certificate, recording which candidate factorizations and transports fail. The universal-foundation conditional certificate also consumes this lineage when assembling kernel, ordered-field, and trace-logic status.
In the broader Recognition Science chain this is bookkeeping inside native-cost uniqueness, not a T5–T8 landmark. It narrows which calibration hypotheses can still force a unique J-cost character, keeping the uniqueness program honest about dead ends.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.