claimroutineinferred_dep

Per-branch cost and total exponent

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

Statement (paper)

For all sufficiently large

n

, on every branch one may use the original precision

\ell=n+1

, and both

\ell

and

m_{\mathrm{test}}

are

O_c(n')

. Then

d_H=O_{k,c}(n'R)

J=O_{k,c}(n'R/Q)+1

, and , in dimension

n'

, has exponent

O_{k,c}\!\left(\frac{n'(\log\log n')^2}{\sqrt{\log n'}}\right)=O_{k,c}\!\left(\frac{n(\log\log n)^2}{\sqrt{\log n}}\right)

. All substitution data, coefficient arrays, and interpolation systems have total representation length

n^{O_{k,c}(1)}

bits, and multiplying the per-branch running time by at most

2^{n/\sqrt\lambda}

leaves this exponential bound unchanged, so summing the branch answers gives the required running time.

In plain English

For large

n

, on every branch the precision can stay at

\ell=n+1

and the parameters

d_H

J

\ell

m_{\mathrm{test}}

are polynomial in

n'

and

R

, so the counting cost has exponent

O_{k,c}(n(\log\log n)^2/\sqrt{\log n})

. All data have size

n^{O_{k,c}(1)}

bits, and summing over at most

2^{n/\sqrt\lambda}

branches keeps this exponent, giving the theorem's running time.

Why it's here

This claim finishes the proof of the theorem. It inserts the concrete sizes of

r

Q

R

D

from the parameter-verification claim into the counting cost from the counting proposition and the general routine. The

2^{n/\sqrt\lambda}

branching overhead is then absorbed into the same exponent, and the polynomial space and representation bounds follow.

Classified routine:

Parameter bookkeeping: it substitutes the per-branch choices of r, Q, R, D from the preceding claim into the cost bounds of prop-count and prop-general-count. The 2^{n/sqrt(lambda)} branching factor is then absorbed into the same exponent.

Uses

claimPer-branch parameters satisfy layout hypothesespropCost of counting solutions via factor evaluationpropGeneral counting routine and its cost

Used by

Nothing in the paper

Sources

PaperOpen

Section: §5.5 Constructing the forms and completing the proof
Page: —
Label: —
Line: main_full_version.tex:3170

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Per-branch running time and total exponent" rests on claim-thm-overview-sparse-polynomials-2
info
inferred_dep
outline: "Per-branch running time and total exponent" rests on prop:count
info
inferred_dep
outline: "Per-branch running time and total exponent" rests on prop:general-count