claimroutineinferred_dep

Network contractions sum to branch polynomial

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

Statement (paper)

The element of B\mathcal B inside Sℓ\mathcal S_\ell in equals the sum, over the arrays (bipartite networks) indexing the monomials of FF, of the contractions of these bipartite networks. Here a test-group entry is ∏i∈Tg[zi,Si]B‾i(zi,V)\prod_{i\in\mathcal T_g}[z_{i,S_i}]\overline B_i(z_i,V) in B\mathcal B, and a variable-group entry is ∑x∈{0,1}Xh∏v∈Xhxvbv=2∣{v∈Xh:bv=0}∣(mod2p)\sum_{x\in\{0,1\}^{\mathcal X_h}}\prod_{v\in\mathcal X_h}x_v^{b_v}=2^{|\{v\in\mathcal X_h:b_v=0\}|}\pmod{2^p}.

In plain English

The element of B\mathcal B inside Sℓ\mathcal S_\ell in the branch residue formula equals the sum, over the arrays indexing the monomials of FF, of the contractions of the corresponding bipartite networks. A test-group entry is ∏i∈Tg[zi,Si]B‾i(zi,V)\prod_{i\in\mathcal T_g}[z_{i,S_i}]\overline B_i(z_i,V), and a variable-group entry is ∑x∈{0,1}Xh∏v∈Xhxvbv=2∣{v∈Xh:bv=0}∣(mod2p)\sum_{x\in\{0,1\}^{\mathcal X_h}}\prod_{v\in\mathcal X_h}x_v^{b_v}=2^{|\{v\in\mathcal X_h:b_v=0\}|}\pmod{2^p}.

Why it's here

This identifies the branch count modulo 2p2^p with a sum of tensor-network contractions. It does so by reading each incidence monomial of the multilinear polynomial FF as a bipartite network, with wires from the monomial-indexing claim, test groups on one side and variable groups on the other. The next claims can then compute the entries and apply the contraction theorem to this sum.
Classified routine:
Direct bookkeeping expansion of the multilinear product F over its incidence monomials, regrouped as bipartite network contractions using the indexing from the previous claims; the variable-group sum identity is an elementary calculation.

Uses

claimMultilinear incidence polynomial with linear degreeclaimIndexing monomials with few wires

Used by

claimTest-group entries by subset inversion

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Network contractions sum to the branch polynomial" rests on claim-lem-tensor-sparse-query-2
  • info
    inferred_dep
    outline: "Network contractions sum to the branch polynomial" rests on claim-lem-tensor-sparse-query-3