ofNat_ne_zero_of_ne_zero
plain-language theorem explainer
Nonzero Lean naturals embed under the orbit constructor to nonzero distinction-orbit positions. Anyone transporting factorization or divisibility between verifier Nats and δ-orbits cites this injectivity-at-zero fact. The proof is a four-line contradiction: apply the orbit-to-Nat map and rewrite by the known round-trip identities.
Claim. For every natural number $n$, if $n \neq 0$ then the distinction-orbit position built from $n$ is not the zero orbit.
background
DistinctionNat (K2.12) is the base-neutral finite orbit of repeated distinction: an inductive type with constructors zero and succ. It is the native carrier for orbit arithmetic in the primitive recognition calculus.
The maps toNat and ofNat mediate between Lean Nat and DistinctionNat. toNat reads off the iteration count (zero maps to 0, succ adds one). ofNat builds an orbit position from a verifier Nat (0 maps to zero, successor iterates succ). The transport theorem toNat_ofNat (K4.5) states that toNat(ofNat n) = n for every n; separately, toNat zero = 0.
This module develops divisibility and factorization on DistinctionNat, importing the orbit arithmetic layer. The present lemma is a private zero-preservation fact used when statements about nonzero factors are moved across the Nat/orbit bridge.
proof idea
Proceed by contradiction. Assume ofNat n equals zero. Apply congrArg of DistinctionNat.toNat to that equality. Rewrite the resulting Nat equality with toNat_ofNat on the left and toNat_zero on the right, obtaining n = 0. Discharge against the hypothesis n ≠ 0.
why it matters
The sole downstream consumer is nontrivialFactorization_iff_toNat, which asserts that native nontrivial factorization of an orbit position is equivalent to ordinary Nat nontrivial factorization of its toNat image (nonzero, non-unit factors whose product recovers the count). Without a guarantee that ofNat sends nonzero Nats to nonzero orbits, the nonzero-factor side of that equivalence cannot be transported cleanly.
In the Recognition foundation stack this sits inside PrimitiveRecognitionCalculus orbit arithmetic: the δ-orbit is the discrete carrier on which divisibility, units, and prime orbits are defined before later forcing-chain material (T5–T8) is attached. It is infrastructure, not a physics claim, but it closes a necessary Nat/orbit coherence gap for factorization display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.