gcd_divides_left
plain-language theorem explainer
On the native distinction orbit, the Euclidean GCD of two positions divides the left argument. Anyone reducing ratios or proving coprimality of normalized orbits cites this. The proof transports the claim to Lean Nat via the toNat bridge and invokes the standard Nat left-divisibility of gcd.
Claim. For any two finite distinction-orbit positions $a$ and $b$, the object-level GCD $\gcd(a,b)$ divides $a$: there exists an orbit position $k$ with $\gcd(a,b)\cdot k = a$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor), the native stand-in for natural numbers in the Primitive Recognition Calculus. Its verifier map toNat reads the orbit as an ordinary Nat.
Native divisibility is existential multiplication on the orbit: $a$ divides $b$ when some $k$ satisfies $a\cdot k=b$. The bridge theorem states this is equivalent to ordinary Nat divisibility of the images under toNat.
The object-level GCD is defined by subtractive Euclidean descent (fuelled recursion on $a+b$). A companion lemma identifies its toNat image with Nat.gcd. The present result is the left half of the usual “GCD divides both inputs” package on that native type.
proof idea
One short rewrite chain. First replace native divides by Nat divisibility via divides_iff_toNat_dvd. Then replace toNat (gcd a b) by Nat.gcd a.toNat b.toNat via gcd_toNat. The goal is exactly Nat.gcd_dvd_left, which finishes the proof.
why it matters
Ratio normalization on orbits cancels the GCD of absolute numerator and denominator. Downstream, normalizeRatio_num_mul_gcd_toInt multiplies the reduced numerator back by that GCD and recovers the original integer numerator; that step needs the GCD to divide the left input. The same fact feeds normalizeRatio_reduced_signCanonical in PRCNativeCostUniqueness, which certifies that normalized ratios are coprime and sign-canonical.
In the Recognition stack this is arithmetic scaffolding under the primitive calculus, not a forcing-chain landmark (T5–T8). It keeps native Euclidean arithmetic aligned with Mathlib so later uniqueness and cost arguments can work entirely on DistinctionNat without leaving the orbit language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.