The Ramanujan-Nagell equation

Stuff

theorem factors_in_R_with_product (x : ℤ) (m : ℕ) (hm_ge : m ≥ 3) (h : (x ^ 2 + 7) / 4 = 2 ^ m) : ∃ (α : NumberField.RingOfIntegers K) (β : NumberField.RingOfIntegers K), α * β = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m * ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m ∧ ↑α - ↑β = 2 * ↑⟨QuadraticAlgebra.omega, is_integral_ω⟩ - 1

Summary

PROVIDED SOLUTION We begin by applying main_factorisation_lemma below. The relationship between m here and n there is m = n - 2. We then have the factorization ((x + √-7)/2) * ((x - √-7)/2) = 2^m = ((1 + √-7)/2)^m * ((1 - √-7)/2)^m which is written in Lean as ((↑x + 2*(↑θ : K) - 1) / 2) * ((↑x - 2*(↑θ : K) + 1) / 2) = (↑θ : K) ^ m * (1 - (↑θ : K)) ^ m. This is a factorization into irreducible elements in the ring of integers of ℚ(√-7) (which is ℤ[θ]). Since the class number is 1, we have unique factorization into irreducibles. Equivalently, the prime elements are the same as the irreducible elements. One shows that the two factors (↑x + 2*(↑θ : K) - 1) / 2) and ((↑x - 2*(↑θ : K) + 1) / 2) are coprime as follows: by uniqueness of factorization, we only need to consider the elements θ and (1 - θ) (the prime factors of 2 in this ring). If either of these divided both factors, then it would divide their difference, which is 2*θ - 1 = √-7, which by taking norms is seen to not be the case. Therefore, by unique factorization, each factor must be equal to one of the two factors on the right up to multiplication by a unit. The units in this ring are just ±1 (use units_pm_one above). Therefore, we obtain the important equation (x ± √-7)/2 = \pm ((1 ± √-7)/2)^m. Eliminating x by taking the difference of these two equations, we obtain the two cases stated in the lemma. There might be several similar cases to deal with at the end to keep track of the signs. The relevant results about unique factorization and UFDs can be found in the NumberTheory and RingTheory folders of mathlib.

theorem conjugate_factors_coprime (α β : NumberField.RingOfIntegers K) (m : ℕ) (h_prod : α * β = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m * ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m) (h_diff : ↑α - ↑β = 2 * ↑⟨QuadraticAlgebra.omega, is_integral_ω⟩ - 1) : IsCoprime α β

Exercise 2: The conjugate factors are coprime in R. The only prime factors of 2 in R are θ and θ' (since 2 = θ·θ' by two_factorisation_R). If either divided both α and β, it would divide their difference 2θ-1 = √(-7), but N(√-7) = 7 is not divisible by N(θ) = 2 or N(θ') = 2.

theorem factor_not_unit_left (α β : NumberField.RingOfIntegers K) (m : ℕ) (h_prod : α * β = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m * ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m) (h_diff : ↑α - ↑β = 2 * ↑⟨QuadraticAlgebra.omega, is_integral_ω⟩ - 1) : ¬IsUnit α

theorem factor_not_unit_right (α β : NumberField.RingOfIntegers K) (m : ℕ) (h_prod : α * β = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m * ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m) (h_diff : ↑α - ↑β = 2 * ↑⟨QuadraticAlgebra.omega, is_integral_ω⟩ - 1) : ¬IsUnit β

theorem eliminate_x_conclude (α β : NumberField.RingOfIntegers K) (m : ℕ) (h_diff : ↑α - ↑β = 2 * ↑⟨QuadraticAlgebra.omega, is_integral_ω⟩ - 1) (h_assoc : (α = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m ∨ α = -⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m) ∨ α = ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m ∨ α = -⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m) (h_prod : α * β = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m * ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m) : 2 * ⟨QuadraticAlgebra.omega, is_integral_ω⟩ - 1 = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m - ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m ∨ -2 * ⟨QuadraticAlgebra.omega, is_integral_ω⟩ + 1 = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m - ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m

Exercise 4: From α = ±θ^m or α = ±θ'^m, use the product relation to determine β, then take the difference α - β = 2θ-1 to eliminate x and obtain the conclusion.

theorem must_have_minus_sign (m : ℕ) (hm_odd : Odd m) (hm_ge : m ≥ 3) (h : 2 * ⟨QuadraticAlgebra.omega, is_integral_ω⟩ - 1 = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m - ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m ∨ -2 * ⟨QuadraticAlgebra.omega, is_integral_ω⟩ + 1 = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m - ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m) : -2 * ⟨QuadraticAlgebra.omega, is_integral_ω⟩ + 1 = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m - ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m

If we know one of (2θ - 1 = θ^m - θ'^m) ∨ (-2θ + 1 = θ^m - θ'^m), then in fact the minus sign must hold: -2*θ + 1 = θ^m - θ'^m. This is proved by reducing modulo θ'^2 and checking which sign is consistent.

theorem main_m_condition (x : ℤ) (m : ℕ) : Odd m → m ≥ 3 → (x ^ 2 + 7) / 4 = 2 ^ m → -2 * ⟨QuadraticAlgebra.omega, is_integral_ω⟩ + 1 = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m - ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m

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

comment

theorem expand_by_binomial (m : ℕ) (hm_odd : Odd m) (hm_ge : m ≥ 3) (h : -2 * ⟨QuadraticAlgebra.omega, is_integral_ω⟩ + 1 = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m - ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ 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).

This follows from the factorization in the ring of integers: ((x+√-7)/2)((x-√-7)/2) = 2^m = ((1+√-7)/2)^m ((1-√-7)/2)^m and unique factorization implies (x±√-7)/2 = ±((1±√-7)/2)^m. The negative sign must occur (proved by considering mod b² where b = (1-√-7)/2). Expanding via binomial theorem yields -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

The following lemmas establish that each residue class mod 42 has at most one solution, via a 7-adic contradiction argument. Together with the mod 42 constraint and known solutions at m = 3, 5, 13, this completes the proof of odd_case_only_three_values.

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₂) : ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m₁ - ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m₁ = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m₂ - ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m₂

