divModFuel_toNat_aux
plain-language theorem explainer
Fueled Euclidean division on distinction naturals agrees with ordinary Nat quotient and remainder after the toNat embedding. Anyone proving that orbit-level div/mod is faithful to verifier arithmetic cites this lemma. The proof is induction on fuel, splitting on whether the divisor is at most the dividend and matching the Nat subtraction recurrences.
Claim. Let $n$, $d$, and fuel be distinction naturals with $d$ nonzero under the embedding to $\mathbb{N}$ and with $n$ bounded by the fuel. Writing $(q,r)$ for the fueled Euclidean division of $n$ by $d$, one has $q^{\mathbb{N}} = n^{\mathbb{N}} / d^{\mathbb{N}}$ and $r^{\mathbb{N}} = n^{\mathbb{N}} \bmod d^{\mathbb{N}}$.
background
Distinction naturals are the orbit-level naturals of the primitive recognition calculus, equipped with an embedding toNat into ordinary Lean Nat that reads off iteration count (identity maps to 0, successor adds one). Successor and the zero case of that embedding are the standard simp facts from ArithmeticFromLogic.
The local module builds a Euclidean algorithm on those orbits: divModFuel is a fuel-bounded recursive division that either returns remainder $n$ when $d \nleq n$, or recurses on truncated subtraction of $d$ from $n$. Comparison leq and truncated subtraction are the IntegerRational primitives; their interaction with toNat is already available as iff lemmas and a toNat_truncatedSub identity.
The setting is the foundation layer that reconstructs arithmetic operations so that later orbit Euclidean facts (quotient, remainder, gcd) can be checked against verifier Nat division rather than re-proved from scratch.
proof idea
Induction on fuel, generalizing over the dividend $n$.
Zero fuel: the bound forces $n^{\mathbb{N}}=0$; unfolding the fuel-zero clause of divModFuel and simplifying gives both sides zero, matching Nat div/mod of 0.
Successor fuel: rewrite the bound via toNat_succ, unfold divModFuel, and case on leq d n.
- If true, obtain $d^{\mathbb{N}} \le n^{\mathbb{N}}$ and positivity of $d^{\mathbb{N}}$. The recursive call is on truncated subtraction; the IH applies after a bound check via
toNat_truncatedSubandomega. Rewrite the IH equalities and finish withNat.div_eq_sub_divandNat.mod_eq_sub_mod. - If false, obtain $n^{\mathbb{N}} < d^{\mathbb{N}}$ from the false-branch of
leq, then both sides matchNat.div_eq_of_ltandNat.mod_eq_of_lt.
why it matters
This private auxiliary is the entire content of the public transport theorem divMod_toNat, which simply unfolds the unfueled divMod wrapper and applies the auxiliary. Downstream, that transport underwrites quotient_toNat, remainder_toNat, the remainder-less-than-divisor inequality, and the reconstruction identity $q\cdot d + r = n$ at the Nat level, and thence the orbit gcd construction.
In the Recognition foundation stack this is bookkeeping, not a physics claim: it certifies that the Euclidean algorithm written in distinction language is the same algorithm the verifier already trusts on Nat. That faithfulness is required before orbit divisibility and gcd can feed higher forcing or modular-realization arguments without a second arithmetic universe. No T0–T8 step is discharged here; the lemma is infrastructure for the primitive recognition calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.