claimroutine

Sum factors over fixed measurement tuples

Claim·§3.3 Separating the sum by fixing measurements·inside lemSeparating sums by fixing measurements

Statement (paper)

For yg∈Zcgy_g\in\mathbb Z^{c_g} let Xg(yg)={u∈{0,1}Sg:Cgu=yg}\mathcal X_g(y_g)=\{u\in\{0,1\}^{S_g}:C_gu=y_g\} and Y=∏g=1r{−D,…,D}cg\mathcal Y=\prod_{g=1}^r\{-D,\ldots,D\}^{c_g}, so that ∣Y∣=(2D+1)c|\mathcal Y|=(2D+1)^c and every tuple of measurements of a Boolean assignment lies in Y\mathcal Y. For y⃗∈Y\vec y\in\mathcal Y with every Xg(yg)\mathcal X_g(y_g) nonempty, choose representatives xˉg∈Xg(yg)\bar x_g\in\mathcal X_g(y_g) and let Xg,E(yg)={u∈Xg(yg):ui=1 for all i∈E∩Sg}\mathcal X_{g,E}(y_g)=\{u\in\mathcal X_g(y_g):u_i=1\text{ for all }i\in E\cap S_g\} and Σg(y⃗)=∑xg∈Xg,E(yg)Ag(xg+∑h≠gxˉh)\Sigma_g(\vec y)=\sum_{x_g\in\mathcal X_{g,E}(y_g)}A_g\bigl(x_g+\sum_{h\ne g}\bar x_h\bigr), which is 00 if Xg,E(yg)\mathcal X_{g,E}(y_g) is empty. Then the assignments with measurement tuple y⃗\vec y and fixed bits indexed by EE contribute ∏gΣg(y⃗)\prod_g\Sigma_g(\vec y) to ZEZ_E, and hence ZE=∑y⃗∈Y∏g=1rΣg(y⃗)Z_E=\sum_{\vec y\in\mathcal Y}\prod_{g=1}^r\Sigma_g(\vec y), where the product is taken to be zero if any Xg(yg)\mathcal X_g(y_g) is empty.

In plain English

Grouping Boolean assignments by their measurement tuple y⃗=(CgxSg)g\vec y=(C_gx_{S_g})_g, the sum over each group factors as a product of per-part sums Σg(y⃗)\Sigma_g(\vec y), so ZE=∑y⃗∈Y∏gΣg(y⃗)Z_E=\sum_{\vec y\in\mathcal Y}\prod_g\Sigma_g(\vec y), with the product taken as zero if any Xg(yg)\mathcal X_g(y_g) is empty.

Why it's here

Within a fixed tuple, each AgA_g can have its argument shifted so that the other parts are replaced by fixed representatives, because differences between assignments with equal measurements lie in ker⁡Ch\ker C_h. The sum over assignments then splits into independent sums over each SgS_g. This turns ZEZ_E into (2D+1)c(2D+1)^c products of smaller sums, which the tuple-by-tuple algorithm then evaluates.
Classified routine:
A direct bookkeeping step: grouping assignments by their measurement tuple and using kernel invariance of each AgA_g to factor the sum. This is the standard technique of splitting a sum over a product domain into a product of independent sums.

Uses

Nothing else in the paper

Used by

claimTuple-by-tuple algorithm computes Z_E

Sources

PaperOpen
Section
§3.3 Separating the sum by fixing measurements
Page
—
Label
—
Line
main_full_version.tex:1810
Leannot aligned

Phase 2 aligns this node to a Lean declaration.