claimroutineinferred_dep

Stated precisions recover F(0) mod 2^p

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

Statement (paper)

Reducing each quotient coefficient of F(t+αz)F(t+\alpha z) modulo 2pt2^{p_t}, that is, replacing it by an arbitrary lift of its residue modulo 2pt2^{p_t} with pt=p+8hDt+8M(a+1)p_t=p+8hD_t+8M(a+1), changes its contribution in by an element of 2pA2^p\mathcal A. Consequently the reconstructed sum is integral and differs from F(0)F(0) by an element of 2pA2^p\mathcal A, so F(0)F(0) modulo 2p2^p is recovered from the stated precisions.

In plain English

Reducing each quotient coefficient of F(t+αz)F(t+\alpha z) modulo 2pt2^{p_t}, with pt=p+8hDt+8M(a+1)p_t=p+8hD_t+8M(a+1), changes the reconstructed sum for F(0)F(0) only by an element of 2pA2^p\mathcal A. So the sum is integral and agrees with F(0)F(0) modulo 2p2^p.

Why it's here

This is the precision bookkeeping step that finishes the lemma's recovery claim. Division by EtE_t loses no precision, and multiplying by Et(0)E_t(0) loses at most 6Dth6D_th bits of 2-adic precision, which the extra 8hDt8hD_t in ptp_t covers. The remaining 8M(a+1)8M(a+1) is the slack in ptp_t that absorbs the other multipliers in the formula.
Classified routine:
Precision bookkeeping that combines the two earlier claims (division by E_t loses no 2-adic precision, and E_t(0) loses at most 6D_t h bits) with the slack 8M(a+1) built into p_t. It follows directly from the Hermite interpolation formula by a standard 2-adic valuation count.

Uses

claimDivision by E_t loses no precisionclaimTwo-adic loss of E_t(0) is at most 6Dh

Used by

claimRecovery runs in polynomial time

Sources

PaperOpen
Section
§D.4.4 Tapered Hermite recovery
Page
—
Label
—
Line
quantitative-contraction.tex:318
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Stated precisions recover F(0) mod 2^p" rests on claim-lem-tapered-hermite-2
  • info
    inferred_dep
    outline: "Stated precisions recover F(0) mod 2^p" rests on claim-lem-tapered-hermite-3