toNat_ne_one_of_not_unit
plain-language theorem explainer
If a finite distinction orbit is not the multiplicative unit, its verifier natural number is not 1. Factorization and prime-coordinate arguments cite this to keep non-unit factors strictly larger than the unit orbit. The proof is the contrapositive of the native unit characterization via toNat.
Claim. Let $N$ be a finite distinction orbit. If $N$ is not the multiplicative unit (the one-step orbit), then the verifier natural number of $N$ satisfies $N_{\mathrm{toNat}} \neq 1$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with zero and successor, standing for discrete recognition steps rather than ordinary Peano arithmetic. Its verifier map toNat sends zero to 0 and successor to Nat.succ, so the orbit length is read as a Lean natural number.
In the orbit divisibility layer, the native unit predicate asserts that an orbit equals the one-step orbit. The only multiplicative unit in the finite δ-orbit is that one-step object. The characterization theorem states that an orbit is a unit if and only if its verifier natural equals 1.
This module builds prime-coordinate transforms and factorization readouts on those orbits. Non-unit factors must be excluded from the unit case before comparing orbit lengths under multiplication.
proof idea
Assume for contradiction that the verifier natural of $N$ equals 1. Rewrite the unit predicate via unit_iff_toNat_eq_one, which equates unit status with toNat = 1. The assumption then yields that $N$ is a unit, contradicting the hypothesis that $N$ is not a unit. The argument is a four-line tactic proof: intro, apply the negated unit hypothesis, rewrite by the iff, and close with the assumed equality.
why it matters
The immediate consumer is factor_left_toNat_lt_product in the same module: when $a \cdot b = N$ with both factors nonzero and $b$ non-unit, the left factor's verifier natural is strictly smaller than that of $N$. That strict decrease needs non-unit factors to have toNat ≠ 1 so multiplication by $b$ cannot leave the length unchanged.
In the Recognition foundation stack this sits under PrimitiveRecognitionCalculus factorization: prime-coordinate data and nontrivial factorization of non-prime orbits. It is a small but necessary bridge from the native unit characterization to length comparisons used when reconstructing products of prime-power coordinates. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure orbit arithmetic supporting later physical period readout.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.