claimroutineinferred_dep

Expected harmonic rank drop per level

Expected harmonic rank drop per level is at most 4θ4\theta
per-level cost summed over the depth
Claim·§3.4 Linear lifts and loss of rank·inside propFull lifts detect the leaf symbol

Statement (paper)

With Δj=Hrj−Hrj+1≥0\Delta_j=H_{r_j}-H_{r_{j+1}}\ge0, for every jj one has E[Δj∣Fj]≤3θ+Hr02r0θBj\E[\Delta_j\mid\mathcal F_j]\le3\theta+H_{r_0}2^{r_0}\theta B_j, and consequently the unconditional bound EΔj≤(3+Hr02r0ε0)θ≤4θ\E\Delta_j\le\bigl(3+H_{r_0}2^{r_0}\eps_0\bigr)\theta\le4\theta holds.

In plain English

With Δj=Hrj−Hrj+1≥0\Delta_j=H_{r_j}-H_{r_{j+1}}\ge0 the drop in harmonic rank at level jj, one has E[Δj∣Fj]≤3θ+Hr02r0θBj\E[\Delta_j\mid\mathcal F_j]\le3\theta+H_{r_0}2^{r_0}\theta B_j. Taking expectations gives EΔj≤(3+Hr02r0ε0)θ≤4θ\E\Delta_j\le(3+H_{r_0}2^{r_0}\eps_0)\theta\le4\theta.

Why it's here

This is the per-level cost estimate: the block-kernel lemma limits how much rank can be lost at a generic level, and the nongeneric indicator BjB_j accounts for the exceptional case. The fresh-isomorphism claim gives EBj≤ε0\E B_j\le\eps_0, which turns the conditional bound into the uniform 4θ4\theta per level. Summing over ss levels then shows the rank survives with good probability in the next claim.
Classified routine:
A per-level expected-cost calculation that combines the block-kernel lemma (rank loss at generic levels) with the genericity bound EBj≤ε0\E B_j\le\eps_0 from the preceding claim. It is bookkeeping inside the proof of the full-lift detection proposition.

Uses

lemKernel of block restriction mapclaimFresh isomorphisms make genericity typical

Used by

claimRank survives and leaf is detected

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Expected harmonic rank drop per level" rests on lem:latent-block-kernel
  • info
    inferred_dep
    outline: "Expected harmonic rank drop per level" rests on claim-prop-latent-full-lift-detection-1