Ternary majority scheduler for a halting polynomial-time verifier machine

Disproved

SipserGacsLautemann.ternary_majority_scheduler_reports_verifier_vote_from_machine

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

complexity-theorysipser-gacs-lautemannturing-machines

Let a two-tape machine decide a verifier predicate in polynomial time, and suppose the ternary amplification tree has polynomially many leaves. This theorem isolates the finite-state scheduler that evaluates the verifier on each leaf block and returns the ternary majority vote.

On input $(x,\rho)$ , the scheduler splits $\rho$ into the inferred leaf blocks, runs the supplied halting verifier machine on each pair $(x,r_j)$ , and folds the resulting Booleans with the complete ternary majority tree. Unlike the earlier arbitrary explicit-bound version, this statement uses the polynomial-time correctness hypothesis and therefore only schedules halting verifier calls.

Preamble

import Definitions.Def_sgl_ternary_machine_vote_data
import Definitions.Def_sgl_machine_infrastructure

Formal statement


namespace SipserGacsLautemann

theorem ternary_majority_scheduler_reports_verifier_vote_from_machine
    (verifier : List Bool → List Bool → Bool)
    (states : Nat)
    (machine : Machine 2 states)
    (time : Nat → Nat)
    (depth : Nat → Nat)
    (htime : PolynomiallyBounded time)
    (hleaves : PolynomiallyBounded (fun n : Nat => 3 ^ depth n))
    (hcorrect :
      ∀ input : Fin 2 → List Bool,
        (machine.acceptsWithin input
            (time (totalInputLength input)) ↔
          verifier (input 0) (input 1) = true) ∧
        (machine.rejectsWithin input
            (time (totalInputLength input)) ↔
          ¬ verifier (input 0) (input 1) = true)) :
    ∃ (State : Type) (_ : Fintype State)
      (scheduler : TypedMachine 2 State)
      (schedulerTime : Nat → Nat),
      PolynomiallyBounded schedulerTime ∧
        ∀ input : Fin 2 → List Bool,
          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
                 (verifier (input 0)) d
                 (ternaryListTreeConstruction
                   randomBits d (input 1))) := by
  sorry

end SipserGacsLautemann

Source

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

View graph