lemmaunknowninferred_dep

Repeated Taylor degrees force determinant decay

Bounds

|\det T|

e^{-c\sum n_a^2+\dots}

: repeated Taylor indices shrink it

supplies the quadratic collision saving

Lemma·det:collision·§3.3 Repeated Taylor degrees force a quadratic saving

Statement (paper)

Choose one translated test row from each row expansion in Lemma , and remove its scalar factor. Let

T

be the resulting square matrix, and let

n_a

be the number of its rows with index

a

. With

c=\frac{\log2}{4},\qquad E_{\rm hol}=\frac{100K}{w_0}+\frac{\log2}{v_0} +\frac{\log(200K)}{w_*},

there is a quantity

\rho_H\to0

, independent of all these row choices and of the selected columns, such that

|\det T| \le\exp\left\{-c\sum_a n_a^2+MH(E_{\rm hol}+\rho_H)\right\}.

In plain English

After picking one translated test row from each row expansion and stripping its scalar factor, the resulting square matrix

T

satisfies

|\det T|\le\exp\{-c\sum_a n_a^2+MH(E_{\rm hol}+\rho_H)\}

, where

n_a

counts rows with index

a

c=\frac{\log 2}{4}

, and

\rho_H\to0

does not depend on the row choices or the selected columns.

Why it's here

This is the quadratic saving: when many rows share the same index

a

, they are forced to be nearly dependent, so the determinant shrinks like

e^{-c\,n_a^2}

for each index. It acts on the entire-function test rows produced by the translation lemma, and the determinant comparison and the final contradiction use it to turn index collisions into a determinant bound.

Uses

lemRows reduce to entire-function rows

Used by

propDeterminant comparison with two savingsclaimCombined error margins contradict determinant comparisonclaimSimplex counts calibrate expanded determinantclaimMany light indices force collisions

Sources

PaperOpen

Section: §3.3 Repeated Taylor degrees force a quadratic saving
Page: —
Label: det:collision
Line: sections/determinant.tex:267

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
critique: The collision lemma explicitly chooses rows from the expansion in Lemma 3.2 (sections/determinant.tex:267–270).