claimroutineinferred_dep

Bit-time bound by configuration counting

Configuration counting bounds

D

H(n+2)^c

bit operations

gives the time bound of the compiled machine

Claim·§13.5 Explicit simultaneous bounds·inside thmEffective compiler from randomized to deterministic logspace

Statement (paper)

For every input

x

of length

n

\operatorname{time}_{\mathrm{bit}}(D,x)\le H(n+2)^c

. Indeed, the deterministic halting computation of

D

x

makes at most

q_D(n+2)(2\rho B_n+1)^t g^{t(2\rho B_n+1)}\le q_D(n+2)2^{SB_n}\le q_D(n+2)^c

finite-alphabet transitions, and each transition costs at most

100(u+1)^8\le 2^{(u+100)^2}

elementary bit operations.

In plain English

On every input of length

n

, the deterministic machine

D

runs in at most

H(n+2)^c

elementary bit operations, a polynomial in

n+2

Why it's here

Given the work-space bound from the previous claim, the number of distinct configurations of

D

is at most

2^{SB_n}

, which is polynomial in

n+2

because the space is logarithmic. The halting run therefore makes polynomially many finite-alphabet transitions, and each costs a bounded number of bit operations. Multiplying the two gives the time bound

H(n+2)^c

in the theorem.

Classified routine:

Standard configuration-counting argument: a halting deterministic machine with logarithmic space never repeats a configuration, so its running time is at most the number of configurations, which is polynomial (classical L ⊆ P bound). Combined here with the work-space bound from the previous claim and a per-transition bit-cost estimate.

Uses

claimSimultaneous work-space bound on all tapes

Used by

Nothing in the paper

Sources

PaperOpen

Section: §13.5 Explicit simultaneous bounds
Page: —
Label: —
Line: sections/compiler.tex:473

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Bit-time bound by configuration counting" rests on claim-thm-effective-simulation-4