Pith. sign in
theorem

PRCPrimeCalibrationForcesOrbitSuccessorIdentityTarget_refuted

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

plain-language theorem explainer

Prime calibration of a ratio character does not force identity orientation to stay fixed under one successor step on every nonzero orbit. Anyone tracking native-cost uniqueness blockers or the PRC foundation certificate chain would cite this. The proof is a short reduction: the successor-identity target implies a comparable-trace target already known to be false.

Claim. It is not the case that every ratio character $\chi$ that is prime-direction calibrated has identity orientation invariant under one successor step on every nonzero orbit direction. Equivalently, the sharper one-step successor-identity target for prime calibration is false.

background

In the Primitive Recognition Calculus, ratio characters $\chi$ assign orbit data compatible with multiplicative ratio laws. Prime-direction calibration pins how $\chi$ behaves on prime generators. The successor-identity target asks something sharper: after one successor step on any nonzero orbit direction, identity orientation should be preserved.

That target is the Prop $\forall\chi,;\mathrm{ratio\ character}(\chi)\to\mathrm{prime\ calibrated}(\chi)\to\mathrm{identity\ respects\ successor}(\chi)$. A related, weaker-looking demand is that prime calibration force identity to respect comparable additive traces. Upstream, the successor-identity target already implies that comparable-trace target by applying the one-step successor hypothesis pointwise to each character.

The comparable-trace target itself has been refuted by reduction to a still coarser trace-coherence target. The present result sits in the native-cost uniqueness module, where such forced-identity claims are systematically tested and blocked.

proof idea

Term-mode reductio. Assume the successor-identity target. Apply the upstream implication that any such target yields the prime-identity comparable-trace target (by specializing the successor step to each calibrated character). Feed that derived target into the already-proved refutation of the comparable-trace target. Contradiction, so the successor-identity target is false. No new orbit arithmetic is performed here; the work is pure target chaining.

why it matters

This closes one of the sharper forced-identity routes that would have made native cost uniqueness fall out of prime calibration alone. Downstream, the orbit-successor-transport target is refuted by reducing to this result, and the native-cost uniqueness blocker certificate records the pattern of which factorization and calibration targets survive versus fail. The universal foundation conditional certificate also sits on this blocker stack.

In Recognition Science terms, the J-cost uniqueness story (T5) and the Recognition Composition Law need a cost that is forced, not merely postulated. Refuting over-strong successor-identity claims prevents a false shortcut: prime calibration plus multiplicative character laws do not automatically supply the missing additive-trace compatibility. The open path remains the zero-calibrated factorization side of the blocker certificate, not this identity-under-successor route.

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