lemmaroutine

Witness envelope is small and collision-controlled

Salt-independent envelope of size 2CEh∗2^{C_Eh_*} has collision probability O(B−1/2)O(B^{-1/2}) per pair
bounds key collisions among all relevant representatives
Lemma·lem:fp-envelope·§9.3 Witness envelopes and escaped paths

Statement (paper)

The set Ex\mathcal E_x is independent of the present salt and has size at most 2CEh∗2^{C_Eh_*} for a fixed CEC_E. All clean nondefault representatives in the small groups belong to this set. Consequently, conditional on the other data, Pr⁡[two distinct IDs in Ex have the same key]≤C 22CEh∗B−1/2. \Pr[\text{two distinct IDs in $\mathcal E_x$ have the same key}] \le C\,2^{2C_Eh_*}B^{-1/2}.

In plain English

The envelope set Ex\mathcal E_x does not depend on the current salt and has at most 2CEh∗2^{C_Eh_*} elements, and it contains every clean nondefault representative in the small groups. Hence, given the other data, the probability that two distinct IDs in Ex\mathcal E_x share a key is at most C 22CEh∗B−1/2C\,2^{2C_Eh_*}B^{-1/2}.

Why it's here

Because Ex\mathcal E_x is fixed independently of the salt and is small, a union bound over its at most 22CEh∗2^{2C_Eh_*} pairs, each colliding with probability O(B−1/2)O(B^{-1/2}) by the pairwise-collision hash lemma, bounds collisions among all relevant representatives at once. This gives the collision gain that later conditioning arguments on the clean block use, relying on the clean-block independence lemma to treat the salt as independent of the envelope.
Classified routine:
This follows directly from the clean-block independence lemma (lem-fp-clean) and the pairwise-collision hash lemma (lem-fp-hash). It applies a standard union bound over at most 2^{2C_E h_*} pairs of IDs in a salt-independent set, each pair colliding with probability O(B^{-1/2}).

Uses

lemClean calculation is independent of the saltlemPairwise-collision hash from few random bits

Used by

claimCollision gain via conditioning on clean sigma-field

Sources

PaperOpen
Section
§9.3 Witness envelopes and escaped paths
Page
—
Label
lem:fp-envelope
Line
sections/fingerprints.tex:304
Leannot aligned

Phase 2 aligns this node to a Lean declaration.