divides_gcd_of_divides_left_right
plain-language theorem explainer
Any common native divisor of two finite-orbit positions also divides their native GCD. Anyone assembling the δ-only Euclidean certificate on DistinctionNat cites this. The proof is a short transport: rewrite through the Nat display of divides and gcd, then apply Mathlib's Nat.dvd_gcd.
Claim. Let $a,b,c$ be positions in the base-neutral finite distinction orbit. If $c$ divides $a$ and $c$ divides $b$ in the native sense (there exist orbit positions $k,\ell$ with $c\cdot k=a$ and $c\cdot\ell=b$), then $c$ divides the native GCD $\gcd(a,b)$.
background
DistinctionNat is the inductive finite orbit of repeated distinction (K2.12): zero and successor, with no preferred base. Native divisibility is existential multiplication: divides c a means there is an orbit position $k$ with $c\cdot k=a$. The native GCD is defined by subtractive Euclidean descent (gcdFuel), not by importing Nat.gcd as the primary object.
The module builds an object-level Euclidean surface on this orbit: div/mod, remainder bounds, and GCD, all stated natively and only displayed to Nat for transport. Upstream, divides_iff_toNat_dvd records that native divisibility is equivalent to ordinary Nat divisibility after toNat. A companion gcd_toNat identifies the native GCD with Nat.gcd on the displays. Coprimality is then unit (gcd a b).
Local setting is Primitive Recognition Calculus: arithmetic that stays inside the closed δ-orbit until a deliberate display step.
proof idea
Term-mode transport, not a native Euclidean argument. Rewrite the goal with divides_iff_toNat_dvd and gcd_toNat, so the claim becomes ordinary Nat divisibility of Nat.gcd. Apply Mathlib Nat.dvd_gcd to the two hypotheses after converting each with (divides_iff_toNat_dvd _ _).mp. No fuel induction or remainder reasoning appears here; those live in the surrounding divMod/gcdFuel lemmas.
why it matters
Feeds orbit_euclidean_certificate, the closed δ-only Euclidean orbit surface that packages div/mod display, remainder bounds, quotient-remainder decomposition, and signed-rational normalization by native orbit GCD. Without common-divisor closure under GCD, that certificate cannot treat GCD as a genuine greatest common native divisor.
In the Recognition stack this is foundation plumbing under the forcing chain: the finite distinction orbit must carry a Euclidean algorithm before later layers (eight-tick octave, Clifford/Bott bridge, ladder arithmetic) can normalize ratios natively. The doc-comment states the content directly: any common native divisor divides the native GCD. It is proved, not scaffolding; it closes one algebraic obligation on the path to the certificate rather than an open physics claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.