PRCCharacterOrbitIdentityRespectsSuccessorStep
plain-language theorem explainer
Packages the one-step law that identity orientation of a ratio-orbit character is invariant under successor on every nonzero distinction direction. Native-cost uniqueness and prime-calibration arguments cite it as the pre-primality step law. It is a Prop definition: a biconditional schema, not a proved theorem.
Claim. A map $\chi$ on rational orbits respects successor identity orientation when, for every nonzero distinction direction $p$, $\chi$ is identity-oriented at $p$ if and only if 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), and a RatioOrbit is an integer numerator over a nonzero distinction denominator. Characters here are maps $\chi$ on rational orbits used to build native cost from orientation data.
Identity orientation on a nonzero orbit direction means the character treats that direction as the canonical identity event (the J-cost minimum at state $1$). The successor operation is one more application of the distinction generator.
This module develops uniqueness of the native cost functional. The present definition isolates the weakest one-step invariance of identity orientation along the $\delta$-orbit, before any primality hypothesis is imposed.
proof idea
Definitional packaging only. The body is the universal biconditional: for every nonzero $p$, identity orientation of $\chi$ at $p$ is equivalent to identity orientation at $\mathrm{succ}(p)$, using the lemma that successors of nonzero distinction values remain nonzero. No tactics or lemmas are applied beyond writing that Prop.
why it matters
This is the pre-primality one-step law in the native-cost uniqueness chain. Downstream, it is the hypothesis that lifts identity at one to identity on every nonzero orbit direction, and conversely collapses any identity direction back to the unit. Transport of identity under successor implies this law by splitting the two directions of the biconditional.
It also feeds the comparable-trace prime-identity law and appears inside the Pass-25 blocker certificate that splits remaining uniqueness gaps into exact Lean targets. The sharper open target is that prime calibration of a ratio character should force this successor-identity invariance on every nonzero orbit direction, tying the step law to the J-uniqueness and self-similar fixed-point forcing (T5–T6) once cost is recovered from character data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.