claimroutine

Conditional environment law is enumerable

Conditional environment is uniform over at most

2^{O(B)}

enumerable encodings

gives the finite list the median step enumerates

Claim·§12.2 A dyadic approximation at the specified start·inside thmDeterministic logspace approximation of acceptance probability

Statement (paper)

The conditional law of the environment given

X_f(z)=1

, as in Equation , is the uniform law on the retained encodings: those choices of field-matrix entries in

\{0,\ldots,P-1\}

and raw salt bit strings whose positive-degree columns form a frame and for which

X_f(z)=1

. At least one encoding is retained, each encoding takes

O(B)

bits, and there are at most

2^{O(B)}

encodings, so they can be enumerated exactly, with raw salt strings counted with multiplicity.

In plain English

Conditioned on

X_f(z)=1

, the environment is uniformly distributed over the retained encodings: field-matrix entries in

\{0,\ldots,P-1\}

and raw salt bit strings whose positive-degree columns form a frame and for which

X_f(z)=1

. At least one encoding is retained, each takes

O(B)

bits, and there are at most

2^{O(B)}

of them, so they can be enumerated exactly with raw salt strings counted with multiplicity.

Why it's here

This turns the conditional distribution into a finite uniform list that a deterministic procedure can enumerate and count exactly. The binary-search median step uses this: it needs a nonempty uniform multiset of retained encodings, whose size

E

it can compare against the threshold

h

Classified routine:

Direct bookkeeping: conditioning a uniform distribution on finitely many O(B)-bit encodings on an event of positive probability yields the uniform law on the retained encodings, which can be enumerated in 2^{O(B)} steps.

Uses

Nothing else in the paper

Used by

claimBinary-search median is accurate

Sources

PaperOpen

Section: §12.2 A dyadic approximation at the specified start
Page: —
Label: —
Line: sections/conclusion.tex:215

Leannot aligned

Phase 2 aligns this node to a Lean declaration.