Polynomial-time generation of the structural tableau clause families

Proved

CookLevin.structuralClauseEmitters_polyTime

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

clause-generationcook-levinpolynomial-timeturing-machine

Fix natural numbers $k,G,Q,c_w,d_w,c_t,d_t$ . For input $x$ , form the shape with $k$ tapes, alphabet bound $G$ , state bound $Q$ , and width given by tabWidth with these parameters. For each of the nine structural clause families—cell, head, state, read, link, inertia, halt, acceptance, and blank suffix on tape 1—the encoded formula is computable in polynomial time:

x \longmapsto \operatorname{encodeFormula}(F(\operatorname{shape}(x))).

All seven parameters are fixed before the input varies; the polynomial and implementing machine may depend on them and on the chosen family. No transition command or input-dependent initial contents are part of these families. The assertion covers zero-valued parameters as well as ordinary well-formed machine shapes.

Preamble

import Definitions.Def_CookLevin_Reduction
open CookLevin

Formal statement

theorem CookLevin.structuralClauseEmitters_polyTime (k G Q cw dw ct dt : Nat) :
    ∀ family ∈ ([cellClauses, headClauses, stateClauses, readClauses,
      linkClauses, inertiaClauses, haltClauses, acceptClauses,
      fun sh => blankSuffixClauses sh 1] : List (Shape → Formula)),
      IsPolyTimeComputable (fun x =>
        encodeFormula (family ⟨k, G, Q, tabWidth cw dw ct dt x⟩)) := 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