propositionroutine

One-stage copy step reduces density and active vertices

Copy stage keeps entries ≤

f/q

, at most doubles active vertices,

C^+P^r=P^rD

one-stage step iterated to build the hierarchy

Proposition·prop:hier-copy-step·§4.4 Copies reduce density while controlling active vertices

Statement (paper)

Choose the detector rank

J

large enough that

J\geq\frac{2C_\pi(D_0-1)k_*(k_*+1)}{\delta_0},

and then choose

R_*

as in Equation . The matrix

C^+

is strictly forward and substochastic, and

C^+(x_i,y_j)\leq f/q, \qquad |\mathcal A(C^+)|\leq2|\mathcal A(C)|.

P^r

is the matrix from

V^+

V

defined by

P^r(x_i,x)=r_i(x),\qquad P^r(x_i,z)=0\quad(z\ne x),

then

C^+P^r=P^rD.

In plain English

With the detector rank

J

and

R_*

chosen as specified, the copy matrix

C^+

is strictly forward and substochastic, has entries at most

f/q

, and has at most twice as many active vertices as

C

. It also satisfies the one-step intertwining

C^+P^r=P^rD

with the projection

P^r

from

V^+

V

Why it's here

This packages one copy stage: the column test (Lemma 4.3) and the pilot bounds (Lemma 4.2) keep heavy columns out of

C^+

, which gives the density cap

f/q

and the active-vertex bound. The residual

D

(Lemma 4.4) is what

C^+

reproduces under projection, so later stages can compare the copied walk to the original through

P^r

and control the reward identity and shallow target that follow.

Classified routine:

This one-stage packaging follows directly from the column test, pilot bounds and residual lemmas: the density cap, active-vertex bound and intertwining identity C^+P^r = P^rD come from bookkeeping on the copy construction rather than from a new idea.

Uses

lemResidual matrix D is bounded and dominatinglemColumn test separates heavy and light columnslemPilot and actual matrices are bounded

Used by

propHierarchy reward approximates base acceptance probability

Sources

PaperOpen

Section: §4.4 Copies reduce density while controlling active vertices
Page: —
Label: prop:hier-copy-step
Line: sections/hierarchy.tex:522

Leannot aligned

Phase 2 aligns this node to a Lean declaration.