claimroutineinferred_dep

Some small piece carries many incidences

Claim·§2.3 Degree control and a maximizing rectangle·inside propIncidence piece with degree and expansion control

Statement (paper)

After the deletion, each remaining region meets at most

t^{2+a}

circles, and its assigned point set is split into sets of size at most

2t^{1+2a}

, so that the total number of pieces is at most

t^{2-2a+o(a)}

. Some piece, with vertex sets

P_0,Q_0

and edge count

e_0

, satisfies

|P_0|\le 2t^{1+2a}

|Q_0|\le t^{2+a}

and

t^{2+2a-o(a)}\le e_0\le t^{2+2a+o(a)}

, where the upper bound follows from .

In plain English

After the cutting deletion, each region meets at most

t^{2+a}

circles and its points are split into chunks of size at most

2t^{1+2a}

, giving at most

t^{2-2a+o(a)}

pieces in total. Some piece with vertex sets

P_0,Q_0

has

|P_0|\le 2t^{1+2a}

|Q_0|\le t^{2+a}

and between

t^{2+2a-o(a)}

and

t^{2+2a+o(a)}

incidences.

Why it's here

The previous claim shows that

t^{4-o(a)}

incidences survive the deletion. Spreading them over at most

t^{2-2a+o(a)}

pieces forces some piece to carry at least

t^{2+2a-o(a)}

of them (pigeonhole). The Szemerédi–Trotter bound for unit circles caps every piece's count at

t^{2+2a+o(a)}

, so this piece has the claimed edge count. The next claim trims high-degree vertices in this piece to reach the degree bounds.

Classified routine:

Pigeonhole over the pieces produced by the cutting lemma, combined with the earlier claim on surviving incidences and the Szemerédi–Trotter-type bound for unit circles. This is standard bookkeeping in cutting arguments.

Uses

claimCutting deletion loses few incidencespropSzemerédi–Trotter bound for unit circles

Used by

claimTrimming high-degree vertices gives degree bounds

Sources

PaperOpen

Section: §2.3 Degree control and a maximizing rectangle
Page: —
Label: —
Line: sections/01-incidence.tex:221

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Some small piece carries many incidences" rests on claim-inc-piece-1
info
inferred_dep
outline: "Some small piece carries many incidences" rests on inc:incidence