Machine-level bounded existential search over unary offsets

Proved

SipserGacsLautemann.bounded_exists_unary_offset_from_machine

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

bounded-searchcomplexity-theoryschedulerturing-machines

Let $P(x,e,u,o)$ be decided by a concrete deterministic four-tape machine in polynomial time. This theorem asserts that there is a concrete polynomial-time three-tape machine deciding

\exists i \le |u|,\; P(x,e,u,1^i),

where the fourth virtual tape is generated as the unary string $1^i$ and the scheduler tries all $|u|+1$ offsets.

This is the machine-level construction underlying the generic bounded-unary scheduler closure.

Preamble

import Definitions.Def_sipser_gacs_lautemann

Formal statement

namespace SipserGacsLautemann

theorem bounded_exists_unary_offset_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)) :
    DecidesInPolynomialTime
      (fun input : Fin 3 → List Bool =>
        decide
          (∃ offset : Fin ((input 2).length + 1),
            predicate (fun j : Fin 4 =>
              if j = 0 then input 0
              else if j = 1 then input 1
              else if j = 2 then input 2
              else List.replicate offset.val true)) = true) := by
  sorry

end SipserGacsLautemann

Source

Internal machine-level scheduler decomposition lemma for the Prove2me mission “The Sipser–Gács–Lautemann Theorem”.

View graph