propositionroutine

Hierarchy reward approximates base acceptance probability

Stage-LL reward WLW_L is within ∣V0∣2−(H−1)L|V_0|2^{-(H-1)L} below p0(x)p_0(x), L=O(B)L=O(B)
one-sided approximation target for the fixed-precision theorem
Proposition·prop:hier-reward-target·§4.5 Reward transport and the final deterministic target

Statement (paper)

For every stage, ClPlc=Plc−Bl(I−S). C_lP_l^c=P_l^c-B_l(I-S). The vectors Wl=BleW_l=B_le satisfy 0≤Wl≤1,Wl=Plcp0−ClPlcp0, 0\leq W_l\leq1,\qquad W_l=P_l^cp_0-C_lP_l^cp_0, and their updates are Wl+1(xi)=ri(x)(Wl(x)+(ElWl)(x)). W_{l+1}(x_i)=r_i(x)\bigl(W_l(x)+(E_lW_l)(x)\bigr). If xˉl\bar x_l is the all-primary copy of a base vertex xx, then 0≤p0(x)−Wl(xˉl)≤∣V0∣ 2−(H−1)l. 0\leq p_0(x)-W_l(\bar x_l) \leq |V_0|\,2^{-(H-1)l}. Consequently there is L=O(B)L=O(B) for which the last upper bound is strictly less than 1/161/16 for every base vertex xx. In particular, p0(x)=0p_0(x)=0 implies WL(xˉL)=0W_L(\bar x_L)=0, and p0(x)≥1/2p_0(x)\ge1/2 implies WL(xˉL)>7/16W_L(\bar x_L)>7/16. Every full stage domain has size 2O(B)2^{O(B)} and admits O(B)O(B)-bit addresses.

In plain English

At every stage, ClPlc=Plc−Bl(I−S)C_lP_l^c=P_l^c-B_l(I-S), and the reward vectors Wl=BleW_l=B_le lie in [0,1][0,1], equal Plcp0−ClPlcp0P_l^cp_0-C_lP_l^cp_0, and obey the explicit update Wl+1(xi)=ri(x)(Wl(x)+(ElWl)(x))W_{l+1}(x_i)=r_i(x)(W_l(x)+(E_lW_l)(x)). At the all-primary copy ar x_l of a base vertex xx, W_l(ar x_l) underestimates p0(x)p_0(x) by at most ∣V0∣2−(H−1)l|V_0|2^{-(H-1)l}, so some L=O(B)L=O(B) separates p0(x)=0p_0(x)=0 (giving WL=0W_L=0) from p0(x)≥1/2p_0(x)\ge1/2 (giving WL>7/16W_L>7/16), with stage domains of size 2O(B)2^{O(B)} and O(B)O(B)-bit addresses.

Why it's here

This turns the copy-step intertwining of the previous proposition into a reward identity. Each stage's reward vector then tracks the acceptance probability up to an error that shrinks geometrically, so a threshold test at a stage L=O(B)L=O(B) decides the base probability. It also bounds the size and addressing of the domains needed to compute it, which the fixed-precision theorem uses as its deterministic target.
Classified routine:
This follows from the copy-step proposition (prop:hier-copy-step) by algebraic bookkeeping: telescoping the intertwining identity into a reward recursion, then turning the geometric density decay into an error bound and a choice of L = O(B). No new idea is needed beyond that earlier node.

Uses

propOne-stage copy step reduces density and active vertices

Used by

thmDeterministic logspace approximation of acceptance probabilityclaimStage-L reward approximates acceptance probability

Sources

PaperOpen
Section
§4.5 Reward transport and the final deterministic target
Page
—
Label
prop:hier-reward-target
Line
sections/hierarchy.tex:647
Leannot aligned

Phase 2 aligns this node to a Lean declaration.