orbit_euclidean_certificate
plain-language theorem explainer
The Euclidean algorithm on DistinctionNat is fully certified: native div/mod, GCD, coprimality, and ratio normalization all match ordinary Nat arithmetic under toNat. Anyone assembling the δ-only first-pass kernel cites this as the closed Euclidean orbit surface. The proof is a structure inhabitant that wires already-proved transport and cancellation lemmas into each certificate field.
Claim. There exists a closed Euclidean certificate on the base-neutral distinction orbit: for nonzero divisor $d$, the native quotient and remainder of $n$ by $d$ transport to $n/d$ and $n \bmod d$ on $\mathbb{N}$; the remainder is strictly smaller than $d$; $n = q\cdot d + r$; the native GCD transports to $\mathrm{Nat.gcd}$; coprimality is equivalent to Nat coprimality; any common divisor divides the GCD; if $a$ is coprime to $b$ and divides $b\cdot c$ then $a$ divides $c$; and signed-rational ratios normalize by the native orbit GCD.
background
DistinctionNat (K2.12) is the base-neutral finite orbit of repeated distinction: an inductive type with zero and successor, used as the native carrier for δ-only arithmetic before any external number system is assumed. The module builds Euclidean division and GCD on this carrier via fuelled recursion (divMod, gcd), then transports results to Mathlib Nat.
OrbitEuclideanCertificate is a Prop-structure bundling the closed surface for this pass: display equalities for div/mod, quotient, remainder, and GCD under toNat; the remainder bound; the decomposition $n = qd+r$; coprimality display; greatest-divisor and cancellation laws; and ratio normalization by native GCD. Upstream lemmas already prove each piece: divMod_toNat and gcd_toNat give transport; divides_gcd_of_divides_left_right is the native greatest-divisor law; coprime_divides_of_divides_mul_left is Euclid's lemma in orbit form ("native at the statement level; Nat appears only in transport").
proof idea
The proof inhabits OrbitEuclideanCertificate by assigning each field. Display and bound fields are direct references: divMod_toNat, quotient_toNat, remainder_toNat, remainder_lt_divisor, quotient_mul_divisor_add_remainder_eq, gcd_toNat, coprime_iff_nat_coprime, and ratio_normalization_target.
Two fields need short tactic wrappers. gcd_greatest_divisor introduces a common divisor $c$ of $a$ and $b$ and applies divides_gcd_of_divides_left_right. coprime_divisor_cancellation introduces coprimality and a divisibility hypothesis and applies coprime_divides_of_divides_mul_left. No new arithmetic is proved here; the certificate only packages the prior orbit-Euclidean lemmas.
why it matters
This certificate is the Euclidean half of the δ-only primitive recognition calculus: once division, GCD, and coprime cancellation live on DistinctionNat, signed-rational normalization and later kernel judgments can stay inside the orbit language. Downstream, kernel_first_pass_certificate (K7/A2) consumes it as part of inhabiting KernelFirstPassCertificate, which records that strength tags, trace syntax, judgment surface, and trace logic exist for the first pass.
In the broader Recognition forcing chain this sits under foundation scaffolding rather than T5–T8 themselves: it supplies the discrete arithmetic surface on which cost and composition laws are later stated. Closing the Euclidean orbit surface removes a scaffolding gap between raw distinction orbits and the integer/rational layer used by the kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.