PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget_of_nonunit_coherent
plain-language theorem explainer
Prime calibration that forces one coherent orientation on all nonunit ratio-orbit directions already yields the split one-step prime-floor successor pair (identity extends and contracts along successor steps). Cited by anyone closing the native-cost uniqueness blocker or the coherent↔step-pair equivalence. Proof is a pure term composition: coherence implies successor transport, which splits into the extends/contracts pair.
Claim. Assume prime calibration forces a single coherent orientation across every nonunit ratio-orbit direction, for every prime-direction-calibrated ratio character $\chi$. Then prime calibration also forces the split one-step prime-floor successor target: identity orientation both extends and contracts along successor steps on the prime floor.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ assign orientations on ratio orbits. Prime-direction calibration pins the character on prime axes. The stronger nonunit-orbit orientation coherence target asks that the same orientation rule hold on every nonunit orbit direction, not only primes; mixed product factors are then ruled out by nonunit non-self-reciprocity.
The prime-floor identity successor step-pair target is the corrected one-step form of the prime-floor successor obligation: it is the conjunction of an extends-step target and a contracts-step target. A companion transport target packages the same content as a single successor-transport statement on prime-floor identity orbits.
This module builds native-cost uniqueness blockers from such calibration targets. Upstream, coherence already implies the transport target, and transport already splits into the extends/contracts pair.
proof idea
One-line term composition of two prior theorems. First apply the lemma that nonunit-orbit orientation coherence yields the prime-floor successor-transport target (that lemma reduces to local adjacent no-mixing via local orientation extracted from global coherence). Then feed the resulting transport hypothesis into the splitter that turns successor transport into the conjunction of the identity-extends and identity-contracts one-step targets. No new case analysis.
why it matters
Closes one direction of the in-module equivalence between nonunit-orbit orientation coherence and the prime-floor identity successor step-pair, so those two blocker faces may be swapped freely. That equivalence and this implication feed the native-cost uniqueness blocker certificate, which packages zero-calibrated factorization and related refutations for the uniqueness program.
Downstream, the same material is consumed by the conditional universal-foundation certificate in UniversalFoundation (kernel, real complete ordered field, and trace-logic legs). In the broader Recognition chain this is foundation scaffolding toward unique native cost before J-uniqueness (T5) and the RCL, not a physical constant claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.