claimroutineinferred_dep

Propagated clean height has small row norm

Propagated clean height HxH_x has row norm at most 2−p+C0h∗2^{-p+C_0h_*}
bounds the clean height that multiplies the collision term
Claim·§9.4 Bucket algebra and the collision charge·inside lemDirect collision charge bound

Statement (paper)

There are fixed constants CP,APC_P,A_P such that CP(d+1)APC_P(d+1)^{A_P} bounds the propagation of an input discrepancy at slack dd to the output metric. For the quantity Hx=CP∑d≤2h∗, d a group slack(d+1)AP(kd+1)max⁡νsup⁡y∣Δdcl,ν(x,y)∣H_x=C_P\sum_{d\le 2h_*,\ d\text{ a group slack}}(d+1)^{A_P}(k_d+1)\max_\nu\sup_y|\Delta_d^{\mathrm{cl},\nu}(x,y)|, with Hx=0H_x=0 when Xu(x)=0X_u(x)=0, which bounds the propagated clean-height terms in Equation , we have ∥H∥row,u;s≤2−p+C0h∗\|H\|_{\mathrm{row},u;s}\le 2^{-p+C_0h_*}.

In plain English

With CP(d+1)APC_P(d+1)^{A_P} bounding how an input discrepancy at slack dd propagates to the output metric, the propagated clean height HxH_x (a weighted sum over group slacks d≤2h∗d\le 2h_* of (kd+1)max⁡νsup⁡y∣Δdcl,ν(x,y)∣(k_d+1)\max_\nu\sup_y|\Delta_d^{\mathrm{cl},\nu}(x,y)|, and 00 when Xu(x)=0X_u(x)=0) satisfies ∥H∥row,u;s≤2−p+C0h∗\|H\|_{\mathrm{row},u;s}\le 2^{-p+C_0h_*}.

Why it's here

This takes the crude 2−p+O(d)2^{-p+O(d)} row-norm bound on clean group increments and sums it over the at most 2h∗2h_* group slacks, where the factors (d+1)AP(d+1)^{A_P}, kd+1≤2Cd+1k_d+1\le 2^{Cd}+1 and the propagation constant cost only 2O(d)2^{O(d)}, giving a total of 2−p+C0h∗2^{-p+C_0h_*}. This controls the clean-height terms in the bucket bound, and the next claim uses it together with the collision probability to obtain the direct collision charge.
Classified routine:
Direct consequence of the crude clean-increment bound (claim-lem-fp-direct-1): it sums the 2^{-p+O(d)} row-norm bounds over at most 2h_* group slacks, absorbing the polynomial and k_d+1 factors into 2^{O(h_*)}, with propagation constants from the buffer-update Lipschitz and clamping lemmas.

Uses

lemBuffer update map: replacement, monotonicity, LipschitzlemClamping preserves final row functionslemBucket discrepancy bound with collision chargeclaimCrude bound on clean group increments

Used by

claimCollision gain via conditioning on clean sigma-field

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Propagated clean height H_x bounded" rests on claim-lem-fp-direct-1