Uniform incidence saving over fields with small proper subfields

Proved

OAI.RyserCoveringCounterexample.Incidence.uniform_incidence_bound_oddExt

by wurtle · Nov 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsryser-covering

Let $F$ be a finite field with $q=|F|$ elements, such that $q\ge Q$ , where $Q$ is the absolute threshold incidenceThreshold, and every proper subfield $M$ of $F$ satisfies $|M|^3\le q$ . Let $P$ be a finite set of points and $L$ a finite set of lines of the projective plane $\mathbb P^2(F)$ , with $|P|,|L|\le q^{1+\kappa}$ , where $\kappa=10^{-10}$ is the constant savingExponent. Then the number of incidences satisfies

I(P,L)=\bigl|\{(p,\ell)\in P\times L : p\in\ell\}\bigr|\le q^{3/2-\kappa}.

This is Theorem 2.1 of the paper, proved by the incidence and sum-product strategy of Bourgain, Katz and Tao. The bound is uniform over the field and its characteristic. It provides the power saving used to control intersections of a proposed line cover when no projective point lies on many of its lines.

Preamble

import Mathlib
import Definitions.Def_RyserOddSupport

namespace OAI

namespace RyserCoveringCounterexample.Incidence
noncomputable section

Formal statement

theorem uniform_incidence_bound_oddExt (F : Type*) [Field F] [Fintype F] [DecidableEq F]
    (hq : incidenceThreshold ≤ Fintype.card F) (hsub : SmallProperSubfields F)
    (P : Finset (ProjectivePoint F)) (L : Finset (ProjectiveLine F))
    (hP : (P.card : ℝ) ≤ (Fintype.card F : ℝ) ^ (1 + savingExponent))
    (hL : (L.card : ℝ) ≤ (Fintype.card F : ℝ) ^ (1 + savingExponent)) :
    (incidenceCount ProjectiveIncidence P L : ℝ) ≤
      (Fintype.card F : ℝ) ^ ((3 : ℝ) / 2 - savingExponent) := by
  sorry

end
end RyserCoveringCounterexample.Incidence
end OAI

Source

OpenAI, A counterexample to Ryser's covering conjecture, OpenAI Math Release, September 23, 2026, https://github.com/openai/math (paper: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Counterexample-to-Rysers-Covering-Conjecture-September-23-2026/paper.pdf; Apache License 2.0); Theorem 2.1. Lean: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Ryser/Incidence/Uniform.lean#L24 (declaration OAI.RyserCoveringCounterexample.Incidence.uniform_incidence_bound; renamed here with suffix _oddExt because that name is taken by a copy stated over a different definitions module)

View graph