PRCCharacterOrbitIdentityContractsSuccessorStep
plain-language theorem explainer
Backward one-step law for identity orientation: if a ratio-orbit character is identity-oriented at the successor of a nonzero distinction count, then it is identity-oriented at that count. Used when packaging successor transport for trace coherence of native cost characters. Pure Prop definition: a universal implication over nonzero distinction-naturals, not a proved theorem.
Claim. For a map $\chi$ from rational orbits to rational orbits, and for every nonzero distinction-natural $p$: if $\chi$ has identity orientation on the orbit direction of $\mathrm{succ}(p)$, then $\chi$ has identity orientation on the orbit direction of $p$.
background
In the Primitive Recognition Calculus, distinction-naturals are the base-neutral finite orbits of repeated distinction (zero and successor). A rational orbit is an integer numerator over a nonzero distinction-natural denominator. Characters here are maps $\chi$ on rational orbits; identity orientation on a nonzero orbit direction means the character acts as the identity direction law at that step (the sibling predicate named in the body).
The local module builds native cost uniqueness from character and doubled-trace structure. Successor on distinction-naturals is the generator step (one more application of the distinction generator). The lemma that the successor of any distinction-natural is nonzero supplies the side condition needed to talk about identity orientation at $\mathrm{succ}(p)$.
This definition isolates the backward half of one-step successor transport: identity orientation at the next step contracts to the current nonzero step.
proof idea
Definitional packaging only. The body is the Prop $\forall p\neq 0,;\mathrm{IdOrient}(\chi,\mathrm{succ}(p))\Rightarrow\mathrm{IdOrient}(\chi,p)$, using the nonzero-successor fact for the successor side condition. No tactics, no lemmas discharged here.
why it matters
Native cost uniqueness needs coherent transport of identity orientation along the distinction successor so character traces stay aligned with the cost. This predicate is the backward leg of that transport: the bundled successor-transport property is exactly the forward one-step law conjoined with this contraction law ("the successor-step transport needed for trace coherence is exactly the forward and backward one-step laws bundled together").
Downstream, additive compatibility with the $\delta$-successor implies this contraction (the of-additive-compat theorem). The same name appears in the Pass-25 native-cost-uniqueness blocker certificate, which splits unfinished uniqueness work into exact Lean targets rather than a single opaque gap. In the broader forcing picture this sits under character/cost uniqueness feeding the J-cost and RCL layer (T5), not under dimensional forcing itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.