Quadratic clock padding for formula-string recognition

Proved

CookLevin.isFormulaStringB_machine_quad_of_unary

by junyihjy · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theorycook-levinturing-machines

Suppose a well-formed multitape Turing machine recognizes whether the fixed input is a syntactically valid encoded formula at the unary quadratic clock $c_0(|x|+1)^2$ , uniformly for every certificate. Then the same machine gives the same verdict at the larger joint clock

c_0(|x|+|w|+1)^2.

The result isolates the monotone clock-padding step used when a verifier's global bound depends on both input and certificate lengths.

Preamble

import Definitions.Def_CookLevin_Verifier
open CookLevin
set_option autoImplicit false

Formal statement

theorem CookLevin.isFormulaStringB_machine_quad_of_unary
    (M : Machine) (k G c0 : Nat)
    (hwf : TuringMachine k G M)
    (hunary : ∀ x w : List Bool,
      DecidesIn M k (boolsToSymbols x) (boolsToSymbols w)
        (c0 * (x.length + 1) ^ 2) (isFormulaStringB x)) :
    ∀ x w : List Bool,
      DecidesIn M k (boolsToSymbols x) (boolsToSymbols w)
        (c0 * (x.length + w.length + 1) ^ 2) (isFormulaStringB x) := by sorry

View graph