QuadraticPopulationContradiction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The large nonexceptional quadratic populations are impossible

The collision estimate uses the integer prime cutoff and the quadratic split-prime estimate. Root equations, separation, and population sizes supply its geometric hypotheses.

theorem OAI.Ostmann.small_kernel_le_split_cutoff line 19
theorem OAI.Ostmann.small_kernel_product_bounds line 29

theorem OAI.Ostmann.no_large_nonexceptional_quadratic_populations line 66

Source documentation

For all sufficiently large scales, two separated prime-difference populations cannot both exceed the split cutoff while carrying small, nonexceptional squarefree kernels about one reduced rational center.

theorem no_large_nonexceptional_quadratic_populations (P : PublishedProgressionInput)
    (H : PublishedRealZeroInput P) (hSiegel : PublishedSiegelBound)
    (C : ℝ) (hM : MertensLowerBound C) :
    ∃ η L₁ : ℝ, 0 < η ∧ η ≤ 1 / 1000 ∧ 0 < L₁ ∧
      ∀ L : ℝ, L₁ ≤ L → ∀ (S T : Finset ℤ) (rootS rootT : ℤ → ℕ)
        (m : ℕ) (h u v : ℤ),
        0 < m → h.natAbs.Coprime m → u ≠ 0 → v ≠ 0 →
        Squarefree u.natAbs → Squarefree v.natAbs →
        (m : ℝ) ≤ Real.exp (η * L) →
        (u.natAbs : ℝ) ≤ Real.exp (η * L) →
        (v.natAbs : ℝ) ≤ Real.exp (η * L) →
        (∀ x ∈ S, u * (rootS x : ℤ) ^ 2 = (m : ℤ) * x - h) →
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedRealZeroInput, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.MertensLowerBound