threeOrbit_toNat
plain-language theorem explainer
The three-step distinction orbit evaluates to the natural number 3 under the verifier map. Anyone working with prime orbits, p-adic valuations of prime directions, or the native-cost uniqueness argument cites this as the arithmetic anchor for the factor 3. The proof unfolds the three-orbit constructor and rewrites once through the successor rule and the two-orbit evaluation.
Claim. Under the verifier representation that sends a finite distinction orbit to a natural number, the three-step orbit equals $3$. Equivalently, if the three-orbit is the successor of the two-orbit, then its iteration count is $\mathrm{succ}(2)=3$.
background
In the Primitive Recognition Calculus, finite orbits of repeated distinction are encoded by the inductive type DistinctionNat (K2.12): a base-neutral successor chain starting from zero. The verifier map toNat reads off the iteration count, sending zero to $0$ and successor to Nat.succ.
The two-orbit is already known to evaluate to $2$ (twoOrbit_toNat). The three-orbit is defined as one further successor of that two-orbit, so its natural-number image is forced by the successor rule on toNat. The ambient module develops native-cost uniqueness for PRC characters, where small prime orbits (2 and 3) seed prime directions and p-adic tests.
Upstream arithmetic from logic supplies the same successor identity on the parallel LogicNat type; the orbit layer mirrors that structure so that orbit primes can be compared by their toNat images.
proof idea
One short tactic proof. Unfold the definition of the three-orbit (successor of the two-orbit). Rewrite with DistinctionNat.toNat_succ, which is definitional (toNat (succ n) = Nat.succ (toNat n)), then apply the simp lemma twoOrbit_toNat (twoOrbit.toNat = 2). The goal reduces to Nat.succ 2 = 3, which closes.
why it matters
This is the arithmetic pin for every later use of the three-orbit inside native-cost uniqueness. Downstream it discharges the size hypothesis in threeOrbit_primeOrbit (primality of the three-orbit via toNat), separates three from two in threeOrbit_ne_twoOrbit, normalizes threePrimeDirection_toRat to the rational $3$, and feeds the p-adic vanishing lemma padicValRat_three_primeDirection_eq_zero_of_ne_three for prime directions other than three. It also appears in the two-adic axis-twist character non-identity check at successor-of-three.
In the broader Recognition forcing chain this is scaffolding under T5/T6 cost uniqueness: prime orbits label independent ratio directions whose characters must match the unique J-cost. Without the concrete evaluation to $3$, the prime-direction and doubled-trace arguments cannot specialize to the odd prime factor that sits beside the two-adic axis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.