lemmaroutine

Direct collision charge bound

Direct collision charge is ≤

2^{-p}2^{Ch_*}B^{-1/(2s)}

; rest is child discrepancy

collision charge in the coupling recurrence

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

Statement (paper)

The direct collision contribution to any final pre-incoming output has norm at most

2^{-p}\,2^{C h_*}B^{-1/(2s)},

for a fixed

C

independent of

D_1,D_2,\epsilon

introduced below. All remaining contributions on

\mathcal F_x^c

are bounded by actual--clean child discrepancy norms with an amplification at most

2^{C d}

at slack

d

In plain English

On the complement of the key-success event, the direct collision contribution to any final pre-incoming output has norm at most

2^{-p}\,2^{C h_*}B^{-1/(2s)}

, with

C

independent of

D_1,D_2,\epsilon

. Every other contribution there is bounded by actual–clean child discrepancy norms, with amplification at most

2^{Cd}

at slack

d

Why it's here

This lemma splits the bucket error from the bucket discrepancy bound into two parts: a collision term whose size is controlled by the collision probability together with the small clean-height row norm, and a remainder controlled by child discrepancies at cost

2^{O(d)}

via the raw difference estimate. The uniform block coupling proposition uses this split to bound the recurrence by an escape/collision charge plus child discrepancies.

Classified routine:

This splits the earlier bucket discrepancy bound into a collision term and child-discrepancy remainders, using the raw difference estimate and buffer Lipschitz/clamping lemmas. It is bookkeeping on top of earlier nodes, not a new idea.

Uses

lemRaw difference bounds at slack-d groupslemBuffer update map: replacement, monotonicity, LipschitzlemClamping preserves final row functionslemBucket discrepancy bound with collision charge

Used by

propActual runs stay close to clean runsclaimCoupling recurrence from child charges

Inside the proof

claimCrude bound on clean group incrementsclaimPropagated clean height has small row normclaimCollision gain via conditioning on clean sigma-fieldclaimRemaining terms bounded by child discrepancies

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.