claimroutineinferred_dep

Enumeration count and space bound

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

Statement (paper)

For each tuple

\vec y

, the scan finding the representatives

\bar x_g

and the scan computing the sums

\Sigma_g(\vec y)

each examine at most

\sum_{g=1}^r 2^{|S_g|}

Boolean vectors, so the algorithm examines at most

2(2D+1)^c\sum_{g=1}^r2^{|S_g|}

Boolean vectors in total. Checking a vector's measurements and fixed bits uses

\poly(n,r,c,\log(D+2))

bit operations, with at most one factor

A_g

evaluation per vector. Apart from the evaluators' own storage, the retained state consists of

\vec y

(

c

integers in

[-D,D]

), the representatives (

n

bits in total),

g

u

, and the ring elements

s,p,Z\in\mathcal A

, so the procedure uses

\poly(n,r,c,\log(D+2))

bits of space plus

O(1)

ring elements.

In plain English

The tuple-by-tuple algorithm examines at most

2(2D+1)^c\sum_g 2^{|S_g|}

Boolean vectors, using at most one

A_g

evaluation and polynomial bit work per vector. Its space is

\poly(n,r,c,\log(D+2))

bits plus

O(1)

ring elements, beyond the evaluators' own storage.

Why it's here

This is the resource accounting that completes the lemma after the correctness claim: each of the at most

(2D+1)^c

tuples

\vec y

costs two scans (one for the representatives, one for the sums

\Sigma_g(\vec y)

), each over at most

\sum_g 2^{|S_g|}

vectors. Only

\vec y

, the representatives, a few counters, and the ring elements

s,p,Z

are kept, which gives the stated space bound.

Classified routine:

Straightforward resource accounting for the tuple-by-tuple enumeration of the preceding claim: it counts (2D+1)^c tuples times two scans over the sum of 2^{|S_g|} vectors and tallies the retained state.

Uses

claimTuple-by-tuple algorithm computes Z_E

Used by

Nothing in the paper

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Enumeration count and space bound" rests on claim-lem-measurement-separation-2