PRCCharacterOrbitIdentityExtendsSuccessorStep
plain-language theorem explainer
Packages the forward one-step successor law: if a ratio-orbit character is identity-oriented at a nonzero distinction direction p, it stays identity-oriented at succ(p). Cited by anyone assembling successor transport or native-cost uniqueness certificates. The body is a pure Prop definition, not a proved theorem.
Claim. A map $\chi$ on rational orbits satisfies the forward successor law when, for every nonzero distinction direction $p$, identity orientation of $\chi$ at $p$ implies identity orientation of $\chi$ at the successor of $p$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (Peano-style: zero and successor). A RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction denominator.
Characters here are maps $\chi$ on ratio orbits. Identity orientation at a nonzero direction means the character aligns with the canonical identity event (the J-cost minimum at state $x=1$). The local module develops native-cost uniqueness: showing the cost extracted from such characters is forced to the unique J-cost shape.
Upstream, successor is one more application of the generator; the one-step trace extension by $\delta$ is the syntactic counterpart. The nonzero-successor lemma orbit_succ_ne_zero keeps the successor direction admissible.
proof idea
Definitional Prop, not a proof. The body quantifies over nonzero distinction directions $p$ and states the implication: identity orientation of $\chi$ at $p$ yields identity orientation at $\mathrm{succ}(p)$, with the successor nonzero witness supplied by orbit_succ_ne_zero. Discharge is deferred to theorems such as the additive-compatibility implication below.
why it matters
This is the forward half of successor transport. Downstream, PRCCharacterOrbitIdentitySuccessorTransport bundles it with the backward contraction law; that bundle is the exact coherence condition needed for trace-level identity orientation under $\delta$-steps.
The theorem ..._of_additive_compat shows additive compatibility with the $\delta$-successor on nonzero orbits implies this forward law, so the Prop is the clean target for that reduction. It also appears in PRCNativeCostUniquenessBlockerCertificate, the Pass-25 split of remaining native-cost uniqueness obligations into exact Lean targets.
In the broader RS chain this sits under T5 J-uniqueness: native cost must match $J(x)=(x+x^{-1})/2-1$, and character orientation along the distinction orbit is part of forcing that match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.