Canonical Euclidean Domains

This module defines CanonicalEuclideanDomain and provides instances for ℤ, Polynomial F, and Field.

class CanonicalEuclideanDomain (R : Type u) extends EuclideanDomain R : Type u

Canonical Euclidean Domains

A CanonicalEuclideanDomain is a restriction of EuclideanDomain. It introduces a selection rule for canonical remainders and guarantees there exists exactly one canonical quotient (q) and remainder (r) for any pair of dividend (a) and divisor (b) (assuming b ≠ 0), no matter how the division is implemented (i.e. the division result is unique and consistent across different implementations).

Motivation: The unpredictable behaviors of / and % in EuclideanDomain

In a standard EuclideanDomain, the operators / and % are viewed as black-boxes and are only required to return some valid pair satisfying a = b * q + r and r ≺ b. This loose specification allows implementations to be unpredictable and inconsistent:

1. Unprovable Algebraic Identities: An implementation is permitted to switch strategies arbitrarily (e.g., rounding up for input x but down for input y; or following truncation-towards-zero as in C/Rust/Java, ...). This makes natural identities like (a + b * k) / b = a / b + k false in the general case, as the term b * k might trigger a strategy switch.
2. Non-Determinism Accumulation (Unit Drift): Algorithms that chain multiple operations (like GCD) accumulate arbitrary unit factors at every step. For example, gcd(a, b) is only unique up to a unit.
   • gcd(a, gcd(b, c)) might return g.
   • gcd(gcd(a, b), c) might return -g (or u * g). While mathematically equivalent (associates), they are not equal as data structures. This breaks any system relying on bit-exact equality (hashing, caching, serialization).

The Solution: CanonicalEuclideanDomain solves this by enforcing a strict is_canonical_remainder predicate. This restricts the implementation space to exactly one valid function, ensuring the bit-exact uniqueness of the outputs, no matter what implementations are used.

Advantages

• Algebraic Stability: Restores critical algebraic properties, enabling a suite of powerful rewrite rules (e.g., add_mod_eq, add_mul_div_right, mul_mod_eq, mod_eq_of_eq_add_mul) that are unprovable in the normal EuclideanDomain setting. This brings canonical regularity to domains with non-unique remainders (e.g., ℤ, Polynomial F).

• Generic Algorithms over Rings: Guarantees strictly normalized outputs (positive GCDs, monic generators) for high-level algorithms (Smith Normal Form, Hermite Normal Form). It prevents the unit drift described above, allowing generic algorithms to run deterministically on complex domains like Polynomial F.

• Protocol Determinism: Essential for cryptographic protocols (ZK transcripts, Fiat-Shamir) where objects must have bit-exact representations. It ensures that every implementation (Lean, Rust, ZK circuits) converges to the same remainder given the same canonical remainder rule, guaranteeing correctness and hash consistency.

Supported Instances

This abstraction unifies commonly used mathematical objects under one interface:

1. Integers (ℤ): The canonical rule enforces non-negative remainders (0 ≤ r < |b|). This matches the behavior of Python's % or Rust's rem_euclid.
2. Polynomials (Polynomial F): Uniqueness is naturally enforced by the degree structure. Any remainder with degree(r) < degree(b) is automatically unique due to the ultrametric property of polynomial degrees (i.e., degree(a - b) ≤ max(degree a, degree b)).
3. Fields (ℚ, ℝ, ZMod p where p is prime, ...): Division is exact; the canonical remainder is always 0.
4. Other Euclidean Rings: Gaussian Integers (ℤ[i]), Eisenstein Integers (ℤ[ω]), and Discrete Valuation Rings (DVRs) can potentially be adapted to this interface by defining strict geometric or valuation-based selection rules.

Definition

It extends EuclideanDomain with:

