lemmaroutine

Bucket discrepancy bound with collision charge

Bucket increment gap is ≤

(k_d+1)

times child gap plus a collision-only term

splits bucket error into child and collision parts

Lemma·lem:fp-buckets·§9.4 Bucket algebra and the collision charge

Statement (paper)

Consider one small group on

\mathcal F_x^c

. Let

\Delta_{\mathrm{ac}}(y),\Delta_{\mathrm{cl}}(y)

be its unaliased increments, namely its true-ID sums using actual and clean children, respectively. Let

k_d\le2^{C d}

bound its number of immediate descriptors, and let

\mathcal C_x

denote a collision on

\mathcal E_x

. The discrepancy between the actual bucket-distributed increment and the clean true-ID increment is at most

(k_d+1)\left( \sup_y|\Delta_{\mathrm{ac}}(y)-\Delta_{\mathrm{cl}}(y)| +\mathbf1_{\mathcal C_x}\sup_y|\Delta_{\mathrm{cl}}(y)| \right)

in sup norm, simultaneously for both channels. The old full-array discrepancy is added to this bound with coefficient one.

In plain English

For one small group on

\mathcal F_x^c

with at most

k_d\le 2^{Cd}

immediate descriptors, the sup-norm gap between the actual bucket-distributed increment and the clean true-ID increment is at most

(k_d+1)\big(\sup_y|\Delta_{\mathrm{ac}}(y)-\Delta_{\mathrm{cl}}(y)|+\mathbf1_{\mathcal C_x}\sup_y|\Delta_{\mathrm{cl}}(y)|\big)

, for both channels at once. The old full-array discrepancy is added with coefficient one.

Why it's here

This converts the bucket-level error into two quantities: the difference between actual and clean children, and a collision term that appears only when a collision occurs on

\mathcal E_x

. The factor

k_d+1\le 2^{Cd}+1

is the cost of summing over descriptors. Later results use it to split the error into a child-discrepancy part and a direct collision charge.

Classified routine:

A triangle-inequality bookkeeping bound: the gap is split into an actual-versus-clean child difference plus a collision indicator term, then summed over at most k_d+1 buckets. It is a direct calculation specific to the paper's bucket construction rather than a new idea.

Uses

Nothing else in the paper

Used by

lemDirect collision charge boundlemEstimator recipes have regenerable records and bounded controlclaimPropagated clean height has small row normclaimRemaining terms bounded by child discrepanciesclaimCoupling recurrence from child chargesclaimCandidate domain and bucket sums

Sources

PaperOpen

Section: §9.4 Bucket algebra and the collision charge
Page: —
Label: lem:fp-buckets
Line: sections/fingerprints.tex:456

Leannot aligned

Phase 2 aligns this node to a Lean declaration.