Polynomial-time closure under concatenation of encoded CNF formulas

Proved

CookLevin.polyTime_encodeFormula_append

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

clause-generationcook-levinpolynomial-timeturing-machine

Let $f$ and $g$ send bit strings to CNF formulas. Suppose their encoded outputs are each computable in polynomial time by the CookLevin multi-tape machine model. Then so is their formula concatenation:

x \longmapsto \operatorname{encodeFormula}(f(x) \mathbin{+\!+} g(x)).

The polynomial constants and number of tapes in the conclusion are existential and may exceed those of both input machines. This is a reusable assembly lemma for separately generated clause families; it does not assert composition with an exact additive running-time bound.

Preamble

import Definitions.Def_CookLevin_Reduction
open CookLevin

Formal statement

theorem CookLevin.polyTime_encodeFormula_append (f g : List Bool → Formula)
    (hf : IsPolyTimeComputable (fun x => encodeFormula (f x)))
    (hg : IsPolyTimeComputable (fun x => encodeFormula (g x))) :
    IsPolyTimeComputable (fun x => encodeFormula (f x ++ g 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