1. is_canonical_remainder b r: A predicate deciding if a remainder r is the "chosen one".
2. remainder_is_canonical: A proof that the built-in % operator satisfies this predicate.
3. unique_division: The Uniqueness Axiom stating that if (q1, r1) and (q2, r2) both satisfy the division equation and the canonical rule, they must be equal.

• zero : R
• add : R → R → R
• add_assoc (a b c : R) : a + b + c = a + (b + c)
• zero_add (a : R) : 0 + a = a
• add_zero (a : R) : a + 0 = a
• nsmul : ℕ → R → R
• nsmul_zero (x : R) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : R) : (n + 1) • x = n • x + x
• add_comm (a b : R) : a + b = b + a
• one : R
• mul : R → R → R
• mul_assoc (a b c : R) : a * b * c = a * (b * c)
• one_mul (a : R) : 1 * a = a
• mul_one (a : R) : a * 1 = a
• npow : ℕ → R → R
• npow_zero (x : R) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : R) : x ^ (n + 1) = x ^ n * x
• zero_mul (a : R) : 0 * a = 0
• mul_zero (a : R) : a * 0 = 0
• left_distrib (a b c : R) : a * (b + c) = a * b + a * c
• right_distrib (a b c : R) : (a + b) * c = a * c + b * c
• natCast : ℕ → R
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• neg : R → R
• sub : R → R → R
• zsmul : ℤ → R → R
• sub_eq_add_neg (a b : R) : a - b = a + -b
• zsmul_zero' (a : R) : 0 • a = 0
• zsmul_succ' (n : ℕ) (a : R) : ↑n.succ • a = ↑n • a + a
• zsmul_neg' (n : ℕ) (a : R) : Int.negSucc n • a = -(↑n.succ • a)
• neg_add_cancel (a : R) : -a + a = 0
• intCast : ℤ → R
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• mul_comm (a b : R) : a * b = b * a
• exists_pair_ne : ∃ (x : R) (y : R), x ≠ y
• quotient : R → R → R
• quotient_zero (a : R) : EuclideanDomain.quotient a 0 = 0
• remainder : R → R → R
• quotient_mul_add_remainder_eq (a b : R) : b * EuclideanDomain.quotient a b + EuclideanDomain.remainder a b = a
• r : R → R → Prop
• r_wellFounded : WellFounded EuclideanDomain.r
• remainder_lt (a : R) {b : R} : b ≠ 0 → EuclideanDomain.r (EuclideanDomain.remainder a b) b
• mul_left_not_lt (a : R) {b : R} : b ≠ 0 → ¬EuclideanDomain.r (a * b) a
• is_canonical_remainder (b r : R) : Prop
• remainder_is_canonical (a b : R) (hb : b ≠ 0) : is_canonical_remainder b (EuclideanDomain.remainder a b)
• unique_division {a b q₁ q₂ r₁ r₂ : R} (hb : b ≠ 0) (h_eq_div_mul_add₁ : a = b * q₁ + r₁) (h_eq_div_mul_add₂ : a = b * q₂ + r₂) (is_canonical_remainder₁ : is_canonical_remainder b r₁) (is_canonical_remainder₂ : is_canonical_remainder b r₂) : q₁ = q₂ ∧ r₁ = r₂

@[instance_reducible]

instance Int.instCanonicalEuclideanDomainInt : CanonicalEuclideanDomain ℤ

@[instance_reducible]

noncomputable instance Polynomial.instCanonicalEuclideanDomainPoly {F : Type u} [Field F] : CanonicalEuclideanDomain (Polynomial F)

theorem Field.mod_eq_zero {K : Type u} [Field K] (a b : K) (hb : b ≠ 0) : a % b = 0

@[instance_reducible]

instance Field.instCanonicalEuclideanDomainField {K : Type u} [Field K] : CanonicalEuclideanDomain K

theorem CanonicalEuclideanDomain.div_eq_of_canonical_eq_mul_add {R : Type u} [CanonicalEuclideanDomain R] {a b q r : R} (hb : b ≠ 0) (h_eq : a = b * q + r) (h_can : is_canonical_remainder b r) : a / b = q

