PRCPrimeCalibrationForcesPrimeFloorIdentityExtendsSuccessorStepTarget
plain-language theorem explainer
Names the forward half of the corrected prime-floor successor target: every prime-direction-calibrated ratio character must extend orbit-direction identity one successor step above the unit floor. Cited by the native-cost uniqueness blocker certificate and the universal-foundation open-target ledger. Pure Prop packaging; no proof content.
Claim. Every map $\chi$ on rational orbits that is a ratio character (unit-preserving and multiplicative up to cross-equivalence) and whose generated cost matches canonical $J$-cost on every prime direction also satisfies one-step forward identity transport: if $\chi$ acts as the identity on the orbit direction of $p$ (with $p$ nonzero and non-unit), then it acts as the identity on the successor orbit direction.
background
In the Primitive Recognition Calculus, costs are recovered from ratio characters via a d'Alembert-style factorization. A PRCRatioCharacter is a map $\chi$ on RatioOrbit (integer numerator over nonzero orbit denominator) that fixes the unit orbit and is multiplicative, both up to cross-equivalence rather than definitional equality, so the statement stays quotient-native.
Prime-direction calibration asks that the cost generated from $\chi$ agree with the canonical $J$-cost on every prime orbit direction. Separately, the prime-floor identity-extension property is the forward one-step transport rule above the unit floor: the unit orbit is self-reciprocal, so forcing transport out of $1$ would wrongly kill the globally reciprocal character branch. The present definition packages the claim that calibration implies that extension property.
Local setting is native-cost uniqueness: which characters, once calibrated on primes, are forced toward the unique PRC cost surface.
proof idea
Definitional Prop abbreviation only. The body is the universal quantification over maps $\chi$, assuming the ratio-character axioms and prime-direction calibration, and concluding the successor-step identity-extension predicate. No tactics, no lemmas applied at this site; downstream theorems either derive the target from a stronger successor-transport hypothesis or refute it outright.
why it matters
This is the forward half of the corrected prime-floor successor target in the native-cost uniqueness program. It feeds the split pair target (forward and backward halves), the blocker certificate that records exactly which uniqueness routes remain open or closed, and the universal-foundation open-target ledger.
Downstream, the target is discharged from a stronger successor-transport hypothesis by projecting the first conjunct, and is separately refuted: the two-adic axis-twist character is prime-calibrated yet fails the extension property. That refutation is the scientifically useful outcome: prime calibration alone does not force one-step identity transport above the unit floor, so uniqueness proofs must not route through this claim.
Relative to the forcing chain, this sits upstream of any appeal to $J$-uniqueness (T5) via character factorization; it prunes a false forcing path rather than establishing a positive landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.