PRCPrimeCalibrationForcesPrimeFloorIdentityContractsSuccessorStepTarget
plain-language theorem explainer
Names the open target that prime-direction calibration of a ratio character should force backward one-step identity transport on orbits above the unit floor. Cited by the native-cost uniqueness blocker certificate and the split successor-step pair target. Pure Prop packaging: universal quantification over characters with two hypotheses and one conclusion predicate; no proof content.
Claim. For every map $\chi$ on ratio orbits that is a ratio character and is calibrated on every native prime direction (its generated cost matches canonical $J$-cost on each prime orbit), $\chi$ satisfies backward one-step identity transport above the unit floor: whenever the successor orbit direction is an identity for $\chi$, the predecessor (non-unit, nonzero) direction is as well.
background
In the Primitive Recognition Calculus, costs are recovered from ratio-orbit characters via a d'Alembert-style factorization. A PRCRatioCharacter is a multiplicative map $\chi$ on ratio orbits (integer numerator over nonzero orbit denominator) that fixes the unit up to cross-equivalence, the quotient-native equality used throughout this module.
Prime-direction calibration means that on every prime orbit the cost built from $\chi$ agrees, again by cross-equivalence, with the canonical $J$-cost evaluated on that prime direction. The conclusion predicate is the backward half of identity transport above the unit floor: for nonzero non-unit $p$, if $\chi$ acts as the identity on the successor direction of $p$, then it acts as the identity on the direction of $p$ itself.
This definition is the contracts (backward) half of the corrected prime-floor successor target; its sibling is the extends (forward) half. Together they form the split one-step pair used by the uniqueness blocker ledger.
proof idea
Definitional packaging only: the body is the universal statement $\forall,\chi,;\mathrm{PRCRatioCharacter},\chi\to\mathrm{PrimeDirectionCalibrated},\chi\to\mathrm{ContractsSuccessorStep},\chi$. No tactics, no lemmas applied. Downstream, the pair target conjoins this with the extends half; a one-line projection theorem recovers this target from a joint successor-transport hypothesis by taking the second conjunct.
why it matters
Sits inside the native-cost uniqueness program: if prime calibration forced floor identity transport, character factorization toward unique $J$-cost would tighten. It is the second conjunct of the split one-step successor pair and appears in PRCNativeCostUniquenessBlockerCertificate, which records that uniqueness is not closed but is split into exact Lean targets.
The route is closed negatively: the companion theorem refutes this target (a calibrated two-adic axis-twist character is a counterexample). That refutation feeds PRCUniversalFoundationOpenTargets as a negative ledger entry, marking a path that cannot force the final uniqueness surface. Relative to the forcing chain, this is foundation-level cost uniqueness scaffolding around T5 $J$-uniqueness, not a derivation of $\phi$, the eight-tick octave, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.