claimroutineinferred_dep

Per-branch parameters satisfy layout hypotheses

Claim·§5.5 Constructing the forms and completing the proof·inside thmCounting zeros of sparse polynomials faster

Statement (paper)

For all sufficiently large nn, on each branch (with n′⩾n/2n'\ge n/2 free variables, restricted scopes If′I'_f and M′⩾n′M'\ge n'), if r⩾2r\ge2 and Q>RQ>R, then with λ′=⌈log⁡2n′⌉\lambda'=\lceil\log_2 n'\rceil, ν′=⌈log⁡2λ′⌉\nu'=\lceil\log_2\lambda'\rceil, r=⌊λ′/(ν′)2⌋r=\lfloor\sqrt{\lambda'}/(\nu')^2\rfloor, Q=⌊λ′/(128ν′)⌋Q=\lfloor\lambda'/(128\nu')\rfloor, R=(β+3)⌈λ′⌉R=(\beta+3)\lceil\sqrt{\lambda'}\rceil, τ=1/(rλ′)\tau=1/(r\lambda'), ϵ=1/(br2λ′)\epsilon=1/(br^2\lambda') and D=r2QD=r^{2Q}, Lemma  applies and Lemma  supplies the required rows and measurement matrices, with r=Θ(log⁡n′/(log⁡log⁡n′)2)r=\Theta(\sqrt{\log n'}/(\log\log n')^2), Q=Θ(log⁡n′/log⁡log⁡n′)Q=\Theta(\log n'/\log\log n'), R=Ok,c(log⁡n′)R=O_{k,c}(\sqrt{\log n'}) and D⩽(2n′)1/128D\le(2n')^{1/128}.

In plain English

For large nn, on each branch with n′⩾n/2n'\ge n/2 free variables, if r⩾2r\ge2 and Q>RQ>R, the explicit choices of rr, QQ, RR, τ\tau, ϵ\epsilon and D=r2QD=r^{2Q} (in terms of λ′=⌈log⁡2n′⌉\lambda'=\lceil\log_2 n'\rceil) meet the hypotheses of the incidence-parameters lemma, so the layout lemma supplies the needed rows and measurement matrices. These choices satisfy r=Θ(log⁡n′/(log⁡log⁡n′)2)r=\Theta(\sqrt{\log n'}/(\log\log n')^2), Q=Θ(log⁡n′/log⁡log⁡n′)Q=\Theta(\log n'/\log\log n'), R=Ok,c(log⁡n′)R=O_{k,c}(\sqrt{\log n'}) and D⩽(2n′)1/128D\le(2n')^{1/128}.

Why it's here

This claim specializes the generic parameter lemma to a branch, using the bounded variable incidence from the branching step so that the scopes have the bounded size and multiplicity the lemma needs. It fixes the concrete sizes of rr, QQ, RR, DD that the per-branch running-time and total-exponent computation uses.
Classified routine:
Direct parameter bookkeeping: it instantiates the earlier incidence-parameters lemma on each branch, using the bounded incidence from the branching claim, and then reads off the asymptotic sizes of r, Q, R and D.

Uses

lemExplicit parameter choice satisfies layout hypotheseslemLayout data is efficiently constructibleclaimBranch on high-incidence variables

Used by

claimPer-branch cost and total exponent

Sources

PaperOpen
Section
§5.5 Constructing the forms and completing the proof
Page
—
Label
—
Line
main_full_version.tex:3129
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Per-branch design from parameter lemma" rests on claim-thm-overview-sparse-polynomials-1