PRCCharacterPrimeFloorOrbitIdentityContractsSuccessorStep_of_local_adjacent_nomix
plain-language theorem explainer
Under local identity-or-reciprocal orientation of nonunit orbits and the prime-floor ban on adjacent mixed orientations, identity orientation of a successor forces identity orientation of the predecessor. Anyone assembling one-step identity transport for PRC characters above the unit floor cites this. The argument is a two-case split on local orientation; the reciprocal case is killed by the no-mix law.
Claim. Let $\chi$ act on rational orbits. Assume every nonunit orbit direction is locally either identity-oriented or reciprocal-oriented, and that adjacent nonunit steps never mix identity on one side with reciprocal on the other. Then identity orientation contracts one successor step above the unit floor: if $\mathrm{succ}(p)$ is identity-oriented under $\chi$, so is $p$.
background
In the primitive recognition calculus, a rational orbit is an integer numerator over a nonzero distinction-natural denominator. A character $\chi$ maps orbits to orbits; its local direction at a nonunit index $p$ is either the identity orientation or the reciprocal orientation.
Local orientation asserts that every nonunit orbit is one of those two alternatives (the nonprime analogue of the already-proved local-prime orientation dichotomy). The prime-floor no-adjacent-mixed law forbids the two cross patterns: identity at $p$ with reciprocal at $\mathrm{succ}(p)$, and reciprocal at $p$ with identity at $\mathrm{succ}(p)$.
The target property is backward one-step identity transport above the unit floor: identity orientation at $\mathrm{succ}(p)$ implies identity orientation at $p$, for every nonunit $p$ away from zero.
proof idea
Fix a nonunit $p$ and assume identity orientation at $\mathrm{succ}(p)$. Local orientation splits $p$ into identity or reciprocal. The identity branch is the desired conclusion. The reciprocal branch, paired with identity at the successor, is exactly the second forbidden mixed pattern in the no-adjacent-mixed hypothesis, so it is eliminated by contradiction. No further lemmas are needed; the proof is pure case analysis on the two supplied hypotheses.
why it matters
This is the contraction half of prime-floor identity transport. Downstream it is packaged with the matching extension step into full successor transport of identity orientation under the same local-plus-no-mix hypotheses. That transport block is then recorded in the native-cost uniqueness blocker certificate, which certifies the zero-calibrated factorization target and the refutation of the signed admissible factorization alternative. In the Recognition forcing chain this sits inside the uniqueness argument for the native cost (the J-cost side of T5), ensuring character orientation cannot flip across adjacent nonunit steps once the unit floor is cleared.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.