claimroutineinferred_dep

Many light indices force collisions

Many light indices force ∑na2≥MHLH\sum n_a^2\ge MHL_H, giving saving −cLH-cL_H
collision case of the term dichotomy
Claim·§3.4 A comparison with two alternatives·inside propDeterminant comparison with two savings

Statement (paper)

Suppose that, for a choice of terms with indices aρa_\rho, at least ηM\eta M of the indices obey wa≤AHwa\le AH. Then ∑ana2≥(ηM)2/DA(H)=MHLH\sum_a n_a^2\ge (\eta M)^2/D_A(H)=MHL_H, and, after division by MHMH, the bound given by Lemma  for this term choice is at most −cLH+Ean+ρH-cL_H+E_{\rm an}+\rho_H.

In plain English

If, for some choice of terms, at least ηM\eta M of the indices aρa_\rho satisfy wa≤AHwa\le AH, then ∑ana2≥(ηM)2/DA(H)=MHLH\sum_a n_a^2\ge(\eta M)^2/D_A(H)=MHL_H. After dividing by MHMH, the collision lemma's bound for that term choice is at most −cLH+Ean+ρH-cL_H+E_{\rm an}+\rho_H.

Why it's here

Light indices live in the simplex wa≤AHwa\le AH, which has only DA(H)D_A(H) lattice points, so by pigeonhole (Cauchy–Schwarz) many rows must share indices, giving a large ∑ana2\sum_a n_a^2. Feeding this into the collision lemma yields the −cLH-cL_H saving for these term choices, which is the first of the two cases the comparison proposition needs to beat the arithmetic lower bound.
Classified routine:
Cauchy–Schwarz applied to the at most DA(H)D_A(H) light indices gives the collision count; substituting it into the earlier det-collision lemma yields the stated saving.

Uses

claimSimplex counts calibrate expanded determinantlemRepeated Taylor degrees force determinant decay

Used by

claimMany heavy indices force approximation savingclaimEither saving defeats arithmetic lower bound

Sources

PaperOpen
Section
§3.4 A comparison with two alternatives
Page
—
Label
—
Line
sections/determinant.tex:393
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Many light indices force collisions" rests on claim-det-comparison-1
  • info
    inferred_dep
    outline: "Many light indices force collisions" rests on det:collision