divMod_toNat
plain-language theorem explainer
Euclidean quotient and remainder on distinction orbits agree with ordinary natural division and modulus after the verifier embedding. Anyone certifying δ-only arithmetic on the orbit surface cites this transport. The proof unfolds the fuelled division routine, rules out a zero divisor image by injectivity of the Nat map, and finishes with omega.
Claim. For distinction-orbit naturals $n,d$ with $d\neq 0$, writing $(q,r)=\mathrm{divMod}(n,d)$, the verifier embedding satisfies $q_{\mathbb{N}}=n_{\mathbb{N}}/d_{\mathbb{N}}$ and $r_{\mathbb{N}}=n_{\mathbb{N}}\bmod d_{\mathbb{N}}$.
background
DistinctionNat is the inductive type of finite orbits of repeated distinction (K2.12): constructors zero and succ. The verifier map toNat sends each orbit position to its iteration count in Lean Nat, with toNat(zero)=0. Injectivity of that map (toNat_inj) and the simp fact toNat_zero are the only arithmetic facts needed about the embedding.
This module builds Euclidean operations natively on those orbits (fuelled divMod, quotient, remainder, later gcd) so that arithmetic stays on the δ-only surface. The verifier Nat layer is the bridge that lets standard / and % certify the orbit operations without importing Mathlib division into the recognition calculus itself.
The immediate upstream engine is the auxiliary lemma divModFuel_toNat_aux, which inducts on fuel and already states the same two equalities for the recursive implementation.
proof idea
Unfold divMod to expose the fuelled implementation, then apply divModFuel_toNat_aux. The first obligation is that the divisor's Nat image is nonzero: if toNat(d)=0, injectivity plus toNat_zero forces d=zero, contradicting the hypothesis. The second obligation is a trivial fuel bound discharged by omega. The auxiliary lemma then returns both equalities at once.
why it matters
This is the display bridge for the closed δ-only Euclidean orbit surface. The package theorem orbit_euclidean_certificate records it as divmod_display; the one-line projections quotient_toNat and remainder_toNat extract its two conjuncts. Together with the remainder bound and the reconstruction identity quotient·divisor+remainder=n, it completes native Euclidean division on distinction orbits, which then feeds signed-rational normalization by native orbit GCD. In the Recognition foundation this keeps arithmetic inside the primitive recognition calculus rather than smuggling Mathlib Nat operations into the δ-layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.