lemmaroutine

Popular unit circles carry few wedges

Lemma·ext:circles·§7.3 Removing common unit circles and choosing witnesses

Statement (paper)

Call a real unit circle popular if it contains at least t9/10t^{9/10} points of PP. The ordinary wedge probability of p,rp,r lying on a common popular circle is at most t−3/5+o(1)+t−9/5+o(1)+2min⁡q∈Qd(q). t^{-3/5+o(1)}+t^{-9/5+o(1)}+\frac{2}{\min_{q\in Q}d(q)}. This is o(1/(R0log⁡(2R0)))o(1/(R_0\log(2R_0))). In particular, removing such wedges from the set in preserves the lower probability bound , after decreasing its constant.

In plain English

Call a real unit circle popular if it contains at least t9/10t^{9/10} points of PP. The ordinary wedge probability that p,rp,r lie on a common popular circle is at most t−3/5+o(1)+t−9/5+o(1)+2/min⁡q∈Qd(q)t^{-3/5+o(1)}+t^{-9/5+o(1)}+2/\min_{q\in Q}d(q), which is o(1/(R0log⁡(2R0)))o(1/(R_0\log(2R_0))).

Why it's here

This bound shows that wedges lying on popular circles are a negligible fraction, so they can be deleted from the wedge set of the earlier band lemma without losing its lower probability bound beyond a change of constant. The smallness of the bound comes from the parameter choices of the hierarchy lemma, in particular that dQ,min⁡−1d_{Q,\min}^{-1} and the other error terms are tiny, and this clean set of wedges is what the organized pair graph construction then uses.
Classified routine:
A counting estimate bounding wedges on rich unit circles via Szemerédi–Trotter-type incidence bounds for unit circles, compared against the parameter choices of the hierarchy lemma; it is bookkeeping that deletes a negligible set of wedges, not a new idea.

Uses

lemChoice of hierarchy parameters K, L, k

Used by

propOrganized pair graph with height-controlled ratios

Sources

PaperOpen
Section
§7.3 Removing common unit circles and choosing witnesses
Page
—
Label
ext:circles
Line
sections/06-extraction.tex:318
Leannot aligned

Phase 2 aligns this node to a Lean declaration.