lemmaroutine

Separating sums by fixing measurements

Lemma·lem:measurement-separation·§3.3 Separating the sum by fixing measurements

Statement (paper)

Let [n]=S1⊔⋯⊔Sr[n]=S_1\sqcup\cdots\sqcup S_r be a partition, allowing empty parts. For each g∈[r]g\in[r], let CgC_g be an integer matrix with cgc_g rows and columns indexed by SgS_g. Suppose each row has sum of absolute values at most an integer D⩾0D\ge0, and write c=∑gcgc=\sum_g c_g. Let A\mathcal A be a commutative ring with identity, and let Ag:Qn→AA_g:\mathbb Q^n\to\mathcal A satisfy Ag(x+ξ)=Ag(x)(x∈Qn, ξ∈ker⁡Ch, h≠g), A_g(x+\xi)=A_g(x) \qquad (x\in\mathbb Q^n,\ \xi\in\ker C_h,\ h\ne g), where ξ\xi is extended by zero outside ShS_h. For any E⊆[n]E\subseteq[n], the sum ZE=∑x∈{0,1}nxi=1 (i∈E)∏g=1rAg(x) Z_E=\sum_{\substack{x\in\{0,1\}^n\\x_i=1\ (i\in E)}} \prod_{g=1}^r A_g(x) can be evaluated by examining at most 2(2D+1)c∑g=1r2∣Sg∣ 2(2D+1)^c\sum_{g=1}^r2^{|S_g|} Boolean vectors, with at most one AgA_g evaluation, poly⁡(n,r,c,log⁡(D+2))\poly(n,r,c,\log(D+2)) additional bit operations, and O(1)O(1) ring operations per vector. Apart from the evaluators' own storage and O(1)O(1) ring elements, the procedure uses poly⁡(n,r,c,log⁡(D+2))\poly(n,r,c,\log(D+2)) bits of space.

In plain English

Given a partition [n]=S1⊔⋯⊔Sr[n]=S_1\sqcup\cdots\sqcup S_r and integer matrices CgC_g (with c=∑gcgc=\sum_g c_g rows in total, row absolute sums at most DD), suppose each AgA_g is invariant under shifts by ker⁡Ch\ker C_h for h≠gh\ne g. Then ZE=∑x∈{0,1}n, xE=1∏gAg(x)Z_E=\sum_{x\in\{0,1\}^n,\,x_E=1}\prod_g A_g(x) can be computed by examining at most 2(2D+1)c∑g2∣Sg∣2(2D+1)^c\sum_g 2^{|S_g|} Boolean vectors, with one AgA_g evaluation and polynomial bit work per vector, in polynomial extra space.

Why it's here

It replaces a sum over 2n2^n assignments by (2D+1)c(2D+1)^c measurement tuples, each contributing a product of sums over the individual parts SgS_g, so the cost is governed by ∑g2∣Sg∣\sum_g 2^{|S_g|} rather than 2n2^n. The kernel-invariance hypothesis lets each AgA_g ignore the other parts once their measurements are fixed, which makes the factorization work. This is the splitting tool that the later counting routine builds on.
Classified routine:
A direct factorization argument: fix the tuple of measurement values ChxShC_hx_{S_h} (at most (2D+1)c(2D+1)^c choices), so the kernel-invariance makes each AgA_g depend only on xSgx_{S_g} and the sum splits into a product of per-part sums. This is standard grouping-by-fingerprint bookkeeping with nothing conceptually beyond that.

Uses

Nothing else in the paper

Used by

propGeneral counting routine and its cost

Inside the proof

claimSum factors over fixed measurement tuplesclaimTuple-by-tuple algorithm computes Z_EclaimEnumeration count and space bound

Sources

PaperOpen
Section
§3.3 Separating the sum by fixing measurements
Page
—
Label
lem:measurement-separation
Line
main_full_version.tex:1781
Leannot aligned

Phase 2 aligns this node to a Lean declaration.