Polynomial-time bounded existential search over unary offsets

Proved

SipserGacsLautemann.decidesInPolynomialTime_bounded_exists_unary_offset

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

bounded-searchcomplexity-theoryschedulerturing-machines

Let $P(x,e,u,o)$ be a decidable four-tape predicate that is decidable in polynomial time. Then the three-tape predicate

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

is also decidable in polynomial time, with the existential encoded by decide and offsets represented as unary strings of length $i$ .

This is the generic bounded-loop scheduler needed for the Lautemann shifted-cover verifier: it formalizes that a polynomial-time subroutine can be run for each of the $|u|+1$ possible offsets.

Preamble

import Definitions.Def_sipser_gacs_lautemann

Formal statement

namespace SipserGacsLautemann

theorem decidesInPolynomialTime_bounded_exists_unary_offset
    {predicate : (Fin 4 → List Bool) → Prop}
    [DecidablePred predicate]
    (hpredicate : DecidesInPolynomialTime predicate) :
    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 scheduler decomposition lemma for the Prove2me mission “The Sipser–Gács–Lautemann Theorem”.

View graph