twoOrbit_primeOrbit
plain-language theorem explainer
The two-step distinction orbit is prime in the base-neutral orbit arithmetic: its natural image is 2, which admits no nontrivial factorization. Anyone calibrating native costs or characters on prime axes cites this as the canonical prime witness at 2. The proof rewrites the primality predicate to a Nat statement and closes by the usual divisor analysis of 2.
Claim. The two-step finite distinction orbit is a prime orbit: if $N$ is its underlying natural number, then $N>1$ and whenever $N=ab$ with $a,b\in\mathbb{N}$, one of $a$ or $b$ is $1$ (equivalently $N=2$ is prime).
background
In the Primitive Recognition Calculus, finite orbits of repeated distinction are packaged as DistinctionNat: a Peano-style inductive type (zero and successor) that is base-neutral, so arithmetic facts about orbits do not depend on a preferred radix. An orbit is called prime when its underlying natural image has no nontrivial factorization; that predicate is equivalent to the usual primality of toNat of the orbit.
The object twoOrbit is the two-step orbit. Its toNat evaluation is definitionally 2. Downstream cost and character work treats 2 as the base calibration point on the native prime axes, so one needs a formal certificate that this orbit is prime in the orbit sense, not merely that 2 is prime as a bare natural.
The local module develops uniqueness and minimality of native costs built from ratio characters. Primality of the two-orbit is the seed fact that lets two-point calibration transport to every native prime direction.
proof idea
Rewrite the goal with the characterization that an orbit is prime iff its toNat is greater than 1 and has no nontrivial factor pair. The first conjunct is twoOrbit_toNat plus norm_num (so the image is 2). For the second, unpack a putative factorization $a\cdot b=\mathrm{toNat}(\mathrm{twoOrbit})$, reduce to $a\cdot b=2$, note $a\mid 2$, and apply the standard dichotomy for divisors of a prime: either $a=1$ (forbidden by the factor hypotheses) or $a=2$, which forces $b=1$ (again forbidden). The only external arithmetic fact is Nat.Prime 2 by decide.
why it matters
This is the canonical prime-orbit witness at 2. Downstream, absValueCharacter_two_cost_calibrated applies prime calibration at twoOrbit using exactly this theorem, and the minimality ledger theorem character_pair_two_calibration_forces_prime_calibration transports two-point calibration plus prime-pair product consistency to full prime-direction calibration. A large family of identity-forcing results in the same uniqueness module (prime-identity iff two-prime-identity under admissibility, branch uniformity, local orientation, etc.) thread through the same two-as-prime seed.
In the broader Recognition stack this sits under the Primitive Recognition Calculus foundation that feeds native cost uniqueness, not yet the T5–T8 forcing chain itself. It is the arithmetic hinge that makes the base ledger at 2 control the prime axes rather than treating each prime calibration as independent data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.