propositionnovelunresolved_ref

Total variation S cannot stay bounded

Proposition·ht:bounded·§4.3 Excluding bounded total variation

Statement (paper)

For a sequence of the incidence pieces in , with the level spaces and quantities SS in , no subsequence has SS bounded. Consequently S→∞S\to\infty.

In plain English

For a sequence of the incidence pieces, no subsequence has the total variation quantity SS bounded, so S→∞S\to\infty.

Why it's here

The proof argues by contradiction: bounded SS gives a normalization with uniformly bounded heights, and a history predictor from the entropy bound together with a determinant and Cramer's rule argument then yields a contradiction. Ruling out bounded SS is the step that lets the main theorem proceed, since only the regime S→∞S\to\infty remains.
Classified novel:
This is one of the paper's core new steps: ruling out bounded total variation of heights by combining a history predictor from the entropy bound with a determinant/Cramer's rule argument. No prior unit-distance argument uses a height-based dichotomy of this kind, and it is essential to getting below the Szemerédi–Trotter exponent 4/3.

Uses

lemMatching labels are nearly constantlemEdge height cost controls point-pair height costlemBasic properties of the heightlemWedge law has tiny atoms and small informationcorPrefix history predicts acceptance failurespropIncidence piece with degree and expansion control

Used by

thmPower-saving bound for planar unit distances

Inside the proof

claimNormalized coordinates with bounded mean heightsclaimCoupling tail bounds uniform in historyclaimQuantized acceptance tests with a history predictorclaimPositive-probability good outcome existsclaimDeterminant and Cramer's rule contradiction

Sources

PaperOpen
Section
§4.3 Excluding bounded total variation
Page
—
Label
ht:bounded
Line
sections/03-heights.tex:216
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • warn
    unresolved_ref
    Choice of d_0 relies on equation ht:independent-profiles (Tonelli/height identity), not a skeleton statement.