PRCCharacterPrimeFloorOrbitIdentitySuccessorTransport
plain-language theorem explainer
Packages the corrected successor-transport rule for a ratio-orbit character: identity orientation moves one δ-successor step both forward and backward once the path sits above the self-reciprocal unit orbit. Anyone proving prime-to-prime trace coherence or nonunit orientation coherence cites this layer. The body is pure definitional packaging: the conjunction of the extend and contract one-step properties.
Claim. For a map $\chi$ on rational orbits, the prime-floor successor-transport property asserts that identity orientation of $\chi$ extends one $\delta$-successor step forward and contracts one step backward, for every non-unit orbit above the unit floor.
background
In the primitive recognition calculus, a rational orbit is an integer numerator over a nonzero distinction-natural denominator (K4.7). A character $\chi$ acts on these orbits; identity orientation at an orbit means $\chi$ fixes the direction of that orbit rather than flipping it.
The unit orbit is self-reciprocal. Forcing identity transport out of the unit would wrongly exclude the globally reciprocal character branch, so both one-step rules are gated above the unit floor: they quantify over nonzero non-unit distinction-naturals $p$ and move identity orientation between $p$ and its successor.
The forward half says identity at $p$ implies identity at $\mathrm{succ},p$. The backward half says identity at $\mathrm{succ},p$ implies identity at $p$. Together they are the exact local layer needed for prime-to-prime trace coherence in the native-cost uniqueness development.
proof idea
Definitional packaging only. The predicate is the conjunction of the forward one-step identity-transport property (extends successor above the unit floor) and the backward one-step property (contracts successor above the unit floor). No tactics, no lemmas applied beyond naming those two components.
why it matters
This is the corrected successor-transport interface that the native-cost uniqueness stack uses to move identity orientation along the distinction-natural spine without contaminating the unit orbit. Downstream it discharges comparable-trace respect for nonunit identity, nonunit orbit-orientation coherence (when paired with local orientation), one-sided orbit-identity propagation for $\le$ and $\ge$ orderings, and the no-adjacent-mixed-orientation rule on the prime floor.
It is also equivalent, under local nonunit orientation, to the adjacent no-mix condition, so the stack can switch between the transport packaging and the local combinatorial form. In the broader Recognition framework this sits inside the PRC path toward uniqueness of the native cost (and ultimately the J-cost forced by T5), by ensuring character orientation is coherent along successive prime-floor steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.