Polynomial-time generation of input and certificate initialization clauses

Open

CookLevin.initialClauseEmitter_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$ . The initialization part of the Cook–Levin reduction, using the input on tape 0 and allowing a certificate of at most the prescribed length on tape 1, has a polynomial-time encoded emitter:

x \longmapsto \operatorname{encodeFormula}(\operatorname{startClauses}(\operatorname{shape}(x),\operatorname{reductionInit}(x,\operatorname{certLen}(x)))).

Here the shape width and certificate bound are exactly the existing tabWidth and certLen functions, with the seven parameters fixed. This isolates input-dependent initialization from the structural and transition clause generators. Blank-suffix constraints are generated separately.

Preamble

import Definitions.Def_CookLevin_Reduction
open CookLevin

Formal statement

theorem CookLevin.initialClauseEmitter_polyTime (k G Q cw dw ct dt : Nat) :
    IsPolyTimeComputable (fun x =>
      encodeFormula (startClauses ⟨k, G, Q, tabWidth cw dw ct dt x⟩
        (reductionInit (boolsToSymbols x) (certLen cw dw 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