Consecutive quadratic residues: Λ(2, 2) = 9 (Erdős Problem 436, Lehmer–Lehmer 1962)

For a prime p, let r(p) be the least n ≥ 1 such that n and n + 1 are both quadratic residues modulo p. Lehmer and Lehmer (1962) showed that limsup r(p) = 9: for p > 10 one of the pairs (1, 2), (4, 5), (9, 10) works, and when 2, 3, 5, 7 are all non-residues no smaller pair does, which happens for infinitely many primes by Dirichlet's theorem and quadratic reciprocity. This closes the sorry of erdos_436.variants.two_two in google-deepmind/formal-conjectures (definitions copied literally, Apache-2.0).

Main results

• Erdos436.r_le_nine: for every prime p > 10, r(2, 2, p) ≤ 9
• Erdos436.r_eq_nine: r(2, 2, p) = 9 for every prime p ≡ 43 (mod 840)
• Erdos436.erdos_436.variants.two_two: Λ(2, 2) = 9 (formal-conjectures erdos_436.variants.two_two)

References

• D. H. Lehmer, E. Lehmer, «On runs of residues», Proc. Amer. Math. Soc. 13 (1962) 102–106.
• google-deepmind/formal-conjectures, FormalConjectures/ErdosProblems/436.lean (Apache-2.0): definiciones y enunciado.

def Erdos436.IsPowerResidue (k p a : ℕ) : Prop

IsPowerResidue k p a: p ∤ a and a ≡ x^k (mod p) for some x.

Equations

• Erdos436.IsPowerResidue k p a = (↑a ≠ 0 ∧ ∃ (x : ZMod p), x ^ k = ↑a)

noncomputable def Erdos436.r (k m p : ℕ) : ℕ∞

r k m p: the least r ≥ 1 with r, …, r + m − 1 all k-th power residues mod p, or ⊤.

Equations

• Erdos436.r k m p = ⨅ (n : ℕ), ⨅ (_ : 1 ≤ n ∧ ∀ i < m, Erdos436.IsPowerResidue k p (n + i)), ↑n

noncomputable def Erdos436.runLimsup (k m : ℕ) : ℕ∞

Λ(k, m) = limsup_{p → ∞} r(k, m, p) over the primes.

Equations

• Erdos436.runLimsup k m = Filter.limsup (Erdos436.r k m) (Filter.atTop ⊓ Filter.principal {p : ℕ | Nat.Prime p})

theorem Erdos436.natCast_ne_zero {p : ℕ} (hlt : 10 < p) {a : ℕ} (h1 : 1 ≤ a) (h10 : a ≤ 10) : ↑a ≠ 0

theorem Erdos436.isPR_iff {p : ℕ} [Fact (Nat.Prime p)] {a : ℕ} (ha : ↑a ≠ 0) : IsPowerResidue 2 p a ↔ legendreSym p ↑a = 1

theorem Erdos436.L_mul {p : ℕ} [Fact (Nat.Prime p)] (a b : ℕ) : legendreSym p ↑(a * b) = legendreSym p ↑a * legendreSym p ↑b

theorem Erdos436.L_sq {p : ℕ} [Fact (Nat.Prime p)] (a : ℕ) (ha : ↑a ≠ 0) : legendreSym p ↑a * legendreSym p ↑a = 1

theorem Erdos436.r_le {p : ℕ} (n : ℕ) (hn : 1 ≤ n) (h : ∀ i < 2, IsPowerResidue 2 p (n + i)) : r 2 2 p ≤ ↑n

theorem Erdos436.r_le_nine {p : ℕ} (hp : Nat.Prime p) (hlt : 10 < p) : r 2 2 p ≤ 9

theorem Erdos436.r_ge_nine {p : ℕ} (hp : Nat.Prime p) (hlt : 10 < p) (h2 : ¬IsSquare 2) (h3 : ¬IsSquare 3) (h5 : ¬IsSquare 5) (h7 : ¬IsSquare 7) : 9 ≤ r 2 2 p

theorem Erdos436.nonres_of_mod {p : ℕ} (hp : Nat.Prime p) (hm : p % 840 = 43) : ¬IsSquare 2 ∧ ¬IsSquare 3 ∧ ¬IsSquare 5 ∧ ¬IsSquare 7

theorem Erdos436.r_eq_nine {p : ℕ} (hp : Nat.Prime p) (hm : p % 840 = 43) : r 2 2 p = 9

theorem Erdos436.erdos_436.variants.two_two : runLimsup 2 2 = 9

Lehmer–Lehmer (1962): Λ(2, 2) = 9 (the statement erdos_436.variants.two_two of formal-conjectures).