Prove2Me

Polynomial-time closure under dropping the final output bit

Proved
CookLevin.polyTime_dropLast

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

complexitycook-levinturing-machines

If a bit-string function is computed by a polynomial-time multitape Turing machine, then the function obtained by deleting its final output bit is also polynomial-time computable. This isolates the output-trimming transducer used by polyTime_dropLast_append.

Preamble
import Definitions.Def_CookLevin_Complexity
open CookLevin
Formal statement
namespace CookLevin
/-- Polynomial-time computability is closed under removing the final output bit. -/
theorem polyTime_dropLast
    (u : List Bool → List Bool)
    (hu : IsPolyTimeComputable u) :
    IsPolyTimeComputable (fun x => (u x).dropLast) := 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