claimroutineinferred_dep

Simultaneous work-space bound on all tapes

All work heads stay within ρBn\rho B_n, so work space is at most Klog⁡(n+2)K\log(n+2)
gives the space guarantee and the configuration count base
Claim·§13.5 Explicit simultaneous bounds·inside thmEffective compiler from randomized to deterministic logspace

Statement (paper)

On every input of length nn, every work head stays in [−ρBn,ρBn][-\rho B_n,\rho B_n], so that the library's live data and all callback data satisfy this bound simultaneously. Encoding each work alphabet of size gig_i in max⁡{1,⌈log⁡2gi⌉}≤g\max\{1,\lceil\log_2 g_i\rceil\}\le g bits per symbol, the total work data is at most t(2ρBn+1)g≤SBnt(2\rho B_n+1)g\le SB_n, and even 2SBn≤KLn2SB_n\le K L_n where Ln=log⁡2(n+2)L_n=\log_2(n+2), since Bn≤2LnB_n\le 2L_n.

In plain English

On every input of length nn, every work head of the compiled machine stays within [−ρBn,ρBn][-\rho B_n,\rho B_n], so the total work data, encoded at at most gg bits per symbol, is at most t(2ρBn+1)g≤SBnt(2\rho B_n+1)g\le SB_n, and even 2SBn≤KLn2SB_n\le K L_n with Ln=log⁡2(n+2)L_n=\log_2(n+2).

Why it's here

This turns the head-position bound into a concrete work-space count that holds at once for the library's live data and all callback data, which gives the Klog⁡(n+2)K\log(n+2) space guarantee of the theorem. The final step uses Bn≤2LnB_n\le 2L_n, and the explicit bound on the number of cells and bits per cell is what the bit-time configuration count in the next claim relies on.
Classified routine:
Direct bookkeeping from the earlier head-position bound: it encodes each work alphabet in binary, counts cells times bits per cell, and applies Bn≤2LnB_n\le 2L_n. This is a standard space-accounting calculation.

Uses

claimFixed deterministic library decides interpreter promiseclaimCallback compiles virtual padded input reads

Used by

claimBit-time bound by configuration counting

Sources

PaperOpen
Section
§13.5 Explicit simultaneous bounds
Page
—
Label
—
Line
sections/compiler.tex:452
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Simultaneous work-space bound for all tapes" rests on claim-thm-effective-simulation-1
  • info
    inferred_dep
    outline: "Simultaneous work-space bound for all tapes" rests on claim-thm-effective-simulation-3