one_ne_zero
plain-language theorem explainer
In the orbit naturals of the primitive recognition calculus, the unit is distinct from zero. Factorization, prime-coordinate, linking-vanishing, and ledger-floor arguments all cite this nontriviality fact. The proof is a one-line reduction to the Peano axiom that zero is never a successor.
Claim. In the orbit naturals, the unit satisfies $1 \neq 0$ (equivalently, $\mathrm{succ}(0) \neq 0$).
background
The module builds divisibility arithmetic on orbit naturals (the distinction-counting type underlying the primitive recognition calculus). Constants zero and one are the base point and its first successor; siblings include multiplication laws, the divides relation, units, and prime orbits.
Upstream, Peano P1 / R8 states that zero is never a successor: for every $n$, $\mathrm{zero} \neq \mathrm{succ}, n$. The ArithmeticFromLogic form phrases this as "the identity is distinguishable from any iterate of the generator"; the Orbit form is the same fact on DistinctionNat. The present claim is the special case at the unit.
proof idea
Term-mode contradiction. Introduce an equality hypothesis $1 = 0$, symmetrize to $0 = 1$, and discharge by zero_ne_succ at zero: since one is the successor of zero, the hypothesis is exactly $\mathrm{zero} = \mathrm{succ},\mathrm{zero}$, which Peano P1 / R8 forbids.
why it matters
Nontriviality of the orbit monoid is a load-bearing primitive: forty downstream uses. It supplies exponent_nonzero for prime-power coordinates in the factorization pipeline, underwrites low-dimensional linking non-detection (not_detects_zero, not_detects_one), appears in the orthogonal-hyperplane isometry for high-dimensional linking vanishing, and supports ledger-to-floor surjectivity and arc-complement acyclicity. Without $1 \neq 0$, prime orbits and the recognition ladder cannot separate the unit from the empty distinction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.