claimroutineinferred_dep

Rank survives and leaf is detected

Rank survives ss levels with probability ≥ 1/2, then the leaf is detected
combines into the 1/4 detection bound
Claim·§3.4 Linear lifts and loss of rank·inside propFull lifts detect the leaf symbol

Statement (paper)

With s=⌊Hr0/(8θ)⌋s=\lfloor H_{r_0}/(8\theta)\rfloor, one has E[Hr0−Hrs]≤4sθ≤Hr0/2\E[H_{r_0}-H_{r_s}]\le 4s\theta\le H_{r_0}/2, hence Pr⁡[rs=0]≤1/2\Pr[r_s=0]\le 1/2. Conditional on any surviving rank rs>0r_s>0, the independent uniform symbol in BB at the leaf is detected with probability 1−2−rs≥1/21-2^{-r_s}\ge 1/2, and such a detection yields some z∈B∗z\in B^* with ψz(ξs)≠0\psi_z(\xi_s)\ne0.

In plain English

With s=⌊Hr0/(8θ)⌋s=\lfloor H_{r_0}/(8\theta)\rfloor, the expected total drop in harmonic rank over ss levels is at most 4sθ≤Hr0/24s\theta\le H_{r_0}/2, so the rank is still positive at depth ss with probability at least 1/21/2. Given positive rank rs>0r_s>0, the leaf symbol is detected with probability 1−2−rs≥1/21-2^{-r_s}\ge 1/2, and detection gives some z∈B∗z\in B^* with ψz(ξs)≠0\psi_z(\xi_s)\ne0.

Why it's here

Summing the per-level bound EΔj≤4θ\E\Delta_j\le4\theta over ss levels gives the expected total drop, and Markov's inequality shows the rank cannot reach zero with probability above 1/21/2. Combining this survival probability of at least 1/21/2 with detection probability at least 1/21/2 at the leaf yields the 1/41/4 lower bound in the parent proposition.
Classified routine:
Direct consequence of the preceding per-level bound EΔj≤4θ\E\Delta_j\le4\theta: summing over ss levels with linearity of expectation and applying Markov's inequality, then the elementary fact that a uniform symbol is detected with probability 1−2−r1-2^{-r} by a rank-rr linear map.

Uses

claimExpected harmonic rank drop per level

Used by

Nothing in the paper

Sources

PaperOpen
Section
§3.4 Linear lifts and loss of rank
Page
—
Label
—
Line
sections/02-latent.tex:600
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Rank survives with probability half, leaf detection" rests on claim-prop-latent-full-lift-detection-2