claimroutineinferred_dep

Multilinear incidence polynomial with linear degree

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

Statement (paper)

The polynomial F(z,V)=∏iB‾i(zi,V)F(z,V)=\prod_i\overline B_i(z_i,V) in B[z]\mathcal B[z] is multilinear in the incidence indeterminates zivz_{iv}, and every incidence monomial in FF has degree at most K=k(a+2(ℓ−1))=Ok,c(n)K=k\bigl(a+2(\ell-1)\bigr)=O_{k,c}(n). Moreover, the branch count is congruent modulo 2p2^p to Sℓ(∑xF((ziv=xv)iv,V))\mathcal S_\ell\left(\sum_x F\bigl((z_{iv}=x_v)_{iv},V\bigr)\right), where xx runs over all free Boolean assignments.

In plain English

The product F(z,V)=∏iB‾i(zi,V)F(z,V)=\prod_i\overline B_i(z_i,V) over B[z]\mathcal B[z] is multilinear in the incidence indeterminates zivz_{iv}, and each incidence monomial has degree at most K=k(a+2(ℓ−1))=Ok,c(n)K=k(a+2(\ell-1))=O_{k,c}(n). Substituting ziv=xvz_{iv}=x_v, summing over all free Boolean assignments xx, and applying Sℓ\mathcal S_\ell gives the branch count modulo 2p2^p.

Why it's here

This is where the truncated-product degree bound of the total-order lemma is applied to the branched system. It turns the branch count into a sum of a multilinear polynomial whose incidence monomials have only linear degree KK. That is the form the later claims need to index monomials with few wires and to express the count as a sum of network contractions.}
Classified routine:
A direct consequence of the truncated-product degree bound (lem-total-order) and the linear-coefficient h-expansion (lem-rational-idempotent), applied to the branched system from the previous claim. Multilinearity follows because Boolean substitution allows reducing z_{iv}^2 to z_{iv}, and the degree bound comes from bookkeeping over the k incidence variables per factor.

Uses

lemParity indicator as linear-coefficient h-expansionlemTruncated product extracts parity indicators with linear degreeclaimBranch on high-incidence variables

Used by

claimIndexing monomials with few wiresclaimNetwork contractions sum to branch polynomial

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Multilinear incidence polynomial with linear degree" rests on claim-lem-tensor-sparse-query-1