propositionnovelinferred_dep

Incidence piece with degree and expansion control

Proposition·inc:piece·§2.3 Degree control and a maximizing rectangle

Statement (paper)

From a sequence of n=t3n=t^3 real planar points with at least t4−o(1)t^{4-o(1)} ordered unit pairs, one can obtain real algebraic point and center sets P,QP,Q, and a nonempty graph E⊆P×QE\subseteq P\times Q consisting of unit incidences, with the following properties. There is a parameter a=a(t)>0a=a(t)>0 such that a→0a\to0, alog⁡t→∞a\log t\to\infty, and ∣P∣=t1+2a+o(a),∣Q∣=t2+a+o(a),∣E∣=t2+2a+o(a). |P|=t^{1+2a+o(a)},\qquad |Q|=t^{2+a+o(a)},\qquad |E|=t^{2+2a+o(a)}. Writing d(p),d(q)d(p),d(q) for graph degrees, uniformly over all vertices, d(p)=t1+o(a),d(q)=ta+o(a). d(p)=t^{1+o(a)},\qquad d(q)=t^{a+o(a)}. The uniform law on EE has marginals μ(p)=d(p)/∣E∣\mu(p)=d(p)/|E| and κ(q)=d(q)/∣E∣\kappa(q)=d(q)/|E| satisfying μ(p)≥γ∣P∣,κ(q)≥γ∣Q∣,γ=2750=0.54. \mu(p)\ge\frac{\gamma}{|P|},\qquad \kappa(q)\ge\frac{\gamma}{|Q|},\qquad \gamma=\frac{27}{50}=0.54. Set η=γ−12=1/25\eta=\gamma-\tfrac12=1/25. There is a single sequence ξt→0\xi_t\to0 such that, for every F⊆PF\subseteq P and G⊆QG\subseteq Q, with counting fractions u=∣F∣/∣P∣u=|F|/|P| and v=∣G∣/∣Q∣v=|G|/|Q|, PE(p∈F,q∈G)≤uv((uv)η+ξt). \Prob_E(p\in F,q\in G) \le \sqrt{uv}\bigl((uv)^\eta+\xi_t\bigr). The sequence ξt\xi_t is independent of the chosen subsets.

In plain English

From n=t3n=t^3 points with at least t4−o(1)t^{4-o(1)} ordered unit pairs, one extracts algebraic point and center sets P,QP,Q and a nonempty unit-incidence graph E⊆P×QE\subseteq P\times Q with ∣P∣=t1+2a+o(a)|P|=t^{1+2a+o(a)}, ∣Q∣=t2+a+o(a)|Q|=t^{2+a+o(a)}, ∣E∣=t2+2a+o(a)|E|=t^{2+2a+o(a)}. Degrees are uniform (d(p)=t1+o(a)d(p)=t^{1+o(a)}, d(q)=ta+o(a)d(q)=t^{a+o(a)}), every marginal atom is at least γ/∣P∣\gamma/|P| or γ/∣Q∣\gamma/|Q| with γ=27/50\gamma=27/50, and for all F⊆PF\subseteq P, G⊆QG\subseteq Q the edge mass satisfies PE(p∈F,q∈G)≤uv((uv)η+ξt)\Prob_E(p\in F,q\in G)\le\sqrt{uv}((uv)^\eta+\xi_t) with η=1/25\eta=1/25 and ξt→0\xi_t\to0 independent of the subsets.

Why it's here

This is the structural reduction on which the rest of the argument rests: it replaces an arbitrary unit-distance configuration by a nearly regular incidence graph that is also a strong two-sided expander. The algebraic specialization makes the points algebraic, and the cutting lemma and unit-circle Szemerédi–Trotter bound produce a small piece with many incidences, which trimming makes nearly regular. A density-maximizing rectangle then yields the expansion bound and the lower bounds on marginal atoms, which the later matching, rare-event, entropy and history arguments use.
Classified novel:
The core structural reduction of the paper: it combines known tools (algebraic specialization, cutting, Szemerédi–Trotter for unit circles) with a new density-maximizing rectangle argument to extract a nearly regular incidence piece with a two-sided expansion bound. No prior unit-distance work supplies this expander structure.

Uses

lemUnit distances persist under algebraic perturbationlemRandom-sampling cutting for unit circlespropSzemerédi–Trotter bound for unit circles

Used by

thmPower-saving bound for planar unit distanceslemMatching labels are nearly constantlemRare sets carry little edge masslemWedge law has tiny atoms and small informationpropTotal variation S cannot stay boundedclaimPositive-probability good outcome existsclaimLayer-cake bound on capped min-expectation

Inside the proof

claimCutting deletion loses few incidencesclaimSome small piece carries many incidencesclaimTrimming high-degree vertices gives degree boundsclaimPreliminary square-root expansion boundclaimDensity-maximizing rectangle retains large fractionsclaimSharpened expansion bound from maximalityclaimMarginal atom lower bounds by vertex removal

Sources

PaperOpen
Section
§2.3 Degree control and a maximizing rectangle
Page
—
Label
inc:piece
Line
sections/01-incidence.tex:176
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    The proof invokes ('the incidence bound') for the edge upper bound, the degree deletions and the preliminary expansion; that equation is the bound of Proposition 2.3.