PRCCharacterPrimeFloorOrbitIdentityExtendsSuccessorStep_of_local_adjacent_nomix
plain-language theorem explainer
Above the unit floor, identity orientation of a ratio-orbit character propagates one successor step whenever every nonunit orbit is locally identity-or-reciprocal and adjacent steps never mix those two orientations. Cost-uniqueness arguments cite it to lock the identity branch along the prime floor. The proof is a short case split: local orientation on the successor plus the no-mix law kills the reciprocal alternative.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose every nonzero nonunit distinction orbit is locally oriented (identity or reciprocal under $\chi$), and no adjacent pair of nonzero nonunit orbits mixes identity on one side with reciprocal on the other. Then for every nonzero nonunit $p$, if $\chi$ is identity-oriented at $p$, it is identity-oriented at the successor of $p$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). The native unit is the one-step orbit; everything else nonzero is nonunit. Ratio orbits package a signed numerator over a nonzero distinction denominator and are the domain of characters $\chi$.
Local orientation says each nonzero nonunit orbit is either identity-directed or reciprocal-directed under $\chi$ (the nonprime analogue of the already-proved local-prime alternative). The prime-floor no-adjacent-mixed law forbids identity on $p$ paired with reciprocal on $\mathrm{succ},p$, and the swapped mix.
The target property is one-step forward identity transport above the unit floor. The unit orbit is self-reciprocal, so transport is deliberately not forced out of $1$; that would exclude the globally reciprocal character branch. Successor lemmas already give $\mathrm{succ},p\neq 0$ and that nonzero nonunit $p$ has nonunit successor.
proof idea
Term-mode proof by introduction of $p$, nonzero, nonunit, and identity at $p$. First apply orbit_succ_not_unit_of_nonzero_not_unit so the successor is nonunit. Local orientation on that successor yields a disjunction: identity or reciprocal. The identity branch is the goal. The reciprocal branch is eliminated by False.elim from the first conjunct of the no-mix hypothesis at $p$, which forbids identity at $p$ together with reciprocal at $\mathrm{succ},p$.
why it matters
This is the forward half of prime-floor identity transport for PRC characters. The immediate parent packages it with the backward step into full successor transport under the same local-orientation and no-mix hypotheses. That transport feeds the native-cost uniqueness blocker certificate, which records the zero-calibrated factorization target and the refutation of the signed-admissible alternative.
In the broader Recognition stack, character uniqueness for the native cost is the bridge from the Recognition Composition Law and $J$-cost uniqueness (forcing chain T5) to a single admissible cost on ratio orbits. Keeping identity coherent along the floor, while still allowing a global reciprocal branch at the unit, is exactly the bookkeeping needed so the cost functional does not split into mixed-orientation pathologies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.