PRCCharacterOrbitIdentity_one_of_identity
plain-language theorem explainer
If a ratio-orbit character preserves identity orientation under successor steps, then identity at any nonzero orbit position forces identity at the unit direction. Cited when reducing composite-orbit identity transport to the generator step before primality. The proof is induction on the distinction index, walking identity backward one successor at a time until the base case p = 1.
Claim. Let $\chi$ map ratio orbits to ratio orbits and preserve identity orientation under one successor step on nonzero distinction indices. If identity orientation holds at some nonzero index $p$ (i.e. $\chi$ fixes the orbit direction of $p$ up to cross-equality), then identity orientation also holds at the unit index $1$.
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 index is the generator step. A RatioOrbit is an integer numerator over a nonzero orbit denominator.
Identity orientation at a nonzero index $p$ means the character $\chi$ fixes the corresponding orbit direction up to cross-equality: $\mathrm{crossEq}(\chi(\mathrm{orbitDirection},p),,\mathrm{orbitDirection},p)$. This is stated for arbitrary nonzero directions, not only primes, so trace transport can pass through composite positions.
The successor-step hypothesis is the one-step trace-order law: identity orientation at $p$ if and only if identity at $\mathrm{succ},p$, for every nonzero $p$. The module doc frames this as smaller than prime-to-prime transport, acting before primality is imposed. Upstream facts used here include orbit_succ_ne_zero (successors are never zero) and one_ne_zero.
proof idea
Term-mode induction on the distinction index $p$.
The zero case is immediate contradiction with the nonzero hypothesis.
On $\mathrm{succ},n$, case-split $n$. If $n=0$, then $p=1$ and the given identity hypothesis is exactly the goal. If $n=\mathrm{succ},m$, form the nonzero witness for $\mathrm{succ},m$ via orbit_succ_ne_zero, then apply the successor-step law in the backward direction: identity at $\mathrm{succ}(\mathrm{succ},m)$ yields identity at $\mathrm{succ},m$. Feed that into the inductive hypothesis to reach identity at $1$.
why it matters
Native cost uniqueness needs identity orientation to travel from an arbitrary nonzero (often composite) orbit position down to the unit generator before prime-axis arguments begin. This lemma is the pure orbit-level reduction: successor-step invariance plus one identity witness implies identity at $1$.
It feeds PRCCharacterPrimeIdentityRespectsComparableTrace_of_successor_step, which lifts the successor law to the prime-identity/comparable-trace interface used in character factorization. It is also listed among the ingredients of prc_native_cost_uniqueness_blocker_certificate, the certificate packaging zero-calibrated native-cost uniqueness targets.
In the broader Recognition stack this sits under foundation work that forces the J-cost and the unique native cost functional (T5 J-uniqueness and the Recognition Composition Law), by controlling how characters act on orbit directions before continuum or measure arguments appear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.