claimroutineinferred_dep

Truncation tails consume limited weight

Bounds tail weight: nonzero coefficients force ∑diwi<H/F0\sum d_iw_i<H/F_0
controls the scalars, giving the ν/F0\nu/F_0 term in EtrE_{\rm tr}
Claim·§3.2 Translation to entire functions·inside lemRows reduce to entire-function rows

Statement (paper)

If a coefficient [tk]∏iτi(t)di[t^k]\prod_i\tau_i(t)^{d_i} occurring in is nonzero (with 0≤k≤s0\le k\le s), then ∑idiwi≤v0F0∑idiTi≤v0sF0<HF0\sum_i d_iw_i\le\frac{v_0}{F_0}\sum_i d_iT_i\le\frac{v_0 s}{F_0}<\frac{H}{F_0}.

In plain English

If a coefficient [tk]∏iτi(t)di[t^k]\prod_i\tau_i(t)^{d_i} appearing in the row identity is nonzero with 0≤k≤s0\le k\le s, then the total weight ∑idiwi\sum_i d_iw_i is at most v0F0∑idiTi\frac{v_0}{F_0}\sum_i d_iT_i, which is at most v0sF0\frac{v_0 s}{F_0} and strictly less than HF0\frac{H}{F_0}.

Why it's here

This bounds how much weight the tail factors τi\tau_i can contribute in the exact expansion from the previous claim: a nonzero coefficient of tkt^k with k≤sk\le s forces the tails' total order ∑idiTi\sum_i d_iT_i to be at most ss, and this converts into a weight bound. The following claim uses this to control the size of the scalars ξ\xi, which gives the νH/F0\nu H/F_0 term in EtrE_{\rm tr}.
Classified routine:
This is a direct consequence of the tail orders in claim-det-translation-1: a nonzero coefficient with k≤s requires ∑ᵢdᵢTᵢ≤s. The remaining inequalities follow from the parameter bounds on wᵢ and H.

Uses

claimRows expand around exact periods

Used by

claimCoefficient bound and term count

Sources

PaperOpen
Section
§3.2 Translation to entire functions
Page
—
Label
—
Line
sections/determinant.tex:224
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Truncation tails consume limited weight" rests on claim-det-translation-1