lemmaroutine

Atom correction is exact with bounded gate

Correction atom has exact conditional mean

F(x,y)

and normalization ≥ 3/4

unbiasedness of the correction estimator

Lemma·lem:atom-correction·§5.3 Corrections with an incoming gate

Statement (paper)

For sufficiently large fixed

K

and then

K_c

, the conditional mean of

f\mathcal F(x,y)

X_u(x)=Y_t(y)=1

is exactly

F(x,y)

. On a true position with

Q(d_y)>0

and

g_0(y)>0

q_y=\alpha(x,y):= \mathbb E[R T_y\mid X_u(x)=Y_t(y)=1]\ge3/4.

No lower bound on

q_y

\alpha(x,y)

is required when

g_0(y)=0

. The true gates and normalization use only the two role channels

X,Y

;

g_0

is deterministic.

In plain English

For sufficiently large fixed

K

and then

K_c

, the conditional mean of

f\mathcal F(x,y)

given

X_u(x)=Y_t(y)=1

equals

F(x,y)

exactly. On a true position with

Q(d_y)>0

and

g_0(y)>0

, the normalization

q_y=\alpha(x,y)=\mathbb E[R T_y\mid X_u(x)=Y_t(y)=1]

is at least

3/4

, and no lower bound is needed when

g_0(y)=0

Why it's here

This shows the correction built on the dense-bin atom table is unbiased on the slice, building on the atom identity of the dense-bin lemma. The lower bound

q_y\ge 3/4

keeps the normalization away from zero on positions where the incoming gate is active. The true gates and normalization depend only on the two role channels

X,Y

, and

g_0

is deterministic, so the correction uses no extra randomness.

Classified routine:

A direct consequence of the dense-bin atom identity (lem-atom-dense): unbiasedness on the slice follows from normalizing by the conditional mean, and the bound q_y ≥ 3/4 comes from taking the constants K and K_c large. This is parameter bookkeeping on top of the earlier lemma, not a new idea.

Uses

lemDense-bin atom table is bounded and unbiased

Used by

Nothing in the paper

Sources

PaperOpen

Section: §5.3 Corrections with an incoming gate
Page: —
Label: lem:atom-correction
Line: sections/atoms.tex:335

Leannot aligned

Phase 2 aligns this node to a Lean declaration.