Corollary C: Any two solutions of the Ramanujan-Nagell equation produce the same theta expression θ^m - θ'^m = -2θ + 1, since main_m_condition shows the RHS is independent of the particular solution.

noncomputable def binomial_B (d : ℕ) : ℤ

The odd-indexed binomial sum: B_d = Σ_{j=0}^{(d-1)/2} C(d, 2j+1) · (-7)^j. This arises from expanding (1+√-7)^d = A_d + √-7 · B_d.

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

Lemma A: The 7-adic valuation of B_d is exactly l when 7^l ∥ d. The j=0 term of B_d equals d (valuation l), and all higher terms have strictly larger 7-adic valuation (≥ l+1), so by the ultrametric property the sum has valuation exactly l.

theorem lemma_B_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

Lemma B: Same valuation result as Lemma A, used for the conjugate θ'. The sign difference (- instead of +) in (1-√-7)^d = A_d - √-7·B_d is what creates the contradiction when combined with Corollary C.

noncomputable def binomial_A' (d : ℕ) : ℤ

The even-indexed binomial sum A'd = Σ{j=0}^{d/2-1} C(d, 2(j+1)) · (-7)^j. This arises from the even-index part of the expansion of (1+√-7)^d.

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

The 7-adic valuation of A'_d is exactly l when 7^l ∥ d. The j=0 term C(d,2) = d(d-1)/2 has valuation l, and all higher terms have strictly larger 7-adic valuation (≥ l+1).

def trace_seq : ℕ → ℤ

The trace sequence a(n) = θ^n + θ'^n, defined as an integer recurrence. Satisfies a(0) = 2, a(1) = 1, a(n+2) = a(n+1) - 2*a(n).

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) = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ n + ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ n

The trace sequence cast into R equals θ^n + θ'^n.

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

The trace sequence is never divisible by 7.

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 * ⟨QuadraticAlgebra.omega, is_integral_ω⟩ + 1 = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m₁ - ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m₁) (h₂_theta : -2 * ⟨QuadraticAlgebra.omega, is_integral_ω⟩ + 1 = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m₂ - ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m₂) : m₁ = m₂

If two solutions m₁, m₂ satisfy m₁ ≡ m₂ (mod 42) and both give θ^m - θ'^m = -2θ+1, then m₁ = m₂. This is proved by contradiction: if m₁ ≠ m₂, the difference d = |m₂ - m₁| is divisible by 42 (hence by 7), and the 7-adic analysis of Lemmas A and B combined with Corollary C yields a contradiction on the valuation of √-7 · B_d.

PROVIDED SOLUTION

1. WLOG m₂ > m₁ (else swap or they're equal). │
2. Let d = m₂ - m₁, which is divisible by 42, hence by 7. │
3. Let l = v₇(d). │
4. From corollary_C (via h₁_theta, h₂_theta): θ^m₁ - θ'^m₁ = θ^m₂ - θ'^m₂. │
5. Expand using binomial sums: this forces B_{m₂} = 2^d · B_{m₁}, equivalently B_d has certain 7-adic properties. │
6. From lemma_A_binomial_valuation: v₇(B_d) = l exactly. │
7. The identity (2θ-1)² = -7 means v_p(√-7) = 1 where p = (2θ-1). │
8. For d ∈ ℤ: v_p(d) = 2·v₇(d) = 2l (always even). │
9. Need v_p(d · √-7) ≥ 2(l+1) but v_p(d · √-7) = 2l+1 < 2l+2. Contradiction.

theorem theta_eq_at_3 : -2 * ⟨QuadraticAlgebra.omega, is_integral_ω⟩ + 1 = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ 3 - ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ 3

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

theorem theta_eq_at_5 : -2 * ⟨QuadraticAlgebra.omega, is_integral_ω⟩ + 1 = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ 5 - ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ 5

Verification: m = 5 (i.e. n = 7) is a solution, via x = 11: (121+7)/4 = 32 = 2⁵.

theorem theta_eq_at_13 : -2 * ⟨QuadraticAlgebra.omega, is_integral_ω⟩ + 1 = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ 13 - ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ 13

Verification: m = 13 (i.e. n = 15) is a solution, via x = 181: (32761+7)/4 = 8192 = 2¹³.

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

For the original equation x² + 7 = 2ⁿ with odd n ≥ 5, the only possible values of n are 5, 7, and 15.

PROOF: From the mod 42 constraint, m = n-2 is congruent to 3, 5, or 13 mod 42. The verification lemmas show these are actual solutions (at m=3,5,13). The uniqueness lemma at_most_one_m_per_class shows each residue class has at most one solution. Therefore n ∈ {5, 7, 15}.

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

theorem not_odd_two_pow (n : ℕ) : n ≠ 0 → ¬Odd (2 ^ n)

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: If x and n are integers satisfying x ^ 2 + 7 = 2 ^ n, then (x, n) = (±1, 3), (±3, 4), (±5, 5), (±11, 7) or (±181, 15).