claimroutineinferred_dep

Two-adic loss of E_t(0) is at most 6Dh

Claim·§D.4.4 Tapered Hermite recovery·inside lemTapered Hermite recovery of F(0)

Statement (paper)

For

t\in S\setminus\{0\}

with

i=v_2(t)

and

D=D_t=L/2^i

, one has

v_2(E_t(0))=\sum_{q\ne0,t}q_q\bigl(v_2(q)-v_2(t-q)\bigr)=D\sum_{j=1}^{a-i}\frac{j}{2^j}\bigl(q(i+j)-q(i)\bigr)\ge -6Dh.

In plain English

For

t\in S\setminus\{0\}

with

i=v_2(t)

and

D=D_t=L/2^i

, the 2-adic valuation of

E_t(0)

equals

\sum_{q\ne0,t}q_q\,(v_2(q)-v_2(t-q))

, which can be rewritten as

D\sum_{j=1}^{a-i}\frac{j}{2^j}(q(i+j)-q(i))

and is at least

-6Dh

Why it's here

This bounds how much 2-adic precision is lost when the Hermite formula multiplies by

E_t(0)

, so

E_t(0)

has valuation no worse than

-6Dh

. The following claim uses this bound, together with the extra

8hD_t

p_t

, to show the stated precisions

p_t

are enough to recover

F(0)

modulo

2^p

. The proof computes the valuation as a sum over the other points weighted by the tapered multiplicities, regroups it by 2-adic level of

t

, and bounds the regrouped sum using the shape of

q(i)=h\max(0,u-i)

Classified routine:

A direct 2-adic valuation calculation on the Hermite interpolation coefficients. It regroups the sum by 2-adic level and bounds it using the explicit form q(i)=h max(0,u-i), which is standard bookkeeping following the earlier claim's setup.

Uses

claimTapered multiplicities permit Hermite recovery of F(0)

Used by

claimStated precisions recover F(0) mod 2^p

Sources

PaperOpen

Section: §D.4.4 Tapered Hermite recovery
Page: —
Label: —
Line: quantitative-contraction.tex:301

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Two-adic loss of E_t(0) at most 6Dh" rests on claim-lem-tapered-hermite-1