Pith. sign in
theorem

PRCPrimeCalibrationForcesPrimeIdentityWitnessGlobalizesNonunitTarget_refuted

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

plain-language theorem explainer

Refutes the witness-globalized prime-floor claim: prime-direction calibration of a ratio character does not force identity on one calibrated prime axis to imply identity on every nonunit orbit direction. Native-cost uniqueness certificates and the next prime-floor successor-transport refutation cite it. Proof is a short reduction through an equivalence to the already-refuted no-mixed-prime-witnesses target.

Claim. It is false that every ratio character $\chi$ which is prime-direction calibrated must satisfy: if any calibrated prime axis picks the identity map, then every nonunit orbit direction also picks the identity.

background

In the Primitive Recognition Calculus, ratio characters are maps on ratio orbits that encode admissible cost-compatible orientations. Prime-direction calibration restricts how $\chi$ acts on prime axes. The target proposition asserts a strong globalization: once any calibrated prime axis is forced to the identity, every nonunit orbit direction must likewise be identity.

That target is one packaging of the prime-floor blocker in the native-cost uniqueness development. An in-module equivalence identifies it with the no-mixed-prime-witnesses target: the two statements are interchangeable as universal claims about calibrated characters.

Upstream, the no-mixed-prime-witnesses target is already refuted, itself by reduction to a coherent-prime-orientation refutation. The present result therefore sits in a chain of equivalent blocker formulations being discharged one by one.

proof idea

Assume the witness-globalization target. Apply the forward direction of the proved equivalence with the no-mixed-prime-witnesses target to obtain that weaker-looking but equivalent claim. Discharge the assumption by invoking the already-established refutation of no-mixed-prime-witnesses. The whole argument is a three-line intro-and-exact reduction; no new analytic work appears here.

why it matters

This closes one packaging of the prime-floor blocker inside PRC native-cost uniqueness. Downstream, the prime-floor successor-transport target is refuted by the same pattern, quoting this theorem through its own equivalence. The native-cost uniqueness blocker certificate aggregates such proved and refuted targets into a single certificate object used by the broader foundation stack.

In the Recognition Science forcing picture, native cost uniqueness is the bridge from the Recognition Composition Law and J-uniqueness (T5) toward a unique cost functional on ratio data. Clearing false globalization claims prevents over-strong prime-axis constraints from being smuggled into that uniqueness argument. The universal-foundation conditional certificate also depends on this module's certificate layer, so the refutation feeds the conditional foundation story rather than a free-standing physics claim.

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