Polynomial-time closure under ternary-majority amplification

Proved

SipserGacsLautemann.ternary_amplified_verifier_decides_in_polynomial_time

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

Let $V(x,r)$ be a Boolean predicate decided in polynomial time by the mission's deterministic two-tape Turing-machine model. For an input $x$ , put

d=\left\lceil\log_2(|x|+1)\right\rceil+3.

Split the supplied random string into $3^d$ padded blocks of equal inferred width, evaluate $V(x,\cdot)$ on every block, and combine those values with the complete depth- $d$ ternary tree whose internal gate is majority-of-three. The resulting predicate

A_V(x,\rho)=\operatorname{Maj}_3^{(d)}\bigl(V(x,r_1),\ldots,V(x,r_{3^d})\bigr)

is decidable in polynomial time.

This is the computational closure lemma for the amplification half of the Sipser–Gács–Lautemann formalization. The number of oracle-machine simulations is polynomial because $3^d$ is polynomial in $|x|$ , and each inferred block has length at most $|\rho|$ .

Formalization Note The block padding, ternary reshaping, recursive vote, and depth are exactly ternaryAmplifiedVerifierConstruction and its published helper definitions.

Preamble

import Definitions.Def_sipser_gacs_lautemann
import Definitions.Def_sgl_verifier_constructions

Formal statement

namespace SipserGacsLautemann

theorem ternary_amplified_verifier_decides_in_polynomial_time
    (verifier : List Bool → List Bool → Bool)
    (hverifier :
      DecidesInPolynomialTime
        (fun input : Fin 2 → List Bool =>
          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

Prove2me mission “The Sipser–Gács–Lautemann Theorem”, computational-closure frontier theorem af8010b9-bcbc-4b35-bc70-beb74d64f2bf, https://beta.prove2.me/

View graph