ofNat_zero
plain-language theorem explainer
The embedding of ordinary naturals into distinction-orbit positions sends 0 to the orbit zero. Anyone simplifying orbit arithmetic or proving denominators are nonzero cites this simp lemma. The proof is pure definitional equality from the recursive clause of the embedding.
Claim. The map sending a verifier natural number $n$ to a distinction-orbit position satisfies $\mathrm{ofNat}(0) = 0$, where the right-hand side is the zero position of the distinction naturals.
background
In the primitive recognition calculus, distinction naturals (DistinctionNat) are the inductive orbit positions generated from a zero and a successor. They are the carrier for discrete recognition steps before signed orbits and rational ratios are built.
The map ofNat embeds ordinary Lean naturals into these orbit positions by recursion: zero goes to orbit zero, and successor is preserved. Its doc-comment states the intent directly: "Build an orbit position from a verifier Nat." The companion map toNat runs the other way; together they form the usual round-trip isomorphism once the remaining simp lemmas are in place.
This module sits under Foundation and imports only Mathlib plus the Basic layer of the primitive recognition calculus. The local setting is the bare inductive arithmetic of orbit positions, prior to growth, signs, or ratio constructions.
proof idea
One-line definitional proof. Unfolding the recursive definition of the embedding on the zero clause yields orbit zero immediately, so rfl closes the goal. No lemmas are applied.
why it matters
The lemma is a simp normalizer for the zero case of the Nat-to-orbit embedding. Downstream, den_toNat_ne_zero uses it to show that a ratio-orbit denominator has nonzero verifier Nat: after rewriting the assumed toNat equality, ofNat_zero converts the right-hand side so that ofNat_toNat forces the denominator itself to be orbit zero, contradicting the ratio invariant.
It is also consumed in the choice-free nonnegativity-flag identity for right-multiplication by a nonzero orbit, where nonzero orbit positions are detected via their verifier Nats. Within the Recognition forcing chain this is pure scaffolding arithmetic: it keeps the discrete orbit layer coherent so later steps (eight-tick structure, ladder rungs) can treat Nat and DistinctionNat interchangeably at zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.