toNat_one
plain-language theorem explainer
The iteration-count map from the logic-forced natural-number carrier sends the unit to ordinary 1. Anyone packaging the semiring isomorphism between that carrier and Lean's ℕ cites this fact as the unit clause. The proof is a one-line definitional equality (rfl): under the standard OfNat reading, the unit is one step from identity, which counts as 1.
Claim. Let $L$ be the logic-forced natural-number carrier (identity and step). The iteration-count map $\tau: L\to\mathbb{N}$ satisfies $\tau(1)=1$.
background
The carrier LogicNat is the free orbit forced by the Law of Logic: identity is the zero-cost element (multiplicative identity of the orbit), and step is one further generator iteration. Its forward map toNat reads the iteration count: identity maps to 0, and step n maps to the successor of the count of n.
This module certifies that distinction forces a full semiring, not merely a tower. The certificate structure packages, for any two strict realizations, a unique bijective map that preserves 0, 1, addition, and multiplication, with forced object canonically $(\mathbb{N},0,1,+,\times)$.
Unit preservation is the missing one-point clause once zero, successor, and the arithmetic operations are already aligned with Lean's Nat.
proof idea
Pure term proof by rfl. With the usual OfNat instance, the numeral 1 on the forced carrier is step identity. Unfolding the iteration-count map gives Nat.succ (toNat identity) = Nat.succ 0 = 1, which is definitionally equal to the right-hand side. No lemmas are invoked.
why it matters
Direct input to forcedArithmeticIsNat, the packaging definition whose doc-comment states "The forced arithmetic is ℕ." That record fills map_one with this theorem alongside the zero, add, and mul clauses of the same isomorphism.
It sits in the UniversalForcing / ForcedSemiring foundation layer: the capstone that distinction forces the carrier isomorphic to Lean's naturals as a $(0,1,+,\times)$-structure, "with no base, no positional notation, and no arithmetic axioms posited." On the strict path the cross-realization forcing map is the identity; the non-trivial content is the preservation and uniqueness package this unit fact completes.
No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.