gcd_divides_right
plain-language theorem explainer
On finite distinction orbits, the native GCD of a and b divides b. Ratio-normalization and Euclidean lemmas on the δ-orbit cite this as the right-divisor half of the GCD property. The proof is a two-step transport: rewrite native divisibility and GCD to Nat, then apply Mathlib's Nat.gcd_dvd_right.
Claim. For any finite distinction orbits $a,b$, the native GCD $\gcd(a,b)$ divides $b$: there exists an orbit $k$ with $\gcd(a,b)\cdot k = b$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and succ), the K2.12 carrier for native arithmetic in the primitive recognition calculus. Its verifier map toNat reads the orbit as an ordinary Nat by counting steps.
Native divisibility is existential multiplication: $a$ divides $b$ when some orbit $k$ satisfies $a\cdot k=b$. The bridge theorem divides_iff_toNat_dvd says this is equivalent to ordinary Nat divisibility of the images. The object-level GCD is defined by subtractive Euclidean descent (gcdFuel), and gcd_toNat identifies its image with Nat.gcd.
This module builds the Euclidean toolkit on orbits so ratios can be reduced without leaving the native carrier.
proof idea
Two rewrites, then a Mathlib fact. First rewrite the goal with divides_iff_toNat_dvd, turning native divisibility into toNat-level Nat divisibility. Second rewrite with gcd_toNat, so the left side becomes Nat.gcd a.toNat b.toNat. The residual goal is exactly Nat.gcd_dvd_right a.toNat b.toNat, which closes the proof.
why it matters
This is the right-hand half of the native GCD divisor property, needed before ratios can be cancelled by their GCD. Downstream, normalizeRatio divides numerator magnitude and denominator by gcd q.num.abs q.den; the companion lemma normalizeRatio_den_mul_gcd_toNat recovers the original denominator as normalized den times that GCD, and its proof invokes the divides hypothesis that this theorem supplies.
In the Recognition foundation stack, Euclidean structure on DistinctionNat is scaffolding for integer/rational reconstruction from pure distinction orbits, upstream of forcing-chain arithmetic and the phi-ladder mass bookkeeping. No T5–T8 claim is made here; the lemma is pure orbit arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.