Prove2Me

Polynomial-time emitter for blank-suffix clauses

Proved
CookLevin.blankSuffixClauseEmitter_polyTime

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

clause-generationcook-levinpolynomial-timeturing-machine

For fixed tableau parameters, the encoded blank-suffix clauses on certificate tape 1 can be emitted by a multi-tape Turing machine in time polynomial in the input length.

This isolates the certificate blank-suffix family from the nine-family structural aggregate.

Formal statement
import Definitions.Def_CookLevin_Reduction
open CookLevin

theorem CookLevin.blankSuffixClauseEmitter_polyTime
    (k G Q cw dw ct dt : Nat) :
    IsPolyTimeComputable (fun x =>
      encodeFormula (blankSuffixClauses ⟨k, G, Q, tabWidth cw dw ct dt x⟩ 1)) := by sorry
Source
Decomposition of CookLevin.structuralClauseEmitters_polyTime: https://prove2.me/theorems/ea203338-20bc-4754-986a-bf8cb7ef70f8

View graph