Polynomial-time closure under concatenating two computed outputs

Proved

CookLevin.polyTime_append

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

complexitycook-levinturing-machines

Given polynomial-time computations of two bit-string functions on the same input, their outputs can be concatenated by a polynomial-time multitape Turing machine. This is the product-machine closure component consumed by polyTime_dropLast_append.

Preamble

import Definitions.Def_CookLevin_Complexity
open CookLevin

Formal statement

namespace CookLevin
/-- Polynomial-time bit-string functions are closed under output concatenation. -/
theorem polyTime_append
    (u v : List Bool → List Bool)
    (hu : IsPolyTimeComputable u)
    (hv : IsPolyTimeComputable v) :
    IsPolyTimeComputable (fun x => u x ++ v x) := by sorry
end CookLevin

Source

Machine-construction decomposition of https://prove2.me/theorems/9dfa5b11-e968-4a25-995d-f22d77d35dbd under the CookLevinLean cost model: https://github.com/Rizvonium/cook_levin_lean_v1/blob/main/CookLevinLean/Complexity.lean

View graph