Machine-level ternary amplified verifier scheduler

Proved

SipserGacsLautemann.ternary_amplified_verifier_decides_from_machine

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

bppcomplexity-theorypolynomial-timeturing-machine

Let $V(x,r)$ be decided by a concrete two-tape deterministic Turing machine $M$ with polynomial time bound $T$ , in the exact sense used by DecidesInPolynomialTime. This theorem asserts the machine-level construction for the ternary-majority amplification verifier: the predicate that decodes the supplied random string into a complete ternary tree of verifier queries and evaluates the recursive majority vote is decidable in polynomial time.

This isolates the ternary scheduler/loader/controller part of the remaining Sipser--Gács--Lautemann aggregation proof.

Preamble

import Definitions.Def_sipser_gacs_lautemann
import Definitions.Def_sgl_verifier_constructions

Formal statement

namespace SipserGacsLautemann

theorem ternary_amplified_verifier_decides_from_machine
    (verifier : List Bool → List Bool → Bool)
    (states : Nat)
    (machine : Machine 2 states)
    (time : Nat → Nat)
    (htime : PolynomiallyBounded time)
    (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 =>
        ternaryAmplifiedVerifierConstruction verifier
          (input 0) (input 1) = true) := by
  sorry

end SipserGacsLautemann

Source

Standard deterministic polynomial-time closure under polynomially many scheduled verifier calls, specialized to the ternary-majority amplifier in the Sipser--Gács--Lautemann proof.

View graph