The Ramanujan-Nagell equation

The integer ring R = ℤ[(1 + √-7)/2] = QuadraticAlgebra ℤ (-2) 1 is a Euclidean domain (see Helpers.lean); in particular it is a PID and a UFD. The proof below uses these facts together with units_pm_one, theta_irreducible, theta'_irreducible, and the UFD scaffolding ufd_power_association.

theorem factors_in_R_with_product (x : ℤ) (m : ℕ) (hm_ge : m ≥ 3) (h : (x ^ 2 + 7) / 4 = 2 ^ m) : ∃ (α : R) (β : R), α * β = θ ^ m * θ' ^ m ∧ α - β = 2 * θ - 1

The conjugate factors (x ± √-7)/2 lie in R (since x is odd) and their product equals (x²+7)/4 = 2^m = θ^m · θ'^m.

theorem conjugate_factors_coprime (α β : R) (m : ℕ) (h_prod : α * β = θ ^ m * θ' ^ m) (h_diff : α - β = 2 * θ - 1) : IsCoprime α β

The conjugate factors are coprime in R.

theorem factor_not_unit_left (α β : R) (m : ℕ) (h_prod : α * β = θ ^ m * θ' ^ m) (h_diff : α - β = 2 * θ - 1) : ¬IsUnit α

If α = ±1, then α - β has im-component 0, but 2θ - 1 has im 2.

theorem factor_not_unit_right (α β : R) (m : ℕ) (h_prod : α * β = θ ^ m * θ' ^ m) (h_diff : α - β = 2 * θ - 1) : ¬IsUnit β

theorem eliminate_x_conclude (α β : R) (m : ℕ) (h_diff : α - β = 2 * θ - 1) (h_assoc : (α = θ ^ m ∨ α = -θ ^ m) ∨ α = θ' ^ m ∨ α = -θ' ^ m) (h_prod : α * β = θ ^ m * θ' ^ m) : 2 * θ - 1 = θ ^ m - θ' ^ m ∨ -2 * θ + 1 = θ ^ m - θ' ^ m

From the dichotomy α ∈ {±θ^m, ±θ'^m} and the product relation, determine β, then take the difference α - β = 2θ-1 to obtain the conclusion.

theorem must_have_minus_sign (m : ℕ) (hm_odd : Odd m) (hm_ge : m ≥ 3) (h : 2 * θ - 1 = θ ^ m - θ' ^ m ∨ -2 * θ + 1 = θ ^ m - θ' ^ m) : -2 * θ + 1 = θ ^ m - θ' ^ m

The minus sign must hold in the disjunction. Proved by reducing modulo θ'²: if 2θ - 1 = θ^m - θ'^m, then θ^m - θ ≡ θ'^m - θ' (mod θ'²), and combining with θ^m ≡ θ (mod θ'²) (for odd m) and θ'^m ≡ 0 (mod θ'²) (m ≥ 2) forces θ'² ∣ θ', hence θ' is a unit — contradicting units_pm_one.

theorem main_m_condition (x : ℤ) (m : ℕ) : Odd m → m ≥ 3 → (x ^ 2 + 7) / 4 = 2 ^ m → -2 * θ + 1 = θ ^ m - θ' ^ m

theorem reduction_divide_by_4 (x : ℤ) (n : ℕ) : Odd n → n ≥ 5 → x ^ 2 + 7 = 2 ^ n → (x ^ 2 + 7) / 4 = 2 ^ (n - 2)

theorem expand_by_binomial (m : ℕ) (hm_ge : m ≥ 3) (h : -2 * θ + 1 = θ ^ m - θ' ^ m) : -2 ^ (m - 1) % 7 = ↑m % 7

From -2θ + 1 = θ^m - θ'^m, expand via the binomial theorem and reduce modulo 7 to obtain -2^(m-1) ≡ m (mod 7).

theorem odd_case_mod_seven_constraint (x : ℤ) (n : ℕ) : Odd n → n ≥ 5 → x ^ 2 + 7 = 2 ^ n → -2 ^ (n - 3) % 7 = (↑n - 2) % 7

Key consequence of unique factorization in ℤ[(1+√-7)/2]: For odd n ≥ 5, if x² + 7 = 2ⁿ, then setting m = n - 2, we have -2^(m-1) ≡ m (mod 7).

theorem odd_case_only_three_values_mod_42 (x : ℤ) (n : ℕ) : Odd n → n ≥ 5 → x ^ 2 + 7 = 2 ^ n → (n - 2) % 42 = 3 ∨ (n - 2) % 42 = 5 ∨ (n - 2) % 42 = 13

From -2^(m-1) ≡ m (mod 7) and 2⁶ ≡ 1 (mod 7), the only solutions are m ≡ 3, 5, or 13 (mod 42).

Skeleton for the uniqueness argument

theorem corollary_C (x₁ x₂ : ℤ) (m₁ m₂ : ℕ) (h₁_odd : Odd m₁) (h₂_odd : Odd m₂) (h₁_ge : m₁ ≥ 3) (h₂_ge : m₂ ≥ 3) (h₁_eq : (x₁ ^ 2 + 7) / 4 = 2 ^ m₁) (h₂_eq : (x₂ ^ 2 + 7) / 4 = 2 ^ m₂) : θ ^ m₁ - θ' ^ m₁ = θ ^ m₂ - θ' ^ m₂

noncomputable def binomial_B (d : ℕ) : ℤ

B_d = Σ_{j=0}^{(d-1)/2} C(d, 2j+1) · (-7)^j.

Equations

• binomial_B d = ∑ j ∈ Finset.range ((d + 1) / 2), ↑(d.choose (2 * j + 1)) * (-7) ^ j

theorem lemma_A_binomial_valuation (d l : ℕ) (hd : d > 0) (h_div : 7 ^ l ∣ ↑d) (h_ndiv : ¬7 ^ (l + 1) ∣ ↑d) : 7 ^ l ∣ binomial_B d ∧ ¬7 ^ (l + 1) ∣ binomial_B d

noncomputable def binomial_A' (d : ℕ) : ℤ

A'd = Σ{j=0}^{d/2-1} C(d, 2(j+1)) · (-7)^j.

Equations

• binomial_A' d = ∑ j ∈ Finset.range (d / 2), ↑(d.choose (2 * (j + 1))) * (-7) ^ j

theorem even_binomial_valuation (d l : ℕ) (hd : d > 0) (h_div : 7 ^ l ∣ ↑d) (h_ndiv : ¬7 ^ (l + 1) ∣ ↑d) (h_7_dvd : 7 ∣ d) : 7 ^ l ∣ binomial_A' d ∧ ¬7 ^ (l + 1) ∣ binomial_A' d

def trace_seq : ℕ → ℤ

a(n) = θ^n + θ'^n, an integer recurrence.

Equations

• trace_seq 0 = 2
• trace_seq 1 = 1
• trace_seq n.succ.succ = trace_seq (n + 1) - 2 * trace_seq n

theorem trace_seq_eq (n : ℕ) : ↑(trace_seq n) = θ ^ n + θ' ^ n

theorem trace_seq_not_dvd_seven (n : ℕ) : ¬7 ∣ trace_seq n

theorem nat_even_iff_not_odd (n : ℕ) : Even n ↔ ¬Odd n

theorem at_most_one_m_per_class (m₁ m₂ : ℕ) (h₁_odd : Odd m₁) (h₂_odd : Odd m₂) (h₁_ge : m₁ ≥ 3) (h₂_ge : m₂ ≥ 3) (h_cong : m₁ % 42 = m₂ % 42) (h₁_theta : -2 * θ + 1 = θ ^ m₁ - θ' ^ m₁) (h₂_theta : -2 * θ + 1 = θ ^ m₂ - θ' ^ m₂) : m₁ = m₂

Each residue class mod 42 has at most one m solving the equation.

theorem theta_eq_at_3 : -2 * θ + 1 = θ ^ 3 - θ' ^ 3

m = 3 is a solution: x = 5, (25+7)/4 = 8 = 2³.

theorem theta_eq_at_5 : -2 * θ + 1 = θ ^ 5 - θ' ^ 5

theorem theta_eq_at_13 : -2 * θ + 1 = θ ^ 13 - θ' ^ 13

theorem odd_case_only_three_values (x : ℤ) (n : ℕ) : Odd n → n ≥ 5 → x ^ 2 + 7 = 2 ^ n → n = 5 ∨ n = 7 ∨ n = 15

For x² + 7 = 2ⁿ with odd n ≥ 5: n ∈ {5, 7, 15}.

theorem sq_odd_then_odd (x : ℤ) : Odd (x ^ 2) → Odd x

theorem two_pow_min_seven_odd (n : ℕ) : n ≠ 0 → Odd (2 ^ n - 7)

theorem x_is_odd (x : ℤ) (n : ℕ) : n ≠ 0 → x ^ 2 + 7 = 2 ^ n → x % 2 = 1

theorem ramanujan_nagell_even_pow_factors (x : ℤ) (k : ℕ) : (2 ^ k + x) * (2 ^ k - x) = 7 → 2 ^ k - x = 1 ∧ 2 ^ k + x = 7 ∨ 2 ^ k - x = 7 ∧ 2 ^ k + x = 1

theorem helper_1 {x : ℤ} {n : ℕ} (h₁ : x ^ 2 = 9) (h₂ : n = 4) : (x, n) = (1, 3) ∨ (x, n) = (-1, 3) ∨ (x, n) = (3, 4) ∨ (x, n) = (-3, 4) ∨ (x, n) = (5, 5) ∨ (x, n) = (-5, 5) ∨ (x, n) = (11, 7) ∨ (x, n) = (-11, 7) ∨ (x, n) = (181, 15) ∨ (x, n) = (-181, 15)

theorem helper_2 {x : ℤ} {n : ℕ} (h₁ : x ^ 2 = 1) (h₂ : n = 3) : (x, n) = (1, 3) ∨ (x, n) = (-1, 3) ∨ (x, n) = (3, 4) ∨ (x, n) = (-3, 4) ∨ (x, n) = (5, 5) ∨ (x, n) = (-5, 5) ∨ (x, n) = (11, 7) ∨ (x, n) = (-11, 7) ∨ (x, n) = (181, 15) ∨ (x, n) = (-181, 15)

theorem omg {n : ℕ} (n_ge_4 : n ≥ 4) (n_ne_4 : n ≠ 4) : n ≥ 5

theorem helper_3 {x : ℤ} {n : ℕ} (h₁ : x ^ 2 = 25) (h₂ : n = 5) : (x, n) = (1, 3) ∨ (x, n) = (-1, 3) ∨ (x, n) = (3, 4) ∨ (x, n) = (-3, 4) ∨ (x, n) = (5, 5) ∨ (x, n) = (-5, 5) ∨ (x, n) = (11, 7) ∨ (x, n) = (-11, 7) ∨ (x, n) = (181, 15) ∨ (x, n) = (-181, 15)

theorem helper_4 {x : ℤ} {n : ℕ} (h₁ : x ^ 2 = 121) (h₂ : n = 7) : (x, n) = (1, 3) ∨ (x, n) = (-1, 3) ∨ (x, n) = (3, 4) ∨ (x, n) = (-3, 4) ∨ (x, n) = (5, 5) ∨ (x, n) = (-5, 5) ∨ (x, n) = (11, 7) ∨ (x, n) = (-11, 7) ∨ (x, n) = (181, 15) ∨ (x, n) = (-181, 15)

theorem helper_5 {x : ℤ} {n : ℕ} (h₁ : x ^ 2 = 32761) (h₂ : n = 15) : (x, n) = (1, 3) ∨ (x, n) = (-1, 3) ∨ (x, n) = (3, 4) ∨ (x, n) = (-3, 4) ∨ (x, n) = (5, 5) ∨ (x, n) = (-5, 5) ∨ (x, n) = (11, 7) ∨ (x, n) = (-11, 7) ∨ (x, n) = (181, 15) ∨ (x, n) = (-181, 15)

theorem RamanujanNagell (x : ℤ) (n : ℕ) : x ^ 2 + 7 = 2 ^ n → (x, n) = (1, 3) ∨ (x, n) = (-1, 3) ∨ (x, n) = (3, 4) ∨ (x, n) = (-3, 4) ∨ (x, n) = (5, 5) ∨ (x, n) = (-5, 5) ∨ (x, n) = (11, 7) ∨ (x, n) = (-11, 7) ∨ (x, n) = (181, 15) ∨ (x, n) = (-181, 15)

The Ramanujan-Nagell theorem.