claimroutineinferred_dep

Density-maximizing rectangle retains large fractions

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

Statement (paper)

Let U,VU,V be the counting fractions and WW the captured edge fraction of a rectangle maximizing w/(uv)γw/(uv)^\gamma among all induced rectangles with counting fractions u,v≥τ=t−a/8u,v\ge\tau=t^{-a/8}. Then U,V,W≥t−o(a)U,V,W\ge t^{-o(a)}.

In plain English

Among induced rectangles with counting fractions u,v≥τ=t−a/8u,v\ge\tau=t^{-a/8}, take one maximizing w/(uv)γw/(uv)^\gamma. Its counting fractions U,VU,V and captured edge fraction WW are all at least t−o(a)t^{-o(a)}.

Why it's here

The maximizer's ratio is at least that of the full rectangle, which is about 1 since u=v=w=1u=v=w=1. Combining this with the preliminary expansion bound from the previous claim and the cutoff τ=t−a/8\tau=t^{-a/8} forces UU, VV and then WW to be only t−o(a)t^{-o(a)} small, so the maximizer cannot be a tiny piece. This lets later claims compare any rectangle with the maximizer to sharpen the expansion exponent to η\eta.
Classified routine:
This is a direct consequence of the preliminary expansion bound (claim-inc-piece-4), the cutoff τ = t^{-a/8}, and comparison with the full rectangle's ratio. It is the standard density-increment / maximizing-subrectangle bookkeeping step.

Uses

claimPreliminary square-root expansion bound

Used by

claimSharpened expansion bound from maximalityclaimMarginal atom lower bounds by vertex removal

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Density-maximizing rectangle retains large fractions" rests on claim-inc-piece-4