one
plain-language theorem explainer
Defines the multiplicative unit in the base-neutral orbit of repeated distinction: the successor of zero. Orbit-arithmetic lemmas (unit laws, divisibility, primes) cite it as the identity element. The body is a one-line constructor application of successor to zero.
Claim. Let $1$ denote the multiplicative unit in the finite orbit of repeated distinction. Set $1 := S(0)$, where $S$ is the successor constructor on that orbit type.
background
DistinctionNat is the inductive type of base-neutral finite orbits of repeated distinction (K2.12): constructors zero and succ. It is the carrier for primitive recognition orbit arithmetic, imported from Orbit and built on the same Peano-style generator pattern as LogicNat.
Successor is one more application of the generator: on LogicNat it is the step constructor; here the same idea lifts to DistinctionNat via its own succ. The multiplicative structure on orbits treats this unit as the identity for orbit multiplication and as the trivial divisor in the divisibility relation developed in the same module.
proof idea
Pure definitional abbreviation: the unit is the term succ zero on DistinctionNat. No lemmas or tactics; the constructors supply the value directly.
why it matters
Supplies the multiplicative identity for orbit arithmetic in PrimitiveRecognitionCalculus. Sibling results (one_toNat, one_ne_zero, mul_one_eq, one_mul_eq, divides, unit, primeOrbit) build unit laws and factorization on top of it. In the Recognition foundation this is the orbit-level analogue of $1$ before divisibility and prime-orbit structure feed higher forcing and ladder constructions; it is scaffolding for the arithmetic side of the primitive recognition calculus rather than a forcing-chain step (T0–T8) itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.