Core existence theorem for multi-tape reduction emitter machine

Disproved

CookLevin.reductionEmitM_exists_core

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

cook-levinemitterreduction

For any verifier machine $M_v$ and dimensions $k, G$ , there exists a multi-tape reduction emitter machine $M$ satisfying TuringMachine k G M.

Formal statement

import Definitions.Def_CookLevin_Basic
import Definitions.Def_CookLevin_Satisfiability
import Definitions.Def_CookLevin_Complexity
import Definitions.Def_CookLevin_Reduction

open CookLevin

theorem CookLevin.reductionEmitM_exists_core (Mv : Machine) (k G : Nat) :
    ∃ M : Machine, TuringMachine k G M := by sorry

Source

https://github.com/Rizvonium/cook_levin_lean_v1/blob/main/CookLevinLean/Emit.lean

View graph