divMod
plain-language theorem explainer
Euclidean quotient and remainder on the object-level naturals of the primitive recognition calculus. Given dividend n and nonzero divisor d, it returns the pair (q,r) built by repeated subtraction. Cited by the orbit Euclidean certificate and by the transport theorems that match this pair to verifier Nat division and modulus. One-line wrapper that seeds the fuelled subtraction routine with fuel equal to the dividend.
Claim. For object-level naturals $n$ and $d$ with $d \neq 0$, the Euclidean pair $(q,r)$ is obtained by running fuelled repeated subtraction on $(n,d)$ with fuel equal to $n$. The first component is the quotient and the second is the remainder.
background
The ambient type is the base-neutral finite orbit of repeated distinction: an inductive Peano-style natural with constructors zero and succ, introduced as K2.12 in the primitive recognition calculus. Arithmetic here is object-level; it is not the verifier's Nat.
Euclidean division is realized by fuelled repeated subtraction. The fuelled routine takes an orbit fuel, a current dividend, and a divisor: if the fuel is exhausted it returns (zero, dividend); otherwise, when the divisor is at most the dividend it recurses on the truncated difference and increments the quotient, else it stops with remainder equal to the current dividend.
This module builds the Euclidean surface on that orbit: quotient, remainder, gcd, and the certificates that transport those operations to ordinary Nat division and modulus.
proof idea
One-line wrapper. It calls the fuelled subtraction routine with fuel equal to the dividend, dividend equal to n, and divisor equal to d. The nonzero hypothesis on d is present only to justify that this fuel bound is enough: each successful subtraction lowers the dividend by at least one, so fuel n cannot run out before the algorithm terminates.
why it matters
This is the single entry point for object-level Euclidean division on DistinctionNat. The projections quotient and remainder are defined by taking the first and second components of the returned pair. The transport theorem divMod_toNat unfolds this definition and applies the fuelled correctness lemma, proving that the pair maps under toNat to ordinary Nat division and modulus. That transport is the divmod_display field of OrbitEuclideanCertificate, the bundling certificate for the Euclidean orbit surface closed in this pass. In the Recognition foundation stack this is scaffolding for later arithmetic on the phi-ladder and eight-tick structures, not yet a physics claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.