claimroutineinferred_dep

Test-group entries by subset inversion

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

Statement (paper)

For each test group, the coefficient [zi,Si]B‾i(zi,V)∈B[z_{i,S_i}]\overline B_i(z_i,V)\in\mathcal B equals ∑T⊆Si(−1)∣Si∣−∣T∣Bi(1T,V)\sum_{T\subseteq S_i}(-1)^{|S_i|-|T|}B_i(\mathbf1_T,V), and each test-group entry (the product over the group of these coefficients in B\mathcal B) can be evaluated in 2λOk,c(1)2^{\lambda^{O_{k,c}(1)}} bit operations and polynomial space, while the variable-side entries and the checks for invalid wire indices take polynomial time and the graph, degree array, and entry procedures have polynomial-size descriptions.

In plain English

Each coefficient [zi,Si]B‾i(zi,V)[z_{i,S_i}]\overline B_i(z_i,V) equals the alternating sum ∑T⊆Si(−1)∣Si∣−∣T∣Bi(1T,V)\sum_{T\subseteq S_i}(-1)^{|S_i|-|T|}B_i(\mathbf1_T,V) in B\mathcal B. So every test-group entry, a product of such coefficients, can be evaluated in 2λOk,c(1)2^{\lambda^{O_{k,c}(1)}} bit operations and polynomial space. The variable-side entries and invalid-wire checks take polynomial time, and the graph, degree array and entry procedures have polynomial-size descriptions.

Why it's here

This makes the entries from the previous claim's network contractions computable. Möbius (subset) inversion turns each multilinear coefficient into a signed sum over at most 2∣Si∣2^{|S_i|} evaluations of BiB_i, which is affordable because a test group is small. The contraction theorem can then be applied in the next claim to the resulting efficiently described networks to get the total cost.
Classified routine:
Standard Möbius/subset inversion for extracting the coefficient of a multilinear monomial from evaluations at 0/1 points, combined with bookkeeping on evaluation cost and description size for the network from the previous claim.

Uses

lemParity indicator as linear-coefficient h-expansionclaimNetwork contractions sum to branch polynomial

Used by

claimContraction cost gives total running time

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Test-group entries by subset inversion" rests on claim-lem-tensor-sparse-query-4