claimroutine

Stack segments telescope to top potential

Live stack segments telescope to Awtop+Dttop+O(1)Aw_{\rm top}+Dt_{\rm top}+O(1)
bounds total record space of the active chain
Claim·§11.5 The uniform space theorem·inside thmController interfaces have restoring O(B)-space implementations

Statement (paper)

If the active chain has boundaries 0,…,r0,\ldots,r, with boundary zero at the top, and Φi=Φ(wi,ti)\Phi_i=\Phi(w_i,t_i), then the total local space of all simultaneously live records is at most ∑i=0r−1(Φi−Φi+1)+Φr+O(1)=Φ0+O(1)=Awtop+Dttop+O(1)\sum_{i=0}^{r-1}(\Phi_i-\Phi_{i+1})+\Phi_r+O(1)=\Phi_0+O(1)=Aw_{\mathrm{top}}+Dt_{\mathrm{top}}+O(1).

In plain English

For an active chain with boundaries 0,…,r0,\ldots,r (boundary zero at the top) and potentials Φi=Φ(wi,ti)\Phi_i=\Phi(w_i,t_i), the total local space of all simultaneously live records is at most ∑i=0r−1(Φi−Φi+1)+Φr+O(1)\sum_{i=0}^{r-1}(\Phi_i-\Phi_{i+1})+\Phi_r+O(1). This sum telescopes to Φ0+O(1)=Awtop+Dttop+O(1)\Phi_0+O(1)=Aw_{\mathrm{top}}+Dt_{\mathrm{top}}+O(1).

Why it's here

Each live record segment between consecutive boundaries is charged the drop in potential Φi−Φi+1\Phi_i-\Phi_{i+1}, using the local-length bound A(w−w′)+D(t−j)A(w-w')+D(t-j) from the guarded local graph lemma. The charges telescope, so the whole stack costs only the top potential plus a constant, which gives the O(Mtop+t+1)O(M_{\mathrm{top}}+t+1) retained-length bound in the realization theorem's space assertion.
Classified routine:
A telescoping-sum charging argument: each stack segment is charged its potential drop using the local-length bound from the guarded local graph lemma, which is a standard amortized potential-function space accounting.

Uses

lemGuarded local graph for terminal recipes

Used by

claimClock invariant bounds shared facilities

Sources

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

Phase 2 aligns this node to a Lean declaration.