lemmaroutine

Explicit parameter choice satisfies layout hypotheses

Lemma·lem:incidence-parameters·§4.7 Choosing the parameters

Statement (paper)

Fix an integer β⩾1\beta\ge1. Let n⩾20n\ge20, put λ=⌈log⁡2n⌉\lambda=\lceil\log_2 n\rceil and ν=⌈log⁡2λ⌉\nu=\lceil\log_2\lambda\rceil, and suppose b,w⩽λβb,w\le\lambda^\beta and n⩽M⩽bnn\le M\le bn. For all sufficiently large nn, the parameters r=⌊λν2⌋,Q=⌊λ128ν⌋,R=(β+3)⌈λ⌉, r=\left\lfloor\frac{\sqrt\lambda}{\nu^2}\right\rfloor, \qquad Q=\left\lfloor\frac{\lambda}{128\nu}\right\rfloor, \qquad R=(\beta+3)\lceil\sqrt\lambda\rceil, τ=1rλ,ϵ=1br2λ,D=r2Q, \tau=\frac1{r\lambda},\qquad \epsilon=\frac1{br^2\lambda},\qquad D=r^{2Q}, together with the interval specified in the proof, satisfy all numerical hypotheses of Lemma . They also satisfy R⩾32,6R⩽Q,D⩽2λ/128, R\ge32,\qquad 6R\le Q,\qquad D\le2^{\lambda/128}, and RQlog⁡2QR+τlog⁡(2D+1)+1r=Oβ ⁣(ν2λ). \frac RQ\log\frac{2Q}{R}+\tau\log(2D+1)+\frac1r =O_\beta\!\left(\frac{\nu^2}{\sqrt\lambda}\right). Given the numerical values n,M,b,wn,M,b,w, the parameters and numerical hypotheses can be computed and checked exactly in poly⁡β(log⁡n)\poly_\beta(\log n) bit operations. For fixed β\beta, only finitely many nn fail these checks.

In plain English

For fixed β\beta and large nn, with λ=⌈log⁡2n⌉\lambda=\lceil\log_2 n\rceil, ν=⌈log⁡2λ⌉\nu=\lceil\log_2\lambda\rceil, b,w⩽λβb,w\le\lambda^\beta and n⩽M⩽bnn\le M\le bn, the explicit choices rr, QQ, RR, τ\tau, ϵ\epsilon, D=r2QD=r^{2Q} and an interval of RR integers meet every numerical hypothesis of the layout lemma. They also give R⩾32R\ge32, 6R⩽Q6R\le Q, D⩽2λ/128D\le2^{\lambda/128}, and the cost sum RQlog⁡2QR+τlog⁡(2D+1)+1r=Oβ(ν2/λ)\frac RQ\log\frac{2Q}{R}+\tau\log(2D+1)+\frac1r=O_\beta(\nu^2/\sqrt\lambda), all checkable in poly⁡β(log⁡n)\poly_\beta(\log n) bit operations.

Why it's here

This lemma turns the layout lemma's abstract parameter requirements into concrete values with a cost of order ν2/λ\nu^2/\sqrt\lambda, which the sparse-polynomial counting results use directly. Its proof fixes the orders of rr, QQ, RR, shows the interval captures the binomial mass up to ϵ\epsilon, bounds the three cost terms, and observes that all checks are exact and run in polylogarithmic time, so only finitely many nn can fail.
Classified routine:
Explicit parameter calculation verifying the numerical hypotheses of the paper's layout lemma; it consists of asymptotic estimates (binomial tail mass, logarithmic bounds) and bookkeeping rather than a new idea.

Uses

Nothing else in the paper

Used by

thmCounting zeros of sparse polynomials fasterclaimPer-branch parameters satisfy layout hypothesesclaimNumerical checks with exhaustive fallback

Inside the proof

claimParameter orders and balance inequalitiesclaimInterpolation interval captures binomial massclaimThree cost terms are balancedclaimParameters computable and checkable in polylog time

Sources

PaperOpen
Section
§4.7 Choosing the parameters
Page
—
Label
lem:incidence-parameters
Line
main_full_version.tex:2747
Leannot aligned

Phase 2 aligns this node to a Lean declaration.