@[reducible, inline]

abbrev R : Type

The integer ring ℤ[(1 + √-7)/2], packaged as QuadraticAlgebra ℤ (-2) 1.

Equations

• R = QuadraticAlgebra ℤ (-2) 1

def θ : R

θ = (1 + √-7)/2, the generator of R.

Equations

• θ = { re := 0, im := 1 }

def θ' : R

θ' = (1 - √-7)/2 = 1 - θ, the Galois conjugate of θ.

Equations

• θ' = { re := 1, im := -1 }

Stoll's rfl claims

theorem theta_sq : θ ^ 2 = θ - 2

theorem theta_mul_theta' : θ * θ' = 2

theorem theta_add_theta' : θ + θ' = 1

theorem theta'_eq_one_sub_theta : θ' = 1 - θ

theorem two_factorisation_R : θ * (1 - θ) = 2

For backward compatibility with the old Helpers API.

Norm form and positivity

norm ⟨x, y⟩ = x² + xy + 2y²; the key identity is 4·N = (2x + y)² + 7y².

theorem norm_eq (x y : ℤ) : QuadraticAlgebra.norm { re := x, im := y } = x ^ 2 + x * y + 2 * y ^ 2

theorem four_norm_eq (z : R) : 4 * QuadraticAlgebra.norm z = (2 * z.re + z.im) ^ 2 + 7 * z.im ^ 2

The completing-the-square identity.

theorem norm_nonneg (z : R) : 0 ≤ QuadraticAlgebra.norm z

theorem norm_eq_zero_iff (z : R) : QuadraticAlgebra.norm z = 0 ↔ z = 0

theorem norm_pos {z : R} (hz : z ≠ 0) : 0 < QuadraticAlgebra.norm z

Units are ±1

theorem units_pm_one (u : Rˣ) : u = 1 ∨ u = -1

θ and θ' are irreducible

theorem theta_irreducible : Irreducible θ

theorem theta'_irreducible : Irreducible θ'

EuclideanDomain instance via smart rounding

R = ℤ[(1+√-7)/2] with norm N(x, y) = x² + xy + 2y². To divide a by b ≠ 0, we want q such that N(a - b·q) < N(b). Naive independent rounding of (a/b) in the (re, im) basis can leave N = 1 exactly at the fundamental-domain corner; the fix is to round im first, then re-round re shifted by half the im residual. With that choice 16·N(rem) ≤ 11·N(b).

noncomputable def quot (a b : R) : R

Smart-rounded quotient.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def rem (a b : R) : R

Equations

• rem a b = a - b * quot a b

@[simp]

theorem quot_zero (a : R) : quot a 0 = 0

theorem quot_mul_add_rem_eq (a b : R) : b * quot a b + rem a b = a

@[implicit_reducible]

noncomputable instance instEuclideanDomain : EuclideanDomain R

R is a Euclidean domain. Division of a by b ≠ 0 uses smart rounding of a · star b / N(b) (round the im coordinate first, then shift-round re), which guarantees 16 · N(rem) ≤ 11 · N(b), hence a strictly smaller norm.

Equations

• One or more equations did not get rendered due to their size.

instance instPrincipalIdealRing : IsPrincipalIdealRing R

R is a principal ideal ring, since every Euclidean domain is one.

instance instUniqueFactorizationMonoid : UniqueFactorizationMonoid R

R is a unique factorization domain, since every principal ideal ring is one.

θ, θ' are prime

theorem theta_prime : Prime θ

theorem theta'_prime : Prime θ'

UFD scaffolding for the Ramanujan-Nagell argument

These lemmas combine units_pm_one with UniqueFactorizationMonoid R to give the key dichotomy α * β = θ^m · θ'^m ∧ IsCoprime α β → α = ±θ^m ∨ α = ±θ'^m.

theorem theta_theta'_not_associated : ¬Associated θ θ'

theorem theta_not_dvd_theta' : ¬θ ∣ θ'

theorem theta'_not_dvd_theta : ¬θ' ∣ θ

theorem theta_pow_dvd_of_coprime_prod (α β : R) (m : ℕ) (h_prod : α * β = θ ^ m * θ' ^ m) (h_coprime : IsCoprime α β) : θ ^ m ∣ α ∨ θ ^ m ∣ β

theorem associated_of_theta_pow_dvd (α β : R) (m : ℕ) (h_prod : α * β = θ ^ m * θ' ^ m) (h_coprime : IsCoprime α β) (_hα : ¬IsUnit α) (hβ : ¬IsUnit β) (h_dvd : θ ^ m ∣ α) : Associated α (θ ^ m)

theorem associated_of_theta_pow_dvd_right (α β : R) (m : ℕ) (h_prod : α * β = θ ^ m * θ' ^ m) (h_coprime : IsCoprime α β) (hα : ¬IsUnit α) (_hβ : ¬IsUnit β) (h_dvd : θ ^ m ∣ β) : Associated α (θ' ^ m)

theorem ufd_associated_dichotomy (α β : R) (m : ℕ) (h_prod : α * β = θ ^ m * θ' ^ m) (h_coprime : IsCoprime α β) (hα : ¬IsUnit α) (hβ : ¬IsUnit β) : Associated α (θ ^ m) ∨ Associated α (θ' ^ m)

theorem associated_eq_or_neg (α γ : R) (h : Associated α γ) : α = γ ∨ α = -γ

theorem ufd_power_association (α β : R) (m : ℕ) (h_prod : α * β = θ ^ m * θ' ^ m) (h_coprime : IsCoprime α β) (hα : ¬IsUnit α) (hβ : ¬IsUnit β) : (α = θ ^ m ∨ α = -θ ^ m) ∨ α = θ' ^ m ∨ α = -θ' ^ m