claimroutineinferred_dep

Parameters computable and checkable in polylog time

Claim·§4.7 Choosing the parameters·inside lemExplicit parameter choice satisfies layout hypotheses

Statement (paper)

Given the numerical values n,M,b,wn,M,b,w, the parameters λ,ν,r,Q,R,τ,ϵ,D\lambda,\nu,r,Q,R,\tau,\epsilon,D of and the endpoints of I\mathcal I can be computed exactly, and the numerical hypotheses of Lemma  together with R⩾32R\ge32, 6R⩽Q6R\le Q and the tail bound can be checked exactly, in poly⁡β(log⁡n)\poly_\beta(\log n) bit operations; for all sufficiently large nn all of these checks pass.

In plain English

From n,M,b,wn,M,b,w, the parameters λ,ν,r,Q,R,τ,ϵ,D\lambda,\nu,r,Q,R,\tau,\epsilon,D and the endpoints of I\mathcal I can be computed exactly, and the layout lemma's numerical hypotheses, R⩾32R\ge32, 6R⩽Q6R\le Q and the binomial tail bound can be verified exactly, using poly⁡β(log⁡n)\poly_\beta(\log n) bit operations; all these checks pass for all sufficiently large nn.

Why it's here

This is the algorithmic half of the parent lemma: it shows the parameter choice is effective and that the checks can be done exactly in polylogarithmic time. Passing for large nn follows from the size bounds and the interval and tail estimates of the two earlier claims, so only finitely many nn can fail.
Classified routine:
Bookkeeping: exact arithmetic on O(log n)-bit numbers and evaluation of a binomial tail sum over polylogarithmically many terms, with eventual success following directly from the asymptotic bounds in the two earlier claims.

Uses

claimParameter orders and balance inequalitiesclaimInterpolation interval captures binomial mass

Used by

Nothing in the paper

Sources

PaperOpen
Section
§4.7 Choosing the parameters
Page
—
Label
—
Line
main_full_version.tex:2828
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Exact computation and checking of parameters" rests on claim-lem-incidence-parameters-1
  • info
    inferred_dep
    outline: "Exact computation and checking of parameters" rests on claim-lem-incidence-parameters-2