Ternary-majority verifier scheduler with polynomially bounded depth

Disproved

SipserGacsLautemann.ternary_majority_scheduler_from_machine_with_polynomial_depth

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

complexity-theoryschedulersipser-gacs-lautemannturing-machines

Let $V(x,r)$ be decided by a deterministic two-tape verifier machine in polynomial time. Let $d(n)$ be any depth function such that the number of leaves $3^{d(n)}$ is polynomially bounded in $n$ .

For input $(x,\rho)$ , split $\rho$ into $3^{d(|x|)}$ padded blocks of inferred equal width, evaluate $V(x,\cdot)$ on every leaf block, and combine the results with the complete ternary majority tree of depth $d(|x|)$ . The resulting predicate is decidable in polynomial time.

This isolates the uniform scheduler needed for the amplification verifier: the arithmetic hypothesis says only that the number of verifier calls is polynomial; the theorem asserts the actual finite-state multitape wrapper can perform those calls and fold the ternary-majority tree.

Preamble

import Definitions.Def_sipser_gacs_lautemann
import Definitions.Def_sgl_verifier_constructions

Formal statement

namespace SipserGacsLautemann

theorem ternary_majority_scheduler_from_machine_with_polynomial_depth
    (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)) :
    DecidesInPolynomialTime
      (fun input : Fin 2 → List Bool =>
        (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)) = true)) := by
  sorry

end SipserGacsLautemann

Source

Internal decomposition lemma for the Prove2me mission “The Sipser–Gács–Lautemann Theorem”, isolating the polynomially bounded ternary-majority scheduler from the specific SGL amplification depth.

View graph