PRCCharacterPrimeFloorOrbitIdentitySuccessorTransport_of_local_adjacent_nomix
plain-language theorem explainer
Local nonunit orientation plus a prime-floor ban on adjacent mixed identity/reciprocal orientations forces identity orientation to transport along one successor step above the unit orbit. Anyone proving prime-to-prime trace coherence or native cost uniqueness cites this bridge. The proof is a one-line pair constructor from the already-proved extend and contract lemmas.
Claim. Let $\chi$ act on rational orbits. If every nonunit orbit direction is locally either identity-oriented or reciprocal-oriented, and no adjacent nonunit pair mixes identity on one side with reciprocal on the other, then identity orientation both extends and contracts along a single $\delta$-successor step once the path is above the self-reciprocal unit orbit.
background
In the primitive recognition calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator: the discrete display on which characters act. A character $\chi$ assigns to each such orbit another orbit; orientation of a nonunit direction means $\chi$ either fixes that axis (identity) or sends it to its reciprocal.
Local nonunit orientation asserts that every nonunit direction is one or the other. The prime-floor no-adjacent-mixed law strengthens this: consecutive nonunit steps cannot flip from identity to reciprocal or vice versa. Successor transport packages the two directed consequences: identity at $p$ forces identity at $\mathrm{succ},p$ (extend), and identity at $\mathrm{succ},p$ forces identity at $p$ (contract), once above the unit orbit.
The module develops native-cost uniqueness for characters obeying the doubled-trace d'Alembert law; this layer is the exact bridge from local orientation data to prime-to-prime trace coherence.
proof idea
Term-mode pair constructor. The target is definitionally the conjunction of the extend and contract successor-step properties. Apply the already-proved lemma that local orientation plus no-adjacent-mix yields the extend half, then the twin lemma that yields the contract half, and pack the two results into the pair. No new case analysis occurs here.
why it matters
This is the one-direction half of the local-adjacent-nomix characterization of successor transport, and the workhorse used by every prime-calibration forcing theorem that concludes successor transport. Downstream, the iff form, the sharpened and local-adjacent target force lemmas, and the nonunit-coherent force lemma all invoke it directly; the native-cost uniqueness blocker certificate sits further up that chain.
In the Recognition framework it supplies the discrete transport step needed for prime-to-prime trace coherence on the character side of native cost uniqueness, sitting under the J-cost uniqueness and composition-law layer (T5 / RCL) rather than replacing it. Without this bridge, local orientation data would not reach the successor-transport target that calibration theorems demand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.