claimroutine

Crude bound on clean group increments

Clean group increments have row norm at most 2−p+O(d)2^{-p+O(d)}
baseline size of clean increments for the height bound
Claim·§9.4 Bucket algebra and the collision charge·inside lemDirect collision charge bound

Statement (paper)

For each small dyadic group of slack dd, the complete clean true-ID increment Δdcl,ν(x,y)\Delta_d^{\mathrm{cl},\nu}(x,y) in channel ν∈{1,2}\nu\in\{1,2\}, with any exact base term assigned to that group and an absent second channel taken to be zero, satisfies the crude absolute estimates in the retained endpoint metric, with variant counting and summation over difference layers costing 2O(d)2^{O(d)} and without using walk contraction. Consequently the row norm of max⁡νsup⁡y∣Δdcl,ν(x,y)∣\max_\nu\sup_y|\Delta_d^{\mathrm{cl},\nu}(x,y)| is at most 2−p+O(d)2^{-p+O(d)}.

In plain English

For each small dyadic group of slack dd, the complete clean true-ID increment Δdcl,ν(x,y)\Delta_d^{\mathrm{cl},\nu}(x,y) in either channel ν∈{1,2}\nu\in\{1,2\} (including any exact base term assigned to the group, with an absent channel set to zero) obeys crude absolute bounds in the retained endpoint metric, losing only 2O(d)2^{O(d)} from variant counting and summing over difference layers. As a result, the row norm of max⁡νsup⁡y∣Δdcl,ν(x,y)∣\max_\nu\sup_y|\Delta_d^{\mathrm{cl},\nu}(x,y)| is at most 2−p+O(d)2^{-p+O(d)}.

Why it's here

This step applies the raw difference estimate at slack-dd groups to the clean increments, without using walk contraction. The resulting 2−p+O(d)2^{-p+O(d)} row-norm bound is a baseline that the propagated clean height bound in the next claim can build on, since all losses are only 2O(d)2^{O(d)}.
Classified routine:
Direct consequence of the earlier raw difference bound at slack-d groups (lem-est-raw-difference). The estimate is obtained by applying that bound and paying 2^{O(d)} for variant counting and the sum over difference layers, with no new idea and no use of walk contraction.

Uses

lemRaw difference bounds at slack-d groups

Used by

claimPropagated clean height has small row norm

Sources

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

Phase 2 aligns this node to a Lean declaration.