PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget_refuted
plain-language theorem explainer
The distinguished-axis reciprocal globalization target is false: calibration that puts the orbit-2 prime axis on the reciprocal branch does not force every native prime axis onto that branch. Native-cost uniqueness and blocker-certificate work cite this negative result. The proof is a short reduction through an equivalence to the already-refuted identity-forces-two target.
Claim. It is not the case that every ratio-orbit character $\chi$ that is prime-direction calibrated and places the orbit-$2$ prime axis on the reciprocal branch must place every native prime axis on the reciprocal branch.
background
In the Primitive Recognition Calculus, native cost uniqueness is attacked by forcing targets on ratio-orbit characters $\chi$. A character is prime-direction calibrated when its action on prime axes is pinned by a fixed calibration convention. The reciprocal branch is the orientation that sends a prime axis to its multiplicative inverse rather than the identity orientation.
The target proposition asserts a distinguished-axis globalization: if calibration already puts the orbit-$2$ prime on the reciprocal branch, then every native prime axis is forced reciprocal as well. An equivalent identity-branch target (prime identity forces the two-prime identity) has already been refuted upstream. An in-module equivalence identifies the reciprocal and identity formulations of this forcing claim.
The local module assembles these targets, their equivalences, and the corresponding refutations as part of the native-cost uniqueness blocker stack.
proof idea
Term-mode reduction in three steps. Assume the reciprocal target. Apply the forward direction of the in-module equivalence ..._iff_identity_forces_two to rewrite it as the identity-forces-two target. Discharge that assumption by the already-proved refutation of the identity-forces-two target. No new analytic work: pure transport of a prior negative result across the equivalence.
why it matters
Closes one distinguished-axis reciprocal branch in the native-cost uniqueness program. Downstream, the split globalization refutation (...PrimeReciprocalWitnessGlobalizesSplitTarget_refuted) reduces directly to this lemma, so the whole reciprocal-witness split collapses with it. The native-cost uniqueness blocker certificate records related zero-calibrated factorization successes and failures; this refutation sits in the same negative ledger that keeps uniqueness from being claimed unconditionally. The universal-foundation conditional certificate consumes the broader PRC stack that includes these blockers, so the result feeds the conditional status of the foundation layer rather than a full uniqueness theorem. Relative to the forcing chain, this is bookkeeping inside cost-character uniqueness, not a T5–T8 landmark; it prevents an over-strong reciprocal globalization from being treated as proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.