propositionroutineinferred_dep

General counting routine and its cost

Proposition·prop:general-count·§3.5 The three exponential costs

Statement (paper)

Let A\mathcal A be a commutative Q\mathbb Q-algebra. Suppose the product of the factors in , computed over A\mathcal A, satisfies the degree bound , and that the replacement rows, partitions, and measurements satisfy Definition . With q,Jq,J as in , the routine computes ZZ by examining at most 2Qr Cq(2D+1)2τn22n/r 2Qr\,C_q(2D+1)^{2\tau n}2^{2n/r} Boolean vectors. For each vector it evaluates at most ∣F∣|\mathcal F| factors in A[z]/(zJ)\mathcal A[z]/(z^J). The additional operations per vector and the final interpolation take polynomially many operations in A\mathcal A and over Q\mathbb Q, in the parameters n,∣F∣,D,Q,R,J,rn,|\mathcal F|,D,Q,R,J,r and the total scope length. Apart from the factor evaluators' own storage, the routine retains only polynomially many algebra elements, rational numbers and index bits.

In plain English

Over a commutative Q\mathbb Q-algebra A\mathcal A, if the factor product obeys the degree bound and the layout satisfies Definition 3.1, then ZZ can be computed by examining at most 2Qr Cq(2D+1)2τn22n/r2Qr\,C_q(2D+1)^{2\tau n}2^{2n/r} Boolean vectors, evaluating at most ∣F∣|\mathcal F| factors in A[z]/(zJ)\mathcal A[z]/(z^J) per vector. The extra work and final interpolation are polynomial in the parameters, and storage beyond the factor evaluators is polynomial.

Why it's here

This packages the three exponential costs into one bound. It combines the Boolean-differences expansion, which replaces evaluation at xx by evaluations at fixed substitutions with at most qq forced coordinates, with the measurement-separation lemma, which splits each resulting sum over the layout's partitions. The (2D+1)2τn(2D+1)^{2\tau n} and 22n/r2^{2n/r} factors come from the measurement count and part sizes in the layout, while the factors QQ, rr and CqC_q come from the points, the groups and the Boolean-differences expansion. Later counting results use it as their running-time and space bound.
Classified routine:
This assembles the paper's earlier Boolean-differences expansion and measurement-separation lemma under the layout definition. The work is a bookkeeping count of vectors, operations and storage, with no new idea of its own.

Uses

lemSeparating sums by fixing measurementslemBoolean sum via fixed substitutionsdefLayout of partitions, measurements, and polynomial rows

Used by

propCost of counting solutions via factor evaluationclaimPer-branch cost and total exponent

Sources

PaperOpen
Section
§3.5 The three exponential costs
Page
—
Label
prop:general-count
Line
main_full_version.tex:2013
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: The enumeration bound 2Qr C_q(2D+1)^{2τn}2^{2n/r} in Prop 3.4 rests on eq:boolean-enumeration. Line 1980 obtains that bound via "Lemma  therefore computes the restricted sum". The proof at line 2033 cites eq:boolean-enumeration directly, but the DAG has no edge to the lemma.
  • info
    inferred_dep
    critique: The proof of Prop 3.4 (main_full_version.tex:2036-2037) says "The preceding Taylor identity and interpolation prove correctness". That identity, eq:full-taylor-sum, comes from "Apply Lemma  to [z^j]G_x" at line 1964. The edge is missing, which also leaves the lemma an orphan.
  • info
    inferred_dep
    critique: The statement of Prop 3.4 (line 2018) requires that the data "satisfy Definition ", and the proof uses that design throughout. The DAG has no edge.