gcdFuel_toNat_aux
plain-language theorem explainer
Fuel-bounded Euclidean GCD on distinction naturals agrees with ordinary Nat.gcd after reading off iteration counts, provided the fuel is at least the sum of the two arguments. Anyone proving that the RS gcd operator is the standard one cites this auxiliary. The argument is induction on fuel with case splits on zeros and the comparison branch, reducing via truncated subtraction to the classical gcd-sub identities.
Claim. Let $a,b,f$ be distinction naturals and write $n\mapsto |n|$ for the iteration-count embedding into $\mathbb{N}$. If $|a|+|b|\le |f|$, then the fuel-bounded Euclidean gcd satisfies $|\mathrm{gcd}_f(a,b)|=\gcd(|a|,|b|)$.
background
In the Primitive Recognition Calculus, counting is built from a generator orbit rather than assumed Peano structure. Distinction naturals carry a map toNat that reads off the iteration count; successor and addition are recovered so that this map is a semiring homomorphism (toNat_succ, toNat_add). Comparison and truncated subtraction are defined on the same carrier so the Euclidean algorithm can be stated without leaving the orbit language.
The module implements a fuel-bounded gcd (gcdFuel) that mirrors the classical subtractive Euclidean algorithm: if either argument is zero the other is returned; otherwise the smaller is subtracted from the larger and fuel decreases by one. Fuel is an explicit termination witness, not a hidden well-founded recursion.
The local goal is fidelity: after embedding by toNat, the fuel-bounded operator must equal Lean's Nat.gcd. The bound $|a|+|b|\le|f|$ guarantees enough steps for every subtraction path.
proof idea
Induct on fuel, generalizing over both arguments.
Zero fuel: the bound forces both arguments to embed to $0$; unfolding gcdFuel and using toNat_add matches Nat.gcd 0 0.
Successor fuel: unfold gcdFuel and split. If $a=0$ or $b=0$, simplify with Nat.gcd_zero_left / Nat.gcd_zero_right. Otherwise branch on whether $b\le a$. In the true branch, positivity of $b$ and the truncated-subtraction identity give a strictly smaller bound for the recursive call; the inductive hypothesis plus Nat.gcd_sub_self_left closes. The false branch is symmetric with Nat.gcd_sub_self_right. Comparison lemmas convert the Boolean leq tests into numeric inequalities used by omega.
why it matters
This private lemma is the computational heart of gcd_toNat, which drops the fuel hypothesis by instantiating fuel as $a+b$ and applying the bound tautologically. That public recovery theorem is what later orbit-divisibility and Euclidean-structure results cite when they need the RS gcd to be interchangeable with classical gcd under the iteration embedding.
In the Recognition foundation stack this sits under arithmetic-from-logic: once addition and order are recovered, the Euclidean algorithm must also transport. Without this transport, divisibility, coprimality, and any later number-theoretic forcing steps that mention gcd would be stuck on the distinction carrier. It does not itself touch the T0–T8 forcing chain, but it keeps the primitive calculus aligned with ordinary arithmetic so those later steps can quote standard gcd facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.