gcd_toNat
plain-language theorem explainer
The object-level GCD on distinction orbits agrees with Lean’s Nat.gcd after the verifier map toNat. Anyone proving native divisibility, coprimality, or ratio normalization cites this bridge. The proof unfolds the fuelled Euclidean definition and applies the fuelled auxiliary, using additivity of toNat for the fuel bound.
Claim. For distinction orbits $a,b$, the verifier reading of their object-level GCD equals the ordinary natural-number GCD of their readings: $\mathrm{toNat}(\gcd(a,b)) = \gcd(\mathrm{toNat}(a),\mathrm{toNat}(b))$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, the primitive counting object of the recognition calculus. Its verifier map toNat sends zero to 0 and successor to Nat.succ, so every orbit position has a unique Nat display.
Object-level addition on orbits is already known to match Nat addition under toNat (OrbitArithmetic.toNat_add / the ArithmeticFromLogic recovery theorem). The Euclidean layer defines gcd by subtractive descent: gcd a b := gcdFuel (a + b) a b, where the sum supplies a fuel bound that decreases along the algorithm.
This module sits in PrimitiveRecognitionCalculus.OrbitEuclidean: it builds native division and GCD so that later ratio normalization and coprimality can be stated without leaving the orbit language, while still recovering classical Nat facts via toNat.
proof idea
One short tactic proof. Unfold the definition gcd a b = gcdFuel (a + b) a b. Apply the auxiliary gcdFuel_toNat_aux, which states that the fuelled Euclidean algorithm on orbits displays as Nat.gcd when the fuel is large enough. Discharge the fuel hypothesis by rewriting with toNat_add, so (a + b).toNat becomes a.toNat + b.toNat, the standard sufficient bound for subtractive Euclidean descent on Nats.
why it matters
This is the display bridge that lets every subsequent native GCD lemma import Mathlib’s Nat.gcd facts in one rewrite. Downstream, gcd_divides_left/right and divides_gcd_of_divides_left_right become Nat.gcd_dvd_* and Nat.dvd_gcd after gcd_toNat; coprime_iff_nat_coprime is a simp of the same equality; gcd_ne_zero_of_right_ne_zero and normalizeRatio_coprime use it to keep reduced ratios coprime in orbit language; orbit_euclidean_certificate packages the whole Euclidean layer.
In the Recognition stack this is foundation arithmetic, not yet the forcing chain T5–T8, but it is the substrate on which integer/rational orbit structure (and later mass-ladder bookkeeping) rests. Without the toNat agreement, native coprimality and ratio normalization would be isolated from classical number theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.