claimroutineinferred_dep

Division by E_t loses no precision

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

Statement (paper)

For each

t

with

q_t>0

, every factor of

E_t(t+\alpha z)

is a power of

1+\alpha z/(t-q)

, which is integral with constant term one. Hence the reciprocal of

E_t(t+\alpha z)

truncated at order

q_t

is integral, so forming the quotient

\left[F(t+\alpha z)/E_t(t+\alpha z)\right]_{<q_t}

loses no precision.

In plain English

For each

t

with

q_t>0

, every factor of

E_t(t+\alpha z)

is a power of

1+\alpha z/(t-q)

, which is integral with constant term one, so the truncated reciprocal of

E_t(t+\alpha z)

at order

q_t

is integral. Hence the quotient

[F(t+\alpha z)/E_t(t+\alpha z)]_{<q_t}

is computed without losing precision.

Why it's here

This checks the first of the two ingredients in the Hermite formula from the previous claim, namely dividing by

E_t

. Multiplying by an integral series with constant term one is invertible on integral coefficients, so the precision of

F(t+\alpha z)

carries over unchanged to the quotient. This leaves only the multiplication by

E_t(0)

as a source of precision loss in the stated precisions

p_t

Classified routine:

Direct bookkeeping check: a power series with constant term one and integral coefficients has an integral inverse, so truncated division by

E_t

preserves precision. This is a standard fact about formal power series applied to the factors from the previous claim.

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:295

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Quotients by E_t lose no precision" rests on claim-lem-tapered-hermite-1