gcdFuel
plain-language theorem explainer
Fuel-bounded subtractive Euclidean algorithm on finite distinction orbits: repeatedly replace the larger argument by its truncated difference until one vanishes. Anyone building object-level gcd, coprimality, or lattice arithmetic on DistinctionNat cites this. The definition is structural recursion on the fuel, with Boolean order and truncated subtraction driving the descent.
Claim. Given fuel $f$ and finite distinction-orbit positions $a,b$, define $\mathrm{gcdFuel}(f,a,b)$ by recursion on $f$: if $f=0$ return $a+b$; if $a=0$ return $b$; if $b=0$ return $a$; if $b\le a$ recurse on $(f-1,\,a\dot{-}b,\,b)$; otherwise recurse on $(f-1,\,a,\,b\dot{-}a)$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with zero and successor, the object-level stand-in for natural numbers in the primitive recognition calculus. Truncated subtraction $a\dot{-}b$ and Boolean order $\mathrm{leq}$ are defined by structural recursion on those constructors, so all comparisons stay inside the orbit language.
The classical Euclidean algorithm computes $\gcd(a,b)$ by repeated remainder (or, equivalently, repeated subtraction). Here the remainder step is replaced by truncated subtraction of the smaller from the larger, and a separate fuel argument guarantees well-founded recursion in Lean without appealing to a well-order on pairs.
The module builds object-level division and gcd on these orbits so that later arithmetic (coprimality, lattice statements) can be stated without jumping to meta-level Nat.
proof idea
Pure definition by pattern-match on fuel. The zero-fuel clause returns $a+b$ (a safe upper bound when fuel is exhausted). With positive fuel, the zero cases short-circuit to the nonzero argument; otherwise Boolean $\mathrm{leq}$ chooses which truncated difference to take, and the call recurses on the predecessor fuel. No lemmas are invoked at the definition site; correctness against Nat.gcd is proved later by induction on fuel.
why it matters
This is the engine under the object-level gcd: gcd a b is defined as gcdFuel (a + b) a b, so every coprimality or Euclidean identity in the module routes through this fuelled descent. The companion lemma gcdFuel_toNat_aux shows that, once fuel is at least $a.toNat + b.toNat$, the result agrees with ordinary Nat.gcd, tying the orbit calculus back to classical arithmetic.
In the Recognition foundation stack this sits inside PrimitiveRecognitionCalculus: building Peano-style arithmetic from distinction orbits rather than positing integers. It is scaffolding for later number-theoretic structure (coprimality, fractions on orbits), not a forcing-chain step (T0–T8) itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.