one_toNat
plain-language theorem explainer
The multiplicative unit of the distinction-orbit monoid evaluates to the ordinary natural number 1 under the verifier map. Anyone working in orbit arithmetic, residue periods, or prime-coordinate factorization cites this as the base case that keeps Nat-side identities aligned with orbit-side ones. The proof is pure definitional equality (rfl).
Claim. If $1_{\mathrm{orb}}$ denotes the multiplicative identity of the distinction-orbit monoid and $\mathrm{toNat}$ is the verifier embedding into ordinary naturals, then $\mathrm{toNat}(1_{\mathrm{orb}}) = 1$.
background
Distinction orbits are the native carriers of Primitive Recognition Calculus: a Peano-style type with zero and successor, equipped with monoid operations that mirror ordinary multiplication on the verifier side. The map toNat (from Orbit, paralleling ArithmeticFromLogic) reads an orbit as a Lean natural by counting successors: zero maps to 0 and each successor increments.
The constant one is the monoid unit in that orbit arithmetic (imported via OrbitArithmetic). It is definitionally the successor of zero, so its verifier image is the ordinary 1. The surrounding module develops divisibility, units, and nontrivial factorizations on orbits; this identity is the bridge that lets Nat lemmas about 1 transfer without extra conversion lemmas.
Upstream, both LogicNat and DistinctionNat expose the same recursive toNat shape ("read off the iteration count" / "verifier representation of the orbit as Lean Nat"), so the unit case is forced once one is built from a single successor.
proof idea
One-line definitional proof: rfl. Unfolding one and toNat yields Nat.succ 0 on the left and 1 on the right, which are definitionally equal in Lean. Marked @[simp] so downstream tactics discharge the unit case automatically.
why it matters
This is the base-case simp fact for the entire orbit-factorization stack. Downstream it appears in orbitPow_toNat (power of the empty exponent is the unit, hence 1), eulerPeriod_returns_one (Euler's theorem in the residue layer: a unit residue to the Euler exponent returns to the identity residue, rewritten via one_toNat), and primeCoordinateProduct_toNat_ne_zero (empty coordinate product is the unit, whose Nat image is nonzero).
It also feeds coordinate uniqueness (coordinateFactorization_eq_factorization_product), even-period-gap factorization witnesses, and prime-coordinate transforms that reconstruct Nat products from orbit data. In the Recognition foundation this keeps the δ-residue / period spectrum layer honest against ordinary arithmetic, which is prerequisite scaffolding for later forcing-chain material that needs clean divisibility and period existence on orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.