Ternary majority scheduler with explicit polynomial simulation bound

Disproved

SipserGacsLautemann.ternary_majority_scheduler_reports_base_accepts_with_explicit_bound

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

complexity-theoryleansipser-gacs-lautemannturing-machines

Let a concrete two-tape verifier machine be given, let the ternary tree have polynomially many leaves, and fix an explicit polynomial upper bound $C(N+1)^d$ for each base-machine call. This theorem isolates the finite-state scheduler needed by ternary amplification when every leaf simulation is run to that explicit common bound.

On input $(x,\rho)$ , the scheduler splits $\rho$ into the inferred leaf blocks, evaluates whether the base machine accepts each virtual pair $(x,r_j)$ within $C(N+1)^d$ , folds the results with the complete ternary majority tree, and reports that Boolean result. The parent reduction uses base-machine exact-clock correctness and halting-state monotonicity to justify replacing the original opaque clock by this explicit upper bound.

Preamble

import Definitions.Def_sgl_ternary_machine_vote_data
import Definitions.Def_sgl_machine_infrastructure

Formal statement

namespace SipserGacsLautemann

theorem ternary_majority_scheduler_reports_base_accepts_with_explicit_bound
    (states : Nat)
    (machine : Machine 2 states)
    (depth : Nat → Nat)
    (coefficient degree : Nat)
    (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,
          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)
                      (coefficient *
                        (totalInputLength input + 1) ^ degree))
                    (Classical.propDecidable _))
                 d
                 (ternaryListTreeConstruction
                   randomBits d (input 1))) := by
  sorry

end SipserGacsLautemann

Source

Prove2me Sipser--Gacs--Lautemann mission ternary-amplification scheduler construction; explicit-bound correction of the machine-level scheduler obligation.

View graph