remainder_lt_divisor
plain-language theorem explainer
In orbit arithmetic on DistinctionNat, the remainder of n by a nonzero divisor d satisfies rem.toNat < d.toNat. Anyone citing the δ-only Euclidean certificate needs this bound. The proof reduces via remainder_toNat to Nat.mod_lt after showing d.toNat is positive from d ≠ zero.
Claim. Let $n,d$ be distinction-orbit naturals with $d \neq 0$. Writing $r$ for the orbit remainder of $n$ on division by $d$, one has $r^{\mathbb{N}} < d^{\mathbb{N}}$, where $(\cdot)^{\mathbb{N}}$ is the canonical map from distinction orbits to ordinary natural numbers.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with constructors zero and succ, carrying a decidable equality. The map toNat reads off the iteration count, sending zero to $0$ and succ to successor; toNat_zero records toNat(zero) = 0.
This module builds a Euclidean (divmod) layer on those orbits. Sibling definitions supply fuelled division, quotient, and remainder, together with display lemmas (remainder_toNat, quotient_toNat, divMod_toNat) that relate orbit operations to ordinary Nat.mod and Nat.div. The nonzero hypothesis on the divisor is required both for the remainder constructor and for the classical remainder bound.
Upstream arithmetic-from-logic supplies the same toNat pattern on LogicNat; here it is specialized to DistinctionNat so that orbit Euclidean facts can be certified by reduction to Mathlib Nat lemmas.
proof idea
Rewrite the goal with remainder_toNat so the claim becomes Nat.mod (n.toNat) (d.toNat) < d.toNat. Apply Nat.mod_lt, which needs d.toNat > 0. Prove positivity by Nat.pos_of_ne_zero: if d.toNat = 0, injectivity of toNat plus toNat_zero forces d = zero, contradicting the hypothesis hd. No orbit-specific arithmetic beyond the display lemma is used.
why it matters
Feeds orbit_euclidean_certificate as the remainder_bound field. That certificate packages the closed δ-only Euclidean orbit surface: divmod/quotient/remainder displays, this strict remainder inequality, and the reconstruction identity quotient·divisor + remainder = dividend, including signed-rational normalization by native orbit GCD.
In the Primitive Recognition Calculus stack, Euclidean structure on distinction orbits is the arithmetic substrate beneath later forcing and ladder constructions. The bound is the orbit-native form of the classical remainder inequality; without it the certificate cannot assert a well-formed Euclidean algorithm on δ-only data. It does not itself invoke T5–T8 or the RCL, but it is part of the foundation those landmarks sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.