claimroutineinferred_dep

Probe copies fit enlarged A,D bound

Probe copies have live length at most A(w−w′)+D(t−j)A(w-w')+D(t-j)
arithmetic behind the probe-size bound
Claim·§11.2 Program states and record bounds·inside lemGuarded local graph for terminal recipes

Statement (paper)

Let Δw=w−w′>0\Delta w=w-w'>0 and Δt=t−j≥−a′Δw\Delta t=t-j\ge -a'\Delta w. For a fixed copy factor kk and bounded metadata cost hh, choose D≥kb0D\ge kb_0 and A≥ka0+(D−kb0)a′+hA\ge ka_0+(D-kb_0)a'+h, uniformly over all finite instruction cases. Then k(a0Δw+b0Δt)+h≤AΔw+DΔtk(a_0\Delta w+b_0\Delta t)+h\le A\Delta w+D\Delta t, so the complete live local portion of a probe at (w′,j)(w',j), including a fixed number of edited or saved controller copies, has length at most A(w−w′)+D(t−j)A(w-w')+D(t-j), and neither shared facilities nor the outside stack are copied.

In plain English

For Δw=w−w′>0\Delta w=w-w'>0 and Δt=t−j≥−a′Δw\Delta t=t-j\ge -a'\Delta w, choosing D≥kb0D\ge kb_0 and A≥ka0+(D−kb0)a′+hA\ge ka_0+(D-kb_0)a'+h gives k(a0Δw+b0Δt)+h≤AΔw+DΔtk(a_0\Delta w+b_0\Delta t)+h\le A\Delta w+D\Delta t. So a probe at (w′,j)(w',j), including a fixed number kk of edited or saved controller copies plus bounded metadata, has live local length at most A(w−w′)+D(t−j)A(w-w')+D(t-j), with shared facilities and the outside stack not copied.

Why it's here

This is the arithmetic behind the probe-size bound in the parent lemma. The allowance definition bounds each suspended record by a0Δw+b0Δta_0\Delta w+b_0\Delta t, and the clock condition Δt≥−a′Δw\Delta t\ge -a'\Delta w lets the extra slope D−kb0≥0D-kb_0\ge 0 be absorbed into AA. Fixed constants A,DA,D, uniform over the finitely many instruction cases, then cover kk copies and metadata cost hh.
Classified routine:
Elementary linear-inequality bookkeeping: with Δt≥−a′Δw\Delta t\ge -a'\Delta w, the excess slope (D−kb0)Δt(D-kb_0)\Delta t is absorbed into AΔwA\Delta w. It applies the allowance bound from def-ctrl-allowance to kk copies plus metadata.

Uses

defController allowance and clock certificateclaimGuarded deterministic finite graph keeps designated paths

Used by

Nothing in the paper

Sources

PaperOpen
Section
§11.2 Program states and record bounds
Page
—
Label
—
Line
sections/implementation.tex:405
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Probe copies fit enlarged A,D bound" rests on def:ctrl-allowance
  • info
    inferred_dep
    outline: "Probe copies fit enlarged A,D bound" rests on claim-lem-ctrl-local-graph-1