claimroutineinferred_dep
Leaf counts via parity rows and queries
Statement (paper)
For every nontrivial leaf of the tree, the leaf count can be computed by taking the initial parity checks of Lemma and running the greedy procedure of Lemma , where each greedy step computes for every candidate row via Lemma and appends one attaining the minimum, and one final call gives for the selected matrix, which equals the leaf count. Every row gives a degree-at-most- equation with at most monomials, and every queried system has at most equations, with a single constant bounding both the ratio of equations to variables and the exponent of in the monomial bound for all sufficiently large .
In plain English
For each nontrivial leaf of the sparsification tree, its model count is obtained by building sparse parity checks, greedily appending rows with counting queries, and making a final query for , which equals the leaf count. All queried systems have at most equations of degree at most with at most monomials each, so one constant bounds both the equation-to-variable ratio and the monomial exponent for large .
Why it's here
This combines the sparse checks of Lemma 6.1 and the greedy construction of Lemma 6.2, using the leaf sparsity from the previous claim (occurrence bound ). It checks that every query fits the hypotheses of the sparse-system counting lemma (linearly many equations, polylogarithmically many monomials), so each leaf can be counted in subexponential time, which the time and space accounting then uses.
Classified routine:
Direct assembly of the earlier lemmas (sparse checks, greedy hashes, sparse-query counting) with the leaf occurrence bound from the preceding claim. The only work is bookkeeping that the queried systems meet the counting lemma's hypotheses on equation count and monomial count.