Ternary-majority scheduler reports acceptance under a uniform halt bound

Disproved

SipserGacsLautemann.ternary_majority_scheduler_reports_accepts_under_halt_bound

by Henry Yuen · Jul 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theorysipser-gacs-lautemannturing-machine

This is the ternary-majority scheduler construction with an explicit uniform halt bound.

Fix a two-tape machine $M$ , a depth function $d(n)$ whose number of ternary leaves $3^{d(n)}$ is polynomially bounded, and a polynomially bounded halt bound $B(n)$ . The theorem asks for a finite-state two-tape scheduler which, on input $(x,r)$ , evaluates the ternary majority tree over the leaf random strings extracted from $r$ .

The hypothesis for each input says that every relevant leaf query has halted by time $B(|x,r|)$ . Under that hypothesis, the scheduler reports the ternary majority of the Boolean values

\mathbf{1}[M \text{ accepts } (x,\rho) \text{ within } B(|x,r|) \text{ steps}]

over all leaves $\rho$ in the ternary tree. This isolates the concrete scheduler/simulation construction from the separate verifier-correctness argument.

Preamble

import Definitions.Def_sgl_ternary_machine_vote_data
import Definitions.Def_sgl_machine_infrastructure

Formal statement

namespace SipserGacsLautemann

theorem ternary_majority_scheduler_reports_accepts_under_halt_bound
    (states : Nat)
    (machine : Machine 2 states)
    (depth : Nat → Nat)
    (bound : Nat → Nat)
    (hbound : PolynomiallyBounded bound)
    (hleaves : PolynomiallyBounded (fun n : Nat => 3 ^ depth n)) :
    ∃ (State : Type) (_ : Fintype State)
      (scheduler : TypedMachine 2 State)
      (schedulerTime : Nat → Nat),
      PolynomiallyBounded schedulerTime ∧
        ∀ input : Fin 2 → List Bool,
          (∀ random : List Bool,
            random.length ≤ (input 1).length →
              ∃ result : Bool,
                machine.result
                    (machine.run
                      (ternaryTwoTapeInput input random)
                      (bound (totalInputLength input))).state =
                  some result) →
          scheduler.result
              (scheduler.run input
                (schedulerTime (totalInputLength input))).state =
            some
              (let d := depth (input 0).length
               let leafCount := 3 ^ d
               let randomBits := (input 1).length / leafCount
               ternaryVoteConstruction
                 (fun random : List Bool =>
                   @decide
                    (machine.acceptsWithin
                      (ternaryTwoTapeInput input random)
                      (bound (totalInputLength input)))
                    (Classical.propDecidable _))
                 d
                 (ternaryListTreeConstruction
                   randomBits d (input 1))) := by
  sorry

end SipserGacsLautemann

Source

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

View graph