claimroutineinferred_dep

Remaining terms bounded by child discrepancies

Non-collision terms are bounded by child discrepancies at cost

2^{Cd}

handles the non-collision part of the bucket bound

Claim·§9.4 Bucket algebra and the collision charge·inside lemDirect collision charge bound

Statement (paper)

All remaining contributions to the first term of Equation on

\mathcal F_x^c

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

2^{Cd}

at slack

d

, for a fixed constant

C

. This holds without any assumption on key success or on independence of the child errors.

In plain English

Apart from the direct collision term, every contribution to the first term of the bucket bound on

\mathcal F_x^c

is controlled by actual–clean child discrepancy norms, losing at most a factor

2^{Cd}

at slack

d

. No assumption on key success or on independence of the child errors is needed.

Why it's here

By the bucket discrepancy bound, the error at a small group is at most

(k_d+1)

times the actual–clean child difference plus a collision-only term, with

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

. The raw difference estimate at slack-

d

groups then bounds the child-difference part by child discrepancies at cost

2^{O(d)}

. This leaves only the direct collision charge for the rest of the parent lemma to handle.

Classified routine:

Direct consequence of the bucket discrepancy bound (lem-fp-buckets) combined with the raw difference estimate at slack-d groups (lem-est-raw-difference); it is bookkeeping of the 2^{O(d)} amplification factors.

Uses

lemRaw difference bounds at slack-d groupslemBucket discrepancy bound with collision charge

Used by

Nothing in the paper

Sources

PaperOpen

Section: §9.4 Bucket algebra and the collision charge
Page: —
Label: —
Line: sections/fingerprints.tex:599

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Remaining terms bounded by child discrepancies" rests on lem:fp-buckets