Exact bounded-unary scheduler reports base-machine acceptance

Disproved

SipserGacsLautemann.bounded_unary_offset_scheduler_reports_base_accepts

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

Let a concrete four-tape machine and polynomial clock be given. This theorem isolates the exact finite-state scheduler needed for the bounded unary existential search: on a three-tape input $(x,e,u)$ , the scheduler tries the virtual inputs $(x,e,u,1^i)$ for offsets $0 \le i \le |u|$ and reports whether the base machine accepts one of those virtual inputs at its prescribed clock.

The theorem is deliberately machine-level and predicate-free. It only concerns the supplied machine acceptance relation. The semantic conversion from base-machine acceptance to the target predicate is handled separately by the parent reduction.

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_base_accepts
    (states : Nat)
    (machine : Machine 4 states)
    (time : Nat → Nat)
    (htime : PolynomiallyBounded time) :
    ∃ (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
              (boundedUnaryOffsetBaseAcceptDecision
                machine time input) := by
  sorry

end SipserGacsLautemann

Source

Prove2me Sipser--Gács--Lautemann mission: bounded-unary machine scheduler obligation.

View graph