A unary budget tape implements exact bounded machine acceptance

Proved

SipserGacsLautemann.unary_budget_simulation_reports_bounded_acceptance

by amorphic · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theorysipser-gacs-lautemannturing-machines

Let $M$ be any deterministic finite-state machine with $k$ tapes. There is one finite-state machine $C_M$ with $k+1$ tapes that works for every input and every natural-number budget $T$ . Its first $k$ tapes contain the original input; its last tape contains exactly $T$ copies of the bit true, supplying a unary clock.

After $T+1$ steps, $C_M$ has halted and reports true exactly when $M$ accepts within $T$ steps. It reports false when $M$ rejects by that time or has not halted by that time. Acceptance on the $T$ -th simulated step is included. The result also holds for $T=0$ and for machines that halt immediately. No termination assumption on $M$ is required.

The clock is input data, so the same finite machine works for every $T$ . This is the timeout simulation primitive needed for an explicit-budget SGL scheduler. Constructing the required polynomial-size clock from the scheduler's original input, and integrating it into that scheduler, are separate obligations.

Preamble

import Definitions.Def_sipser_gacs_lautemann
import Definitions.Def_sgl_machine_infrastructure

open SipserGacsLautemann

Formal statement

theorem SipserGacsLautemann.unary_budget_simulation_reports_bounded_acceptance
    {tapes states : Nat} (machine : Machine tapes states) :
    ∃ (State : Type) (_ : Fintype State)
      (clocked : TypedMachine (tapes + 1) State),
      ∀ (input : Fin tapes → List Bool) (budget : Nat),
        clocked.result
          (clocked.run
            (Fin.lastCases (List.replicate budget true) input)
            (budget + 1)).state =
          some (@decide (machine.acceptsWithin input budget)
            (Classical.propDecidable _)) := by
  sorry

Source

New supporting formalization of the standard unary timeout construction in the published Sipser–Gács–Lautemann machine model. Uses Henry Yuen’s public sgl_machine_infrastructure and sgl_embed_clock definitions (https://prove2.me/theorems/0f971a8e-ece0-4dab-927b-711041e8e42f and https://prove2.me/theorems/f3269127-dcff-431f-b2b5-dbfb902dbc34). Motivated by the remaining explicit-bound scheduler obligation https://prove2.me/theorems/5a84396c-95f6-4e79-8d72-ee390b3e7629; this lemma does not claim to close that scheduler.

View graph