divides_one_iff_unit
plain-language theorem explainer
On the finite distinction orbit, an element divides the multiplicative identity if and only if it is the unit (the one-step orbit). Anyone building native prime factorization or the orbit-divisibility certificate cites this. The proof rewrites both sides to ordinary Nat statements and applies Nat.dvd_one.
Claim. For every finite distinction-orbit position $a$, $a$ divides the one-step orbit if and only if $a$ is a multiplicative unit (equivalently $a$ equals the one-step orbit).
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive copy of the naturals used as the native carrier for orbit arithmetic (K2.12). Multiplication and the one-step orbit live on this carrier.
Native divisibility is existential: $a$ divides $b$ when there exists an orbit position $k$ with $a \cdot k = b$. The native unit predicate is equality with the one-step orbit; the module doc states that in the finite $\delta$-orbit the only multiplicative unit is that one-step position.
Two display lemmas bridge the native layer to Mathlib: divisibility on DistinctionNat is equivalent to ordinary Nat divisibility of the underlying toNat values, and unit-hood is equivalent to toNat = 1. The identity orbit has toNat = 1.
proof idea
Term-mode rewrite chain. Rewrite the left side with divides_iff_toNat_dvd, the right side with unit_iff_toNat_eq_one, and the identity with one_toNat. The goal collapses to the Mathlib fact Nat.dvd_one (only $1$ divides $1$ in $\mathbb{N}$), which finishes the proof.
why it matters
This is a standard unit characterization needed to close the native divisibility API. It is consumed by orbit_divisibility_certificate, whose doc-comment states that "the native orbit divisibility surface is closed." That certificate packages display, reflexivity, and related laws so later foundation work can treat orbit divisibility as a finished interface rather than an open stub.
In the broader Recognition stack this sits in Primitive Recognition Calculus: arithmetic on finite distinction orbits that underpins later forcing and ladder constructions. It does not itself invoke T5–T8 or the RCL; it is infrastructure those layers rely on when they need clean factorization language on the orbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.