PRCCharacterOrbitIdentity_of_one
plain-language theorem explainer
If a ratio-orbit character preserves identity orientation under one successor step and already does so at the unit direction, then it preserves identity orientation at every nonzero orbit direction. Native-cost uniqueness arguments cite this to push the unit calibration along the full δ-orbit before primality is imposed. The proof is induction on DistinctionNat, discharging zero by the nonzero hypothesis and advancing via the successor-step biconditional.
Claim. Let $\chi$ map ratio-orbits to ratio-orbits. Suppose identity orientation of $\chi$ is invariant under one successor step on every nonzero orbit direction, and suppose $\chi$ has identity orientation at the unit direction. Then for every nonzero orbit index $r$, $\chi$ has identity orientation at the direction of $r$: the cross-equality $\chi(\mathrm{dir}(r)) \simeq \mathrm{dir}(r)$ holds.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). Nonzero indices label orbit directions; the unit is one step past zero. A RatioOrbit is an integer numerator over a nonzero orbit denominator.
Identity orientation at a nonzero direction $p$ means the character $\chi$ fixes that direction up to the ratio-orbit cross-equality: $\chi(\mathrm{dir}(p))$ matches $\mathrm{dir}(p)$. The successor-step law is the biconditional that this identity orientation at $p$ holds if and only if it holds at $\mathrm{succ}(p)$. That law is deliberately weaker than prime-to-prime transport: it acts before primality is imposed, so composite orbit positions remain available for trace transport.
The local setting is native-cost uniqueness for PRC characters: one calibrates orientation at the unit and must propagate it along the whole nonzero orbit so later prime-axis and doubled-trace comparisons stay coherent.
proof idea
Induct on the orbit index $r$. The zero case is immediate contradiction with the hypothesis $r \neq 0$.
On a successor, case-split the predecessor. If the predecessor is zero, $r$ is the unit direction and the given unit identity applies directly.
If the predecessor is itself a successor of some $m$, the inductive hypothesis supplies identity orientation at $\mathrm{succ}(m)$ (using that successors are nonzero). The forward half of the successor-step biconditional then lifts that identity one more step to $\mathrm{succ}(\mathrm{succ}(m))$, which is $r$.
why it matters
This lemma is the unit-to-all-nonzero bridge for identity orientation. Downstream, PRCCharacterPrimeIdentityRespectsComparableTrace_of_successor_step applies it so that a successor-step identity law yields prime identity that respects comparable traces: once the unit is calibrated, every nonzero (hence every prime) direction inherits identity orientation before trace comparison.
It also feeds the native-cost uniqueness blocker certificate, which packages proved factorization targets and refutations used to close the uniqueness argument for the native cost attached to PRC characters. In the broader Recognition stack this sits under the J-cost / character uniqueness thread (T5 J-uniqueness and the Recognition Composition Law background): characters that preserve orbit directions are the discrete skeleton on which the continuous cost $J$ is later matched. Without propagating identity from one along the orbit, composite and prime axes would not share a single orientation convention.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.