Polynomial-time generation of a fixed machine’s transition clauses

Open

CookLevin.transitionClauseEmitter_polyTime

by wurtle · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

clause-generationcook-levinpolynomial-timeturing-machine

Let $M$ be a well-formed $k$ -tape machine over an alphabet of size $G$ , and fix the certificate and running-time parameters. The transition-clause portion of its Cook–Levin tableau reduction can be emitted in polynomial time:

x \longmapsto \operatorname{encodeFormula}(\operatorname{transitionClauses}(\operatorname{shape}_M(x),M)).

The machine, tape count, alphabet size, and all polynomial parameters are fixed independently of $x$ . In particular, the enumeration of scanned-symbol tuples has fixed size. The output is the mission’s existing transition encoding, with state bound equal to the length of $M$ and width equal to tabWidth.

Preamble

import Definitions.Def_CookLevin_Reduction
open CookLevin

Formal statement

theorem CookLevin.transitionClauseEmitter_polyTime (Mv : Machine) (k G cw dw ct dt : Nat)
    (hwf : TuringMachine k G Mv) :
    IsPolyTimeComputable (fun x =>
      encodeFormula (transitionClauses
        ⟨k, G, Mv.length, tabWidth cw dw ct dt x⟩ Mv)) := by sorry

Source

Model-specific decomposition of CookLevin.reductionIsPolyTime: https://prove2.me/theorems/aff607bb-957c-459e-8d05-89e440634d91; exact definitions in Def_CookLevin_Tableau (tableauCNF and its clause constructors), Def_CookLevin_Reduction (cookLevinReduction, tabWidth, reductionInit), and Def_CookLevin_Satisfiability (encodeFormulaN). Construction pattern adapted from OpenAI ten-proofs, GapCVP.lean, commit 94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6, namespace CLStructuralWholeCNFOutputTM and CNFFiveFamilySourceIndexedORGadgetFinalCert.actualWholeStructuralCNFOutputComputable, lines 22849–22934 and 62083–62092: https://github.com/openai/ten-proofs/blob/94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6/GapCVP.lean#L62083 . The source uses a different machine model; these are explicit remaining porting obligations, not claims that its declarations apply unchanged.

View graph