← All papers
First page of A dot-product bound from separate growth-minimizing bases

A dot-product bound from separate growth-minimizing bases

Zhipeng Lu

math.CO Sep 6, 2026 · v1
The algebraic core, median lemma, surface identities, and pinned construction of the dot-product bound are formally verified in Lean 4 as ancillary files.
For every finite $P\subset\mathbb{R}^2$ we prove $|\{p\cdot q: p,q\in P\}|\gg |P|^{199/295}$, with an absolute constant and no logarithmic loss, where $199/295 = 2/3+7/885$. This improves the bound $2/3+7/1425$ of Kokkinos (arXiv:2502.12727), which in turn had improved the first superthreshold bound of Hanson, Roche-Newton, and Senger. The main new ingredient is the inequality $|F^{(2)}G^{(2)}/(F^{(2)}G)| \le |AB|(|AF|/|A|)^4(|BG|/|B|)^3$: each radial profile retains its own Petridis growth-minimizing subset, and the product of the two subsets serves as a common base for both growth operators; a prime-power construction shows this is sharp under its hypotheses. The second ingredient is a weighted-median replacement for the dyadic selection in the squeezing argument of Roche-Newton and Wong, upgrading their seven-factor expander to a logarithm-free form; an appendix gives the complete proof from the Solymosi-Zahl incidence theorem. We complement the lower bound with a third-moment structure theorem for near-extremal configurations and a construction showing that the pinned problem admits no linear lower bound: $\max_{p\in P}|p\cdot P| = O(|P|/\sqrt{\log |P|})$ is attainable. The algebraic core, the median lemma, the surface identities, and the pinned construction are formally verified in Lean 4 and included as ancillary files.

For a finite planar point set P, one asks how small the dot-product set {p·q : p,q∈P} can be. The Szemerédi–Trotter threshold gives |P|^(2/3), and improving the superthreshold exponent is the goal.

A new growth inequality lets each radial profile keep its own Petridis growth-minimizing subset, whose product serves as a common base for both growth operators, avoiding a lossy common intersection. A weighted-median replacement for dyadic selection upgrades a seven-factor expander to a logarithm-free form. The algebraic core, median lemma, surface identities, and pinned construction are formally verified in Lean 4.

The paper proves |{p·q : p,q∈P}| ≫ |P|^(199/295) = |P|^(2/3+7/885) with an absolute constant and no logarithmic loss, improving the prior 2/3+7/1425 bound, plus a structure theorem and a pinned construction showing no linear lower bound.