claimroutineinferred_dep

Collision gain via conditioning on clean sigma-field

Collision event costs a factor 22CEh∗B−1/22^{2C_Eh_*}B^{-1/2} on the clean height
yields the direct collision charge of the lemma
Claim·§9.4 Bucket algebra and the collision charge·inside lemDirect collision charge bound

Statement (paper)

The quantities HxH_x and Ex\mathcal E_x are Gb\mathcal G_b-measurable, and E[1CxHxs∣Gb]=HxsPr⁡(Cx∣Gb)≤C 22CEh∗B−1/2Hxs\mathbb E\bigl[\mathbf1_{\mathcal C_x}H_x^s\mid\mathcal G_b\bigr]=H_x^s\Pr(\mathcal C_x\mid\mathcal G_b)\le C\,2^{2C_Eh_*}B^{-1/2}H_x^s. Since the row membership Xu(x)X_u(x) is also Gb\mathcal G_b-measurable, integrating in the row measure gives ∥1CH∥row,u;ss≤C 22CEh∗B−1/2∥H∥row,u;ss\|\mathbf1_{\mathcal C}H\|_{\mathrm{row},u;s}^s\le C\,2^{2C_Eh_*}B^{-1/2}\|H\|_{\mathrm{row},u;s}^s, with no conditioning on Fxc\mathcal F_x^c.

In plain English

The clean height HxH_x and envelope Ex\mathcal E_x are Gb\mathcal G_b-measurable, so conditioning on Gb\mathcal G_b gives E[1CxHxs∣Gb]=HxsPr⁡(Cx∣Gb)≤C 22CEh∗B−1/2Hxs\mathbb E[\mathbf1_{\mathcal C_x}H_x^s\mid\mathcal G_b]=H_x^s\Pr(\mathcal C_x\mid\mathcal G_b)\le C\,2^{2C_Eh_*}B^{-1/2}H_x^s. Integrating over the row measure (row membership Xu(x)X_u(x) is also Gb\mathcal G_b-measurable) yields ∥1CH∥row,u;ss≤C 22CEh∗B−1/2∥H∥row,u;ss\|\mathbf1_{\mathcal C}H\|_{\mathrm{row},u;s}^s\le C\,2^{2C_Eh_*}B^{-1/2}\|H\|_{\mathrm{row},u;s}^s, with no conditioning on Fxc\mathcal F_x^c.

Why it's here

Since HxH_x is fixed by the clean data, the collision event Cx\mathcal C_x can be bounded by the envelope collision probability from the envelope lemma, which pulls out a factor B−1/2B^{-1/2} at a cost of only 22CEh∗2^{2C_Eh_*}. Combined with the row-norm bound on HH from the previous claim, this gives the direct collision charge 2−p2Ch∗B−1/(2s)2^{-p}2^{Ch_*}B^{-1/(2s)} in the parent lemma.
Classified routine:
Direct consequence of the envelope lemma (lem-fp-envelope): pull the G_b-measurable factor H_x^s out of the conditional expectation, then integrate against the G_b-measurable row measure. This is a standard tower-property and measurability step.

Uses

lemWitness envelope is small and collision-controlledclaimPropagated clean height has small row norm

Used by

Nothing in the paper

Sources

PaperOpen
Section
§9.4 Bucket algebra and the collision charge
Page
—
Label
—
Line
sections/fingerprints.tex:577
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Conditioning on clean sigma-field gives collision gain" rests on lem:fp-envelope
  • info
    inferred_dep
    outline: "Conditioning on clean sigma-field gives collision gain" rests on claim-lem-fp-direct-2