Pith. sign in
theorem

PRCPrimeCalibrationForcesPrimeFloorIdentityContractsSuccessorStepTarget_refuted

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

plain-language theorem explainer

The candidate target that every prime-direction-calibrated ratio character has prime-floor orbit identity contracting the successor step is false. Anyone tracking native-cost uniqueness blockers or the universal-foundation certificate cites this. The proof instantiates the two-adic axis-twist character, forces the two-orbit direction to equal its reciprocal under cross-equivalence, and contradicts the non-unit reciprocal lemma.

Claim. It is not the case that every map $\chi$ from ratio orbits to ratio orbits that is a PRC ratio character and is prime-direction calibrated has the property that prime-floor orbit identity contracts the successor step for $\chi$.

background

In the Primitive Recognition Calculus, ratio orbits are rational displays built from a signed-orbit numerator and a nonzero distinction-nat denominator. Cross-equivalence crossEq is the internal rational equality: two ratio orbits match when the cross-multiplied signed orbits balance. Reciprocal sends a ratio orbit to its inverse (zero to zero).

A ratio character is a map on ratio orbits preserving the PRC multiplicative structure. Prime-direction calibration means the character acts in a controlled way on prime orbit directions. The successor-step contraction target asserts that, once calibrated, identity of the character on a prime-floor orbit forces identity one successor step earlier.

The module develops native-cost uniqueness for PRC. This declaration is the backward half of a corrected prime-floor successor target, stated as a universal claim over calibrated characters, and then refuted.

proof idea

Assume the universal target. Specialize to the two-adic axis-twist character, which is already a ratio character and is prime-direction calibrated by the two-adic branch lemma.

The target then yields successor-step contraction for that character. From the branch data one obtains direction-identity on the three-orbit (successor of the two-orbit). Contraction pushes that identity down to the two-orbit. The same branch supplies the reciprocal identity on the two-orbit direction.

Symmetry and transitivity of crossEq glue identity and reciprocal into crossEq d (recip d) for the two-orbit direction $d$. The lemma that a non-unit orbit direction is never cross-equivalent to its reciprocal closes the contradiction.

why it matters

Native-cost uniqueness in PRC needs a clean account of which prime-floor identities survive calibration. This refutation kills one natural strengthening: that calibration alone forces successor-step contraction of prime-floor identities for every ratio character.

It feeds prc_native_cost_uniqueness_blocker_certificate, which packages proved and refuted factorization targets into the uniqueness blocker certificate, and is also listed under the conditional universal-foundation certificate. In the forcing chain this sits upstream of J-uniqueness (T5) and the Recognition Composition Law: cost characters must be constrained tightly enough that only the native J-cost remains, without over-claiming contraction at every prime floor.

The result is a negative landmark: it tells the uniqueness program which successor-step target is too strong and must be replaced by a weaker, still-proved formulation.

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