claimroutine

Allowance strictly drops at every boundary

Allowance drops by at least cdcd at every operation-to-child boundary
checks the allowance contract needed for induction
Claim·§11.5 The uniform space theorem·inside thmController interfaces have restoring O(B)-space implementations

Statement (paper)

With w=K1(1+M)−(K0+s0)dw=K_1(1+M)-(K_0+s_0)d as in , every required boundary between an operation and a child operation has allowance drop w−w′≥c dw-w'\ge c\,d for a fixed c>0c>0, where dd is the parent's prefix slack. Moreover, all allowances remain positive and are O(1+M)O(1+M).

In plain English

With allowance w=K1(1+M)−(K0+s0)dw=K_1(1+M)-(K_0+s_0)d, every required boundary from an operation to a child operation lowers the allowance by at least c dc\,d for a fixed c>0c>0, where dd is the parent's prefix slack. All allowances also stay positive and are O(1+M)O(1+M).

Why it's here

This checks the allowance-drop condition of the controller allowance and clock certificate at each boundary, using the control and stratum bounds from the estimator recipes lemma. Strict decrease lets the realization theorem do induction on allowance and bound suspended records, while positivity and the O(1+M)O(1+M) size keep the total space at O(Mtop+t+1)O(M_{\mathrm{top}}+t+1).
Classified routine:
A direct check of the allowance-drop condition from def-ctrl-allowance, plugging the control and stratum bounds of lem-ctrl-recipes into the explicit allowance formula. It is a standard potential-function bookkeeping argument.

Uses

lemEstimator recipes have regenerable records and bounded controldefController allowance and clock certificate

Used by

Nothing in the paper

Sources

PaperOpen
Section
§11.5 The uniform space theorem
Page
—
Label
—
Line
sections/implementation.tex:1201
Leannot aligned

Phase 2 aligns this node to a Lean declaration.