PRCPrimeCalibrationForcesPrimeFloorIdentityExtendsSuccessorStepTarget_of_successor_transport
plain-language theorem explainer
If prime-direction calibration forces successor transport above the self-reciprocal unit floor, then the forward half follows: prime-floor identity extends along successor steps. Native-cost uniqueness and the universal-foundation certificate cite this projection. Proof is a one-line first-component extract from the transport witness.
Claim. Assume that every ratio-orbit character $\chi$ that is a PRC ratio character and prime-direction calibrated satisfies prime-floor orbit-identity successor transport. Then every such $\chi$ satisfies the forward half: prime-floor orbit identity extends along successor steps.
background
In the Primitive Recognition Calculus, cost uniqueness is attacked through ratio-orbit characters $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$. A character is prime-direction calibrated when its action on prime axes matches the native calibration; the prime floor is the self-reciprocal unit orbit, the base of the ladder above which transport is forced.
The corrected successor-transport target (after the reciprocal-character check) asserts that prime calibration forces successor transport above that unit floor, not additive escape from the unit orbit. That target packages a pair: identity extends along successor steps, and identity contracts along them. The present declaration isolates the forward (extends) half of that pair as its own named proposition.
Local setting is native-cost uniqueness in PRC: characters whose doubled-trace data match a cost functional must be pinned by prime-floor identity transport before the J-cost can be forced unique.
proof idea
One-line projection. Introduce the character $\chi$ together with the ratio-character and prime-calibration hypotheses. Apply the assumed successor-transport target at $(\chi, h_\chi, h_{\mathrm{prime}})$; the resulting witness is a pair whose first component is exactly the extends-successor-step statement. Return that component with exact ... .1.
why it matters
Closes the forward half of the corrected prime-floor successor target so the paired theorem can assemble both extends and contracts halves from a single transport hypothesis. Downstream, that pair feeds prc_native_cost_uniqueness_blocker_certificate, which packages the zero-calibrated factorization and signed-admissible refutation legs of native-cost uniqueness. The same chain is referenced by prc_universal_foundation_conditional_certificate in UniversalFoundation.
In the broader RS forcing chain this is scaffolding under T5 (J-uniqueness): native cost must be the unique character-compatible cost before $J(x)=\cosh(\log x)-1$ can be forced. No open sorry remains here; the residual obligation is to discharge the transport hypothesis itself upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.