Algebraic infrastructure for R = QuadraticAlgebra ℤ (-2) 1 = ℤ[(1+√-7)/2]

Following Michael Stoll's suggestion to work directly in QuadraticAlgebra ℤ (-2) 1 rather than through 𝓞 K where K = QuadraticAlgebra ℚ (-2) 1. The payoff:

• θ ^ 2 = θ - 2, θ * θ' = 2, θ + θ' = 1, norm θ = 2, norm θ' = 2 are all literal rfls (no Subtype.ext ceremony, no omega_mul_omega_eq_mk).
• units_pm_one reduces to a one-page completing-the-square argument over ℤ.
• EuclideanDomain R → IsPrincipalIdealRing R → UniqueFactorizationMonoid R replaces the discriminant / class-number-1 detour through Dirichlet.

@[reducible, inline]

abbrev RamanujanNagell.R : Type

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

Equations

• RamanujanNagell.R = QuadraticAlgebra ℤ (-2) 1

def RamanujanNagell.θ : R

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

Equations

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

def RamanujanNagell.θ' : R

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

Equations

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

Stoll's rfl claims

theorem RamanujanNagell.theta_sq : θ ^ 2 = θ - 2

theorem RamanujanNagell.theta_mul_theta' : θ * θ' = 2

theorem RamanujanNagell.theta_add_theta' : θ + θ' = 1

theorem RamanujanNagell.theta'_eq_one_sub_theta : θ' = 1 - θ

theorem RamanujanNagell.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 RamanujanNagell.norm_eq (x y : ℤ) : QuadraticAlgebra.norm { re := x, im := y } = x ^ 2 + x * y + 2 * y ^ 2

theorem RamanujanNagell.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 RamanujanNagell.norm_nonneg (z : R) : 0 ≤ QuadraticAlgebra.norm z

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

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

Units are ±1

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

θ and θ' are irreducible

theorem RamanujanNagell.theta_irreducible : Irreducible θ

theorem RamanujanNagell.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 RamanujanNagell.quot (a b : R) : R

Smart-rounded quotient.

Equations

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

noncomputable def RamanujanNagell.rem (a b : R) : R

Smart-rounded remainder: rem a b = a - b * quot a b.

Equations

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

@[simp]

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

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

@[implicit_reducible]

noncomputable instance RamanujanNagell.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 RamanujanNagell.instPrincipalIdealRing : IsPrincipalIdealRing R

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

instance RamanujanNagell.instUniqueFactorizationMonoid : UniqueFactorizationMonoid R

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

θ, θ' are prime

theorem RamanujanNagell.theta_prime : Prime θ

theorem RamanujanNagell.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 RamanujanNagell.theta_theta'_not_associated : ¬Associated θ θ'

theorem RamanujanNagell.theta_not_dvd_theta' : ¬θ ∣ θ'

theorem RamanujanNagell.theta'_not_dvd_theta : ¬θ' ∣ θ

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

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

theorem RamanujanNagell.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 RamanujanNagell.ufd_associated_dichotomy (α β : R) (m : ℕ) (h_prod : α * β = θ ^ m * θ' ^ m) (h_coprime : IsCoprime α β) (hα : ¬IsUnit α) (hβ : ¬IsUnit β) : Associated α (θ ^ m) ∨ Associated α (θ' ^ m)

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

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