lemmaroutineinferred_dep

Greedy appended rows give exact count

Lemma·lem:greedy-hashes·§6.2 Choosing additional equations by counting common zeros

Statement (paper)

With

P,D_0

and

A^{(0)}

from Lemma , a deterministic procedure appends

3n

rows of list length

P

and obtains a matrix

A

with

N(A)=\#F

. It uses at most

3n(2m)^P

common-zero counts. Every candidate system has at most

6n

equations, each involving at most

2^k\max(D_0,P)

monomials of degree at most

k

In plain English

Starting from the sparse parity-check matrix

A^{(0)}

of Lemma 6.1, a deterministic procedure appends

3n

rows with list length

P

to get a matrix

A

with

N(A)=\#F

, using at most

3n(2m)^P

common-zero counts. Every candidate system has at most

6n

equations, each with at most

2^k\max(D_0,P)

monomials of degree at most

k

Why it's here

Lemma 6.1 gives sparse checks that rule out all small violation sets, and this lemma adds a few more equations, chosen greedily by counting common zeros, so that the count

N(A)

matches

\#F

exactly. It also bounds the number of counting queries and the size and degree of the resulting equation systems, which the main theorem and the interpolation and leaf-count bounds need for their running-time analysis.

Classified routine:

A greedy method-of-conditional-expectations style choice of hash rows: each row is picked by counting common zeros so that the number of surviving bad violation sets shrinks. It builds directly on the sparse checks of Lemma 6.1 and follows the standard derandomized isolation/hashing argument.

Uses

lemSparse parity checks force large supports

Used by

thmSubexponential deterministic k-CNF model countingpropRunning time of the interpolation counting algorithmclaimLeaf counts via parity rows and queries

Sources

PaperOpen

Section: §6.2 Choosing additional equations by counting common zeros
Page: —
Label: lem:greedy-hashes
Line: main_full_version.tex:3446

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
critique: Lemma 6.2 opens "With $P,D_0$ and $A^{(0)}$ from Lemma " (line 3447). Its proof uses the weight bound |supp v(x)| ≥ m/P from that lemma (line 3470). The DAG has no edge.