claimroutineinferred_dep

Indexing monomials with few wires

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

Statement (paper)

For each array

(d_{gh})

with

0\le d_{gh}\le N_{gh}

and

\sum_{g,h}d_{gh}\le K

, the subsets of selected incidences can be indexed in lexicographic order by Boolean wires, with decoding in polynomial time and space, so that the number of wires

M

in the network satisfies

M\le J^2+\log_2\binom{N+K}{K}=O_{k,c}(n\nu)

. Moreover, the number of arrays is at most

(K+1)^{J^2}=2^{O_{k,c}(\sqrt n\log n)}

, and the degree of each vertex is at most its number of incidences,

n^{3/4}\lambda^{O_{k,c}(1)}

In plain English

For each array

(d_{gh})

with

0\le d_{gh}\le N_{gh}

and

\sum_{g,h}d_{gh}\le K

, the selected-incidence subsets can be indexed in lexicographic order by Boolean wires, decodable in polynomial time and space, with the number of wires

M\le J^2+\log_2\binom{N+K}{K}=O_{k,c}(n\nu)

. There are at most

(K+1)^{J^2}=2^{O_{k,c}(\sqrt n\log n)}

arrays, and each vertex has degree at most its number of incidences,

n^{3/4}\lambda^{O_{k,c}(1)}

Why it's here

This turns the multilinear incidence polynomial with linear degree

K

from the previous claim into a family of bipartite networks with only

O(n\nu)

wires, each monomial sum being indexed by an array. The small wire count, small number of arrays and bounded vertex degree are the size parameters needed to express the branch count as a sum of network contractions and then to apply the contraction theorem in the later claims.

Classified routine:

Standard combinatorial bookkeeping: lexicographic ranking/unranking of bounded-size subsets (combinatorial number system) encoded in binary wires, plus elementary counting of arrays and degrees from the previous claim's degree bound K.

Uses

claimMultilinear incidence polynomial with linear degree

Used by

claimNetwork contractions sum to branch polynomialclaimContraction cost gives total running time

Sources

PaperOpen

Section: §D.3 Arbitrary clause density
Page: —
Label: —
Line: quantitative-reduction.tex:192

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Indexing monomials with O(n log log n) wires" rests on claim-lem-tensor-sparse-query-2