Pith. sign in
theorem

PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget_refuted

proved
show as:
module
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness
domain
Foundation
line
12971 · github
papers citing
none yet

plain-language theorem explainer

The distinguished-axis converse half of reciprocal globalization is false: prime-direction calibration need not push the orbit-2 prime axis onto the reciprocal branch whenever some native prime axis is reciprocal. Native-cost uniqueness and universal-foundation certificate authors cite this as a closed negative. The proof is a one-line reduction through an iff to the already-refuted identity-branch twin.

Claim. It is false that every ratio-orbit character $\chi$ which is a PRC ratio character and is prime-direction calibrated must send the orbit-$2$ prime axis to the reciprocal branch whenever any native prime axis of $\chi$ is reciprocal-oriented.

background

In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits encoding how multiplicative structure is read. Prime-direction calibration fixes the orientation of distinguished prime axes. Each such axis may sit on an identity branch or a reciprocal branch.

The target proposition asserts a converse globalization for the reciprocal side: if calibration is in force and any native prime axis is reciprocal, then the orbit-$2$ prime axis is forced reciprocal as well. Its identity-branch twin is the same claim with identity in place of reciprocal.

An upstream iff identifies the two targets. The identity twin is already refuted by reduction to a pair-product cost-consistency failure. The present result is the reciprocal half of that negative.

proof idea

Term-mode proof. Assume the reciprocal target. Apply the forward direction of the iff equating the reciprocal target with the identity target, obtaining the identity target as a hypothesis. Discharge by the already-proved refutation of the identity target. No new arithmetic is performed; the work is pure logical transport along the equivalence.

why it matters

Native cost uniqueness in PRC needs a clean map of which globalization routes survive. This closes the reciprocal distinguished-axis converse as a dead end, matching the earlier identity-side refutation. Downstream it is consumed by the native-cost uniqueness blocker certificate and, through that stack, by the conditional universal-foundation certificate.

In the broader Recognition forcing chain the point is local bookkeeping rather than a T5--T8 landmark: J-uniqueness and $\phi$ still sit upstream. The lemma prevents a false positive path in which reciprocal calibration alone would pin the doubled-trace cost character. Open scaffolding around signed admissible factorization remains separate; this only kills one reciprocal globalization claim.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.