Bounded unary-offset scheduler for a halting polynomial-time base machine

Proved

SipserGacsLautemann.bounded_unary_offset_scheduler_reports_predicate_from_machine

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

complexity-theorysipser-gacs-lautemannturing-machines

Let a four-tape machine decide a predicate within a polynomial clock. This theorem isolates the finite-state scheduler needed for bounded unary-offset search under that halting/correctness hypothesis.

On input $(x,e,u)$ , the scheduler must examine the virtual inputs

(x,e,u,1^i) \qquad 0\le i\le |u|,

run the supplied base decider on those virtual inputs, and return whether one of the corresponding predicate instances is true. Unlike the earlier arbitrary explicit-bound scheduler obligation, this statement uses the polynomial-time correctness hypothesis, so the machine only has to schedule halting base-decider calls rather than decide nonhalting timeout behavior.

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_predicate_from_machine
    {predicate : (Fin 4 → List Bool) → Prop}
    [DecidablePred predicate]
    (states : Nat)
    (machine : Machine 4 states)
    (time : Nat → Nat)
    (htime : PolynomiallyBounded time)
    (hcorrect :
      ∀ input : Fin 4 → List Bool,
        (machine.acceptsWithin input
            (time (totalInputLength input)) ↔
          predicate input) ∧
        (machine.rejectsWithin input
            (time (totalInputLength input)) ↔
          ¬ predicate input)) :
    ∃ (State : Type) (_ : Fintype State)
      (scheduler : TypedMachine 3 State)
      (schedulerTime : Nat → Nat),
      PolynomiallyBounded schedulerTime ∧
        ∀ input : Fin 3 → List Bool,
          scheduler.result
              (scheduler.run input
                (schedulerTime (totalInputLength input))).state =
            some
              (@decide
                (∃ offset : Fin ((input 2).length + 1),
                  predicate
                    (boundedUnaryOffsetInput input offset.val))
                (Classical.propDecidable _)) := by
  sorry

end SipserGacsLautemann

Source

Prove2me Sipser--Gács--Lautemann mission; DPT-specific replacement for the bounded-unary explicit-bound scheduler leaf.

View graph