claimroutineinferred_dep

False-type first overflow charge bound

False-type first-overflow error power is at most Cc∗s2−sp∑j(⋯ )Cc_*^s2^{-sp}\sum_j(\cdots)
false-type term of the error budget
Claim·§8.4 Charging overflow events·inside propCompression preserves row error budget

Statement (paper)

On the event of a false-type first overflow, by Equation  and the disjointness of the possible first-overflow events, the total false-type error power is at most Cc∗s2−sp∑j(njρjs)−1(2sB1dj+2−sKndj)Cc_*^s2^{-sp}\sum_j (n_j\rho_j^s)^{-1}\bigl(2^{sB_1d_j}+2^{-sK_nd_j}\bigr).

In plain English

On the event that the first overflow is of false type, the total false-type error power is at most Cc∗s2−sp∑j(njρjs)−1(2sB1dj+2−sKndj)Cc_*^s2^{-sp}\sum_j (n_j\rho_j^s)^{-1}\bigl(2^{sB_1d_j}+2^{-sK_nd_j}\bigr).

Why it's here

It sums the per-event false-type charge from Equation (buf-false-charge) over the possible first-overflow events, which are disjoint, so each outcome is charged only once and the sum over jj has no overlap. The resulting series is the one whose convergence under the floor and capacity exponent choices is handled in the later claim, which keeps the false-type contribution within the error budget.
Classified routine:
This is bookkeeping inside the proof of prop-buf-error. It sums the per-event charge from Equation (buf-false-charge) over disjoint first-overflow events, a standard union/disjointness summation, using the row-sup-to-summed-power conversion from claim-prop-buf-error-1.

Uses

claimRow sup bounds convert to summed powers

Used by

claimFloor and capacity exponents make sums converge

Sources

PaperOpen
Section
§8.4 Charging overflow events
Page
—
Label
—
Line
sections/compression.tex:498
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "False-type first overflow charge" rests on claim-prop-buf-error-1