claimroutineinferred_dep

Tuple-by-tuple algorithm computes Z_E

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

Statement (paper)

The algorithm, which processes the measurement tuples

\vec y\in\mathcal Y

one at a time starting from

Z=0_{\mathcal A}

, skips each tuple for which some

\mathcal X_g(y_g)

is empty, and otherwise computes

p=\prod_{g=1}^r\Sigma_g(\vec y)

by scanning

u\in\{0,1\}^{S_g}

and adding

A_g\bigl(u+\sum_{h\ne g}\bar x_h\bigr)

s

whenever

C_gu=y_g

and

u_i=1

for

i\in E\cap S_g

, and then updates

Z\leftarrow Z+p

, terminates with

Z=Z_E

In plain English

The algorithm that loops over measurement tuples

\vec y\in\mathcal Y

, skips tuples where some

\mathcal X_g(y_g)

is empty, computes

p=\prod_g\Sigma_g(\vec y)

by scanning each

\{0,1\}^{S_g}

, and accumulates

Z\leftarrow Z+p

, ends with

Z=Z_E

Why it's here

This is the correctness step: by the factorization claim,

Z_E

is the sum over tuples of the products

\prod_g\Sigma_g(\vec y)

, with empty tuples contributing zero. The algorithm computes exactly these terms, since each

\Sigma_g(\vec y)

is the sum of

A_g

at the shifted argument over

u

with

C_gu=y_g

and

u_i=1

E\cap S_g

. Adding the products one at a time therefore yields

Z_E

Classified routine:

A direct correctness check for the enumeration loop: it computes each per-part sum by brute force and adds up the products, matching the factorization in the preceding claim (claim-lem-measurement-separation-1) term by term.

Uses

claimSum factors over fixed measurement tuples

Used by

claimEnumeration count and space bound

Sources

PaperOpen

Section: §3.3 Separating the sum by fixing measurements
Page: —
Label: —
Line: main_full_version.tex:1850

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Tuple-by-tuple evaluation algorithm" rests on claim-lem-measurement-separation-1