divModFuel
plain-language theorem explainer
Fuelled Euclidean division on finite distinction-orbit naturals: fuel, dividend, and divisor yield a quotient–remainder pair by repeated truncated subtraction. The unfuelled div-mod wrapper and the bridge that matches ordinary natural division both call it. The body is pure structural recursion on the fuel argument.
Claim. On finite distinction-orbit naturals, define $\mathrm{divModFuel}(f,n,d)$ by recursion on fuel $f$: if $f=0$, return $(0,n)$; if $f=f'+1$ and $d\le n$, let $(q,r)=\mathrm{divModFuel}(f',n\dot{-}d,d)$ and return $(q+1,r)$; otherwise return $(0,n)$.
background
DistinctionNat (K2.12) is the base-neutral finite orbit of repeated distinction: an inductive type with zero and successor, the object-level stand-in for naturals built from recognition primitives rather than from the verifier's Nat.
On that type the IntegerRational layer supplies Boolean order by structural recursion and truncated subtraction (both free of meta-level arithmetic). The Euclidean module builds quotient and remainder from those primitives so later gcd and divisibility stay inside the orbit calculus.
The first argument is orbit fuel used only to guarantee termination of repeated subtraction; the module doc for the unfuelled wrapper notes that fuel equal to the dividend is enough when the divisor is nonzero, because each successful subtraction lowers the dividend by at least one.
proof idea
Definition by pattern match on fuel, not a proved theorem. Zero fuel returns quotient zero and remainder equal to the dividend. On successor fuel, test Boolean order of divisor against dividend: if true, recurse on truncated subtraction of divisor from dividend with decremented fuel, then take successor of the recursive quotient and keep the recursive remainder; if false, stop with quotient zero and remainder the dividend. No lemmas are invoked; the clauses are the algorithm.
why it matters
Direct body of the unfuelled Euclidean div-mod, which sets fuel equal to the dividend under a nonzero-divisor hypothesis. Also the object of the private bridge theorem that identifies the orbit-level pair with ordinary natural division and modulo (under a fuel bound and nonzero divisor).
That bridge underwrites the object-level quotient and remainder projections, the remainder-strictly-less-than-divisor fact, and the reconstruction identity quotient times divisor plus remainder equals the dividend. Those facts are the Euclidean toolkit for orbit-level gcd in the same module. In the Recognition foundation this keeps arithmetic inside the distinction-orbit calculus instead of importing Peano structure from the meta-level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.