Exact ternary-majority scheduler reports base-machine acceptance

Disproved

SipserGacsLautemann.ternary_majority_scheduler_reports_base_accepts_with_polynomial_depth

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

Let a concrete two-tape verifier machine be given, with a polynomial clock, and let the ternary-majority tree have polynomially many leaves. This theorem isolates the exact finite-state scheduler needed by ternary amplification: on input $(x,\rho)$ , the scheduler splits $\rho$ into the inferred leaf blocks, runs the base machine on each virtual pair $(x,r_j)$ at its prescribed clock, folds the resulting acceptance bits by the complete ternary majority tree, and reports that Boolean result.

This theorem is predicate-free: it only schedules base-machine acceptance tests. The parent reduction separately uses the base-machine correctness hypothesis to identify those acceptance tests with the verifier predicate $V(x,r_j)$ .

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_polynomial_depth
    (states : Nat)
    (machine : Machine 2 states)
    (time : Nat → Nat)
    (depth : Nat → Nat)
    (htime : PolynomiallyBounded time)
    (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
              (ternaryBaseMachineVote
                machine time depth input) := by
  sorry

end SipserGacsLautemann

Source

Prove2me Sipser--Gács--Lautemann mission: ternary-majority machine scheduler obligation.

View graph