PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget
plain-language theorem explainer
Defines the corrected prime-floor successor target as the conjunction of its forward (extends) and backward (contracts) one-step halves. Anyone tracking native-cost uniqueness blockers cites this as the split form of the prime-calibration obligation on identity transport along successor steps. The body is a pure Prop abbreviation: no proof, only pairing of the two directional targets.
Claim. The prime-floor identity successor-step pair target is the conjunction of: (i) every ratio-orbit character that is prime-direction calibrated extends prime-floor orbit identity one successor step forward, and (ii) every such character contracts prime-floor orbit identity one successor step backward.
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio-orbit characters are maps $\chi$ on ratio orbits that encode admissible cost/trace data. Prime-direction calibration is the hypothesis that $\chi$ is already fixed on prime axes. The corrected prime-floor successor problem asks whether that calibration forces identity of the character with the prime-floor orbit identity not only on primes but after one successor step along nonunit orbits.
The module splits that obligation into a forward half (extends successor step) and a backward half (contracts successor step). Each half is a universal statement: for every ratio character that is prime-direction calibrated, the corresponding one-step identity transport property holds. This definition packages those two halves as a single Prop so later certificates and iff bridges can name one object.
Local setting is the Pass-25 blocker decomposition: native cost uniqueness is not closed, but missing mathematics is carved into exact Lean targets rather than a single opaque sorry.
proof idea
No proof. The declaration is a definitional abbreviation whose body is the conjunction of the forward successor-step target and the backward successor-step target. Both conjuncts are themselves Prop defs quantifying over ratio characters with prime-direction calibration.
why it matters
This pair target is the hub for several reduction theorems in the same module. Downstream, nonunit identity-comparable trace, nonunit orbit orientation coherence, and orbit-product no-mixed-orientation targets are each proved equivalent to this pair (via dedicated iff theorems and one-direction transport lemmas). The native-cost uniqueness blocker certificate records the open obligations in this split form, so discharging the pair would collapse a large block of the uniqueness ladder.
In framework terms the target sits under J-cost uniqueness and character/trace matching for the Recognition Composition Law side of the forcing chain: prime calibration is meant to pin the discrete ladder structure that later feeds mass and coupling normalizations. It does not yet prove uniqueness; it names the exact successor-step identity gap that still blocks closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.