Amplification-depth ternary scheduler under a halt bound

Proved

SipserGacsLautemann.ternary_amplification_scheduler_reports_accepts_under_halt_bound

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

complexity-theoryproof-engineeringturing-machines

Fix a two-tape verifier machine and a polynomial halt bound. This theorem asserts the existence of a two-tape scheduler for the specific ternary majority tree used by ternaryAmplifiedVerifierConstruction: on input tapes (x, R), let

d = mathrm{amplificationDepthConstruction}(|x|),qquad L = 3^d,qquad r = |R|/L.

Assuming every verifier call on a random string of length at most |R| has halted by the supplied bound, the scheduler returns the ternary majority vote over the L length-r leaves decoded from R, where each leaf vote is the bounded acceptance predicate of the base machine.

This is the computable-depth version needed for the SGL amplification construction; unlike the more general polynomial-depth scheduler statement, the depth function is fixed to the explicit amplification depth.

Preamble

import Definitions.Def_sgl_ternary_machine_vote_data
import Definitions.Def_sgl_machine_infrastructure

Formal statement


namespace SipserGacsLautemann

theorem ternary_amplification_scheduler_reports_accepts_under_halt_bound
    (states : Nat)
    (machine : Machine 2 states)
    (bound : Nat → Nat)
    (hbound : PolynomiallyBounded bound) :
    ∃ (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 := amplificationDepthConstruction (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

Proof-engineering lemma for the Sipser--Gacs--Lautemann Prove2me mission; specializes the ternary scheduler obligation to the explicit amplificationDepthConstruction used in the formalized majority-amplification step.

View graph