gcd

Distinction-naturals are the base-neutral finite orbits of repeated distinction: an inductive type with zero and successor, standing in for ordinary natural numbers without committing to a numeral base. The surrounding module builds an object-level Euclidean toolkit (division-with-remainder, quotient, remainder, and GCD) entirely inside that type, so later factorization and gap arguments never leave the recognition calculus.

The fuelled routine takes three arguments: remaining fuel, current $a$, and current $b$. When fuel is exhausted it returns $a+b$; otherwise it branches on zeros and subtracts the smaller from the larger, decrementing fuel. Seeding fuel by $a+b$ is the standard termination trick for subtractive Euclidean descent on naturals: each successful subtraction strictly decreases the sum, so the fuel bound is tight enough to finish.

One-line wrapper: call the fuelled subtractive Euclidean GCD on the triple $(a+b,,a,,b)$. No further case analysis lives at this definition; all branching and termination logic sits inside the fuelled helper.

This is the workhorse GCD used throughout the foundation layer. Downstream it appears in dimension forcing (sync-period factorization $360=8\times 45/\gcd(8,45)$, and the claim that gap-45 has factor 9), in gap derivation (coprimality of $2^D$ with $D^2(D+2)$ for odd $D$, and failure of coprimality for even $D$), and in period-factorization lemmas that extract nontrivial factors from even periods. Those results feed the forcing chain toward $D=3$ spatial dimensions and the eight-tick octave (T7–T8). It is also referenced from the cost-side rational-exponent argument that closes the gauge-classification exponent step.