Polynomial-time closure under terminal-bit deletion and output concatenation

Proved

CookLevin.polyTime_dropLast_append

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

closure-propertycook-levinpolynomial-timeturing-machine

Let $u$ and $v$ be polynomial-time computable bit-string functions in the Cook-Levin multi-tape machine model. Then the function that removes the final bit from $u(x)$ and concatenates the result with $v(x)$ is also polynomial-time computable. This isolates the output-splicing routine needed to concatenate two encoded CNF formula streams, whose first terminal delimiter must be removed.

Preamble

import Definitions.Def_CookLevin_Complexity
open CookLevin

Formal statement

namespace CookLevin
/-- Polynomial-time bit-string functions are closed under deleting the last bit of the first output and appending the second output. -/
theorem polyTime_dropLast_append
    (u v : List Bool → List Bool)
    (hu : IsPolyTimeComputable u)
    (hv : IsPolyTimeComputable v) :
    IsPolyTimeComputable (fun x => (u x).dropLast ++ v x) := by sorry
end CookLevin

Source

Reusable machine-construction lemma for CookLevin.polyTime_encodeFormula_append: https://prove2.me/theorems/52bfe0b2-676b-48d9-a6ee-9a495cd865fb . The encoding splice identity is proved directly from Definitions.Def_CookLevin_Satisfiability.

View graph