Bounded-unary scheduler reports acceptance under a uniform halt bound

Proved

SipserGacsLautemann.bounded_unary_offset_scheduler_reports_accepts_under_halt_bound

by Henry Yuen · Jul 24, 2026 · Mathlib c5ea003 (Lean v4.30.0)

complexity-theorysipser-gacs-lautemannturing-machine

This is the bounded-unary-offset scheduler construction with an explicit uniform halt bound.

Fix a four-tape machine $M$ and a polynomially bounded function $B(n)$ . The theorem asks for a finite-state three-tape scheduler such that, for every three-tape input $x$ , if every virtual query

\mathrm{boundedUnaryOffsetInput}(x,i)

has halted by time $B(|x|)$ , then the scheduler eventually reports whether at least one of those virtual queries is accepted by $M$ by time $B(|x|)$ .

This isolates the actual machine-construction part of the bounded existential search: the scheduler must enumerate the finitely many unary offsets, simulate the base machine on each generated query until the common halt bound is reached, and return the disjunction of the accepting outcomes.

Preamble

import Definitions.Def_sgl_bounded_unary_offset_data
import Definitions.Def_sgl_machine_infrastructure

Formal statement

namespace SipserGacsLautemann

theorem bounded_unary_offset_scheduler_reports_accepts_under_halt_bound
    (states : Nat)
    (machine : Machine 4 states)
    (bound : Nat → Nat)
    (hbound : PolynomiallyBounded bound) :
    ∃ (State : Type) (_ : Fintype State)
      (scheduler : TypedMachine 3 State)
      (schedulerTime : Nat → Nat),
      PolynomiallyBounded schedulerTime ∧
        ∀ input : Fin 3 → List Bool,
          (∀ offset : Fin ((input 2).length + 1),
            ∃ result : Bool,
              machine.result
                  (machine.run
                    (boundedUnaryOffsetInput input offset.val)
                    (bound (totalInputLength input))).state =
                some result) →
          scheduler.result
              (scheduler.run input
                (schedulerTime (totalInputLength input))).state =
            some
              (@decide
                (∃ offset : Fin ((input 2).length + 1),
                  machine.acceptsWithin
                    (boundedUnaryOffsetInput input offset.val)
                    (bound (totalInputLength input)))
                (Classical.propDecidable _)) := by
  sorry

end SipserGacsLautemann

Source

Internal decomposition lemma for the Prove2me mission “The Sipser–Gács–Lautemann Theorem”; refines the bounded-unary scheduler obligation by retaining the halt-bound condition needed for a uniform simulator.

View graph