claimroutineinferred_dep

Contraction cost gives total running time

Claim·§D.3 Arbitrary clause density·inside lemCounting zeros of sparse polynomial systems

Statement (paper)

Applying Theorem  with size parameter s=nνs=n\nu, root precision p=n+1p=n+1, and truncation order ℓ=n+1\ell=n+1, each contraction takes nOk,c(1)2Ok,c(s/log⁡s)n^{O_{k,c}(1)}2^{O_{k,c}(s/\sqrt{\log s})} bit operations and polynomial space, where s/log⁡s=O(nν/λ)s/\sqrt{\log s}=O(n\nu/\sqrt\lambda). Including the high-incidence branches and degree arrays, which multiply the running time by at most 2n/λ+Ok,c(nlog⁡n)=2Ok,c(nν/λ)2^{n/\sqrt{\lambda}+O_{k,c}(\sqrt n\log n)}=2^{O_{k,c}(n\nu/\sqrt{\lambda})}, summing the contractions in B\mathcal B on each branch, applying Sℓ\mathcal S_\ell, and adding the branch residues modulo 2n+12^{n+1} recovers the number of common zeros, within the claimed time and space bounds.

In plain English

Applying the tensor contraction theorem with s=nνs=n\nu, root precision n+1n+1 and truncation order n+1n+1 makes each contraction cost nOk,c(1)2O(nν/λ)n^{O_{k,c}(1)}2^{O(n\nu/\sqrt\lambda)} bit operations in polynomial space. Summing over all branches and degree arrays, then reducing modulo 2n+12^{n+1}, yields the number of common zeros within the lemma's time and space bounds.

Why it's here

This is the closing step of the proof. The earlier claims reduce the count to a sum of low-degree network contractions with efficiently computable entries, so the contraction theorem applies to each. The extra factor from the high-incidence branches and degree arrays is only 2O(nν/λ)2^{O(n\nu/\sqrt\lambda)}, so the total stays within the stated bounds.
Classified routine:
Direct bookkeeping: plugs parameters into the paper's tensor contraction theorem and multiplies by the branch and degree-array counts established in the earlier claims.

Uses

thmSubexponential Boolean tensor network contractionclaimIndexing monomials with few wiresclaimTest-group entries by subset inversion

Used by

Nothing in the paper

Sources

PaperOpen
Section
§D.3 Arbitrary clause density
Page
—
Label
—
Line
quantitative-reduction.tex:294
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Apply contraction theorem and total cost" rests on claim-lem-tensor-sparse-query-3
  • info
    inferred_dep
    outline: "Apply contraction theorem and total cost" rests on claim-lem-tensor-sparse-query-5