corollaryroutine

Cross-pair error bound for true states

Corollary·pred:cross·§3.3 Equality of one coordinate

Statement (paper)

Let

\omega,\pi,D

be as above, let

K\ge1,L\ge2

be integers, and let

T

be an independent random test giving the state maps just described. Set

s_0=\E_T\Prob_{(p,q)\sim\omega} \{y_T(p)\notin R_{y_T(q)}\}.

There exists a fixed history

H:P\to\mathcal H

, with

\abs{H(P)}\le L^{2K}

, for which the laws of the true, unhashed states

\nu_{h,T}=(y_T)_*\mu_h

satisfy

\E_T\E_{(p,q)\sim\omega} [1-\nu_{H(p),T}(R_{y_T(q)})] \le s_0+\frac4L+18(D/K)^{1/4}.

The history is formed from earlier tests and does not use

T

In plain English

With

s_0

the average rate at which

y_T(p)\notin R_{y_T(q)}

over

(p,q)\sim\omega

and random test

T

, there is a single history

H:P\to\mathcal H

with at most

L^{2K}

values, chosen from earlier tests and independent of

T

, such that

\E_T\E_{(p,q)\sim\omega}[1-\nu_{H(p),T}(R_{y_T(q)})]\le s_0+4/L+18(D/K)^{1/4}

Why it's here

This turns the abstract prefix-history bound of the device lemma into a statement about the true, unhashed states: the history-conditioned law of

y_T(p)

lands in

R_{y_T(q)}

with failure probability only slightly above the baseline

s_0

. The extra

4/L

and

(D/K)^{1/4}

terms are the cost of hashing the states and of the history's imperfect prediction. The history has bounded size and does not depend on

T

, so it can be fixed in advance.

Classified routine:

A direct corollary of the prefix-history device lemma (pred-device), obtained by hashing the states into L buckets (the 4/L term), averaging over the random step to fix one history, and converting the bounded discrepancy into a failure-probability estimate; this is bookkeeping on top of that lemma.

Uses

lemPrefix history predicts test discrepancy

Used by

Nothing in the paper

Sources

PaperOpen

Section: §3.3 Equality of one coordinate
Page: —
Label: pred:cross
Line: sections/02-prediction.tex:280

Leannot aligned

Phase 2 aligns this node to a Lean declaration.