toNat_zero
plain-language theorem explainer
The zero distinction-orbit is sent to the natural number 0 by the verifier representation map. Anyone simplifying arithmetic or integer recovery lemmas on the orbit carrier cites this. The proof is pure definitional reflexivity from the recursive clause of the map.
Claim. Under the verifier representation of distinction-orbits as ordinary natural numbers, the zero orbit is mapped to $0$.
background
In the primitive recognition calculus, a distinction-orbit (DistinctionNat) is the free inductive carrier generated by a zero position and a successor step. It is the orbit of iterated recognition steps starting from the identity distinction.
The verifier map toNat reads that orbit as a Lean Nat by the obvious recursion: zero goes to $0$, and successor adds one. The dual construction ofNat rebuilds an orbit from a verifier natural. Parallel maps exist on the logic-native natural numbers (LogicNat) in ArithmeticFromLogic, with the same zero clause.
This module sits in the foundation layer that recovers ordinary arithmetic from recognition structure before integers and ordered realizations are built.
proof idea
One-line wrapper: rfl. By the defining equation of the verifier map, the zero constructor is definitionally equal to $0$, so the goal closes by reflexivity. Marked @[simp] for automatic rewriting.
why it matters
Base simp fact for every recovery theorem that compares orbit arithmetic to ordinary Nat arithmetic. Downstream it is rewritten in the addition and multiplication recovery proofs (toNat_add, toNat_mul), in the integer carrier lemmas (toInt_zero, toInt_one, toInt_fromInt), and in the ordered realization of naturals. Without the zero clause, the inductive steps that identify logic-native and verifier arithmetic cannot fire. It is scaffolding for the arithmetic-from-logic bridge that later supports factorization coordinates and the broader forcing chain, not a physics claim by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.