The Fundamental Theorem of Canonical Euclidean Domains. If you find ANY pair (q, r) that satisfies the division equation AND the canonical condition, then q MUST be the result of the division operation.

theorem CanonicalEuclideanDomain.div_eq_and_mod_eq_iff {R : Type u} [CanonicalEuclideanDomain R] {a b q r : R} (hn : b ≠ 0) : a / b = q ∧ a % b = r ↔ a = b * q + r ∧ is_canonical_remainder b r

The Fundamental Theorem of CEDs: Satisfying the division equation + size constraint is EQUIVALENT to being the output of the division function.

Division Properties

theorem CanonicalEuclideanDomain.add_mul_div_right {R : Type u} [CanonicalEuclideanDomain R] (a b r : R) (hb : b ≠ 0) : (a + b * r) / b = a / b + r

Generalized add_mul_div_right: (a + b * r) / b = a / b + r In a standard ED, this isn't always true (the quotient is not unique). In a CED, it is always true.

theorem CanonicalEuclideanDomain.add_mul_mod_right {R : Type u} [CanonicalEuclideanDomain R] (a b r : R) (hb : b ≠ 0) : (a + b * r) % b = a % b

Generalized add_mul_mod_right: (a + b * r) % b = a % b The remainder ignores multiples of the divisor.

theorem CanonicalEuclideanDomain.add_mul_mod_left {R : Type u} [CanonicalEuclideanDomain R] (a b r : R) (hb : a ≠ 0) : (a * r + b) % a = b % a

Generalized add_mul_mod_left: (a * r + b) % a = b % a` The remainder ignores multiples of the divisor.

theorem CanonicalEuclideanDomain.mod_eq_of_eq_add_mul {R : Type u} [CanonicalEuclideanDomain R] {a b n q : R} (h_eq_add_mul : a = b + n * q) (hn : n ≠ 0) : a % n = b % n

If a = b + n * r, then a % n = b % n.

Arithmetic Modulo Properties

theorem CanonicalEuclideanDomain.mul_mod_eq_mul_mod_left {R : Type u} [CanonicalEuclideanDomain R] (a b n : R) (hn : n ≠ 0) : a * b % n = a % n * b % n

(a * b) % n = ((a % n) * b) % n

theorem CanonicalEuclideanDomain.mul_mod_eq_zero_of_mod_dvd {R : Type u} [CanonicalEuclideanDomain R] (a b n : R) (hn : n ≠ 0) (h_mod_eq_zero : a % n = 0) : a * b % n = 0

(a * b) % n = 0 if a % n = 0

theorem CanonicalEuclideanDomain.add_mod_eq_add_mod_left {R : Type u} [CanonicalEuclideanDomain R] (a b n : R) (hn : n ≠ 0) : (a + b) % n = (a % n + b) % n

(a + b) % n = ((a % n) + b) % n

theorem CanonicalEuclideanDomain.add_mod_eq {R : Type u} [CanonicalEuclideanDomain R] (a b n : R) (hn : n ≠ 0) : (a + b) % n = (a % n + b % n) % n

(a + b) % n = (a % n + b % n) % n

theorem CanonicalEuclideanDomain.mul_mod_eq {R : Type u} [CanonicalEuclideanDomain R] (a b n : R) (hn : n ≠ 0) : a * b % n = a % n * (b % n) % n

(a * b) % n = ((a % n) * (b % n)) % n

theorem CanonicalEuclideanDomain.mod_mod_eq_mod {R : Type u} [CanonicalEuclideanDomain R] (a n : R) (hn : n ≠ 0) : a % n % n = a % n

(a % n) % n = a % n

theorem CanonicalEuclideanDomain.dvd_sub_mod {R : Type u} [CanonicalEuclideanDomain R] (a b : R) : b ∣ a - a % b

b | a - (a % b)