lemmaroutine

Layout data is efficiently constructible

Lemma·lem:layout·§4.6 Coefficient bounds and the completed construction

Statement (paper)

Let

n,b,w\ge1

be integers, and let

(I_f)_{f\in\mathcal F}

be subsets of

[n]

of size at most

w

, with each

v\in[n]

belonging to at most

b

sets. Put

M=\sum_f|I_f|

and assume

n\le M\le bn

. Let

r\ge2

and

1\le R<Q

be integers, let

0<\tau\le1/2

, and put

D=r^{2Q}

. Suppose

2(b+w)D^2\le M,\qquad 2Qr^2\le n,

and an interval

\mathcal I=\{A_0,\ldots,A_0+R-1\}\subseteq\{0,\ldots,Q\}

satisfies

\Pr[W\notin\mathcal I]\le\frac{\tau}{rb},\qquad W\sim\operatorname{Bin}\!\left(Q,\frac{r-1}{2r}\right).

One can deterministically construct all the data in Definition in

\poly(n,M,|\mathcal F|,D,Q,r,b,w)

bit operations.

In plain English

Given scopes

I_f\subseteq[n]

of size at most

w

, each variable in at most

b

scopes, with

n\le M\le bn

, together with the stated inequalities on

D=r^{2Q}

Q

r

and a binomial tail bound for an interval

\mathcal I

of length

R

, all the data of the layout definition can be built deterministically in time polynomial in

n,M,|\mathcal F|,D,Q,r,b,w

Why it's here

This lemma assembles the earlier pieces into the completed construction: balanced labels from the incidence-labeling lemma, the swap matrix

C^{\mathcal B}

and support structure of

M_0

, and the bounded row coefficients from the row-coefficients lemma. Its role is to certify that the layout exists under the stated parameter conditions and is computable in polynomial time, which the sparse-polynomial counting theorem and its per-branch design step rely on.

Classified routine:

An assembly lemma: it combines the incidence-labeling, swap-matrix, support and row-coefficient lemmas proved earlier, and only checks that each piece meets the parameter conditions and is computable in polynomial time.

Uses

lemSwap matrix with few rows fixes M_0lemNonzero entries of M_0 have few differing coordinateslemPolynomial rows vanish on off-block vectorslemDeterministic balanced incidence labelinglemRow coefficients are bounded and constructible

Used by

thmCounting zeros of sparse polynomials fasterclaimPer-branch parameters satisfy layout hypotheses

Sources

PaperOpen

Section: §4.6 Coefficient bounds and the completed construction
Page: —
Label: lem:layout
Line: main_full_version.tex:2696

Leannot aligned

Phase 2 aligns this node to a Lean declaration.