claimroutineinferred_dep

Simplex counts calibrate expanded determinant

Counts simplex points

D_A(H)

, so

L_H\to L

, and expands

\Delta_H

into ≤

Q_H^M

terms

sets up the expansion and limit

L

for the case split

Claim·§3.4 A comparison with two alternatives·inside propDeterminant comparison with two savings

Statement (paper)

With

D_A(H)=\#\{a\in\ZZ_{\ge0}^m:wa\le AH\}

and

L_H=\eta^2M/(HD_A(H))

, one has

D_A(H)\sim (AH)^m/(m!\prod_iw_i)

and

L_H\to L

. Moreover, in the expansion of

\Delta_H

by the row identities of Lemma , there are at most

Q_H^M

term choices, and for each choice with indices

a_\rho

the product of the scalar factors has modulus at most

\exp\{-\nu\sum_\rho wa_\rho+\nu MH\bar b+MHE_{\rm tr}\}

, so that Lemma applies to each term choice.

In plain English

The number

D_A(H)

of lattice points

a\in\ZZ_{\ge0}^m

with

wa\le AH

grows like

(AH)^m/(m!\prod_i w_i)

, so

L_H=\eta^2M/(HD_A(H))

tends to

L

. Expanding

\Delta_H

row by row via the translation lemma gives at most

Q_H^M

term choices, each with scalar factors bounded by

\exp\{-\nu\sum_\rho wa_\rho+\nu MH\bar b+MHE_{\rm tr}\}

, so the collision lemma applies to each term.

Why it's here

This claim sets up the proof of the comparison proposition. The simplex count asymptotics identify the limit

L

appearing in the budget conditions, and the expansion reduces

\Delta_H

to a bounded number of terms with explicit scalar bounds, each controlled by the collision lemma. The two follow-up claims then split the term choices into many light indices (collisions) and many heavy indices (approximation saving).

Classified routine:

The simplex asymptotic is a standard lattice-point volume estimate. The term count and scalar bound follow by expanding the rows using det-translation; det-collision then applies to each choice.

Uses

lemRows reduce to entire-function rowslemRepeated Taylor degrees force determinant decaythmInterpolation with separated weights

Used by

claimMany light indices force collisionsclaimMany heavy indices force approximation saving

Sources

PaperOpen

Section: §3.4 A comparison with two alternatives
Page: —
Label: —
Line: sections/determinant.tex:372

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Simplex counts calibrate expanded determinant" rests on geom:interpolation