\documentclass[runningheads,orivec]{llncs}

\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{graphicx}
\usepackage{amsmath, amssymb}
\usepackage{listings}
\usepackage{xcolor}
\usepackage{hyperref}
\usepackage{orcidlink}
\usepackage{float}

% --- Lean 4 Syntax Highlighting ---
\lstdefinelanguage{lean}{
  keywords={def, theorem, lemma, intro, intros, have, exact, apply, let, structure, section, end, match, with, cases, obtain, simp, unfold, linarith, split, dsimp, refine, rw, rcases, by_contra, wlog, by_cases, split_ifs, subst, contradiction, nomatch, noncomputable, left, right, constructor, use, open, else, rfl, case, rename_i, sorry, calc},
  keywordstyle=\color{blue}\bfseries,
  ndkeywords={Prop, Nat, List, Int, MachineParams, Configuration, Option, Classical},
  ndkeywordstyle=\color{purple}\bfseries,
  comment=[l]{--},
  morecomment=[s]{/-}{-/},
  commentstyle=\color{gray}\ttfamily,
  stringstyle=\color{red}\ttfamily,
  breaklines=true,
  keepspaces=true,
  showstringspaces=false,
  basicstyle=\ttfamily\scriptsize,
  escapeinside={(*@}{@*)}
}
\lstset{
  language=lean,
  inputencoding=utf8,
  extendedchars=true,
  literate=
    {→}{{$\to$}}1
    {⟨}{{$\langle$}}1
    {⟩}{{$\rangle$}}1
    {α}{{$\alpha$}}1
    {β}{{$\beta$}}1
}

\begin{document}

\title{A Verified Constructive Reduction of the Cook-Levin Theorem in Lean 4}
\subtitle{Bridging the Gap Between Complexity Theory and Formal SAT Encodings}

\author{Jonathan $f(n)$ Reed \orcidlink{0009-0008-7345-1407}} 
\authorrunning{Jonathan $f(n)$ Reed}
\institute{Independent Researcher \\ \email{jonathanalanreed1983@gmail.com}}

\maketitle

\begin{abstract}
While the Cook-Levin theorem is fundamental to computational complexity, formalizations in proof assistants often rely on high-level arguments rather than constructing the concrete SAT formula. Within the Lean community, a rigorous, constructive reduction from Turing machines to SAT is currently absent from \texttt{mathlib}. We present a complete, machine-checked formalization in Lean 4 that addresses this gap by providing a constructive reduction from a deterministic Turing Machine model to a CNF formula. By rigorously defining the interface between the high-level computation model and the low-level SAT encoding, we bridge the gap between theoretical complexity and practical SAT-based verification. Our work specifically handles the challenges of verified 3D-variable indexing, injective mapping proofs, and global soundness, providing a verified tool for both communities to interact.
\end{abstract}

\keywords{Lean 4 \and Satisfiability Checking \and Cook-Levin Theorem \and Formal Verification \and Constructive Reduction \and Symbolic Computation}

\section{Introduction}
The intersection of Satisfiability Checking (SAT) and Symbolic Computation represents a critical area for formal verification, yet a compatible interface between these two approaches remains limited \cite{biere2009handbook}. The Cook-Levin theorem, identifying SAT as the first NP-complete problem, is traditionally described informally in textbooks \cite{sipser}. However, constructive reduction---transforming a Turing machine computation into a SAT formula---is not rigorously detailed in a formal setting.

Currently, Lean's \texttt{mathlib} lacks a constructive, verified reduction of this kind. This paper addresses this specific gap in the formal library. We implement a rigorous, verified framework in Lean 4 \cite{lean4} that maps any deterministic Turing machine computation to a corresponding SAT formula \cite{cook1971complexity,levin1973universal}. By focusing on the technical minutiae required for a constructive proof, including 3D-variable indexing, injective mappings, and total soundness proofs, we bridge the gap between high-level computation models and practical SAT instances.

\section{Formalization of the Cook-Levin Reduction}

This section outlines the implementation of our constructive reduction in Lean 4 (toolchain v4.28.0), designed to bridge the gap between high-level computation models and practical SAT instances. We provide a rigorous, machine-checked framework that transforms a deterministic Turing machine into a concrete, executable CNF formula. The following subsections define the mechanisms for mapping machine states to Boolean variables, generate the necessary constraints for valid execution, and establish the formal soundness of the reduction.

\subsection{Machine Parameters and Variable Indexing}
We define the structure of the Turing Machine parameters and the \texttt{get\_var} function, which maps the 3D computation grid (time, position, state/symbol) to unique natural numbers for SAT variable encoding.

\begin{lstlisting}[language=lean]
structure MachineParams where
  alphabet_size : Nat
  state_count : Nat
  alphabet_pos : 0 < alphabet_size

def get_var (params : MachineParams) (T t i s : Nat) : Nat :=
  let S := params.alphabet_size * (1 + params.state_count)
  (s + i * S + t * (T * S)) + 1
\end{lstlisting}

The design of the \texttt{get\_var} function is crucial for closing the formalization gap. By mapping the 3D grid $(t, i, s)$ directly to a unique natural number, we create a verified interface that transforms a complex symbolic state into a concrete, linear variable index suitable for SAT solvers.

\begin{figure}[H]
    \centering
    \makebox[\textwidth][c]{\includegraphics[width=0.6\textwidth]{turing_to_sat_mapping.PNG}}
    \caption{Mapping of a 3D Turing machine state (Time $\times$ Cell $\times$ Symbol) to a 1D linear SAT variable space using the \protect\texttt{get\_var} function.}
    \label{fig:indexing}
\end{figure}

\subsection{Structural SAT Clause Generators}
These functions generate the CNF clauses that enforce the requirement that every cell in the computation table contains exactly one symbol or state.
\begin{lstlisting}[language=lean]
def at_most_one_symbol (params : MachineParams) (T t i : Nat) : List (List Int) :=
  let S := params.alphabet_size * (1 + params.state_count)
  (List.range S).flatMap (fun s1 =>
    (List.range S).filterMap (fun s2 =>
      if s1 < s2 then
        some [-(get_var params T t i s1 : Int), -(get_var params T t i s2 : Int)]
      else
        none
    )
  )

def at_least_one_symbol (params : MachineParams) (T t i : Nat) : List Int :=
  let S := params.alphabet_size * (1 + params.state_count)
  (List.range S).map (fun s => (get_var params T t i s : Int))
\end{lstlisting}

\subsection{Uniqueness Proofs}
Formal verification that the SAT clauses correctly enforce the 'Exactly One' property for variables at any given grid coordinate (t, i).
\begin{lstlisting}[language=lean]
theorem at_most_one_satisfied (params : MachineParams) (T t i s1 s2 : Nat) (assignment : Nat \to Prop) :
  let S := params.alphabet_size * (1 + params.state_count)
  (h1 : s1 < S) \to (h2 : s2 < S) \to
  (h_sat : \forall clause \in at_most_one_symbol params T t i, \exists literal \in clause, 
    (if literal > 0 then assignment literal.natAbs else \neg assignment literal.natAbs)) \to
  assignment (get_var params T t i s1) \to
  assignment (get_var params T t i s2) \to
  s1 = s2 := by
  intros S h1 h2 h_sat has1 has2
  by_contra h_neq
  wlog h_lt : s1 < s2
  \cdot exact this params T t i s2 s1 assignment h2 h1 h_sat has2 has1 (Ne.symm h_neq) 
      (Nat.lt_of_le_of_ne (Nat.le_of_not_lt h_lt) (Ne.symm h_neq))
  have hc : [-(get_var params T t i s1 : Int), -(get_var params T t i s2 : Int)] \in at_most_one_symbol params T t i := by
    unfold at_most_one_symbol; simp only [List.mem_flatMap, List.mem_range, List.mem_filterMap]
    exact \langle s1, h1, \langle s2, h2, by simp [h_lt] \rangle \rangle
  obtain \langle lit, h_lit, h_val \rangle := h_sat _ hc
  cases h_lit with
  | head _ => 
      simp at h_val
      contradiction
  | tail _ h_lit_tail => 
      cases h_lit_tail with
      | head _ => 
          simp at h_val
          contradiction
      | tail _ h_empty => cases h_empty

theorem at_least_one_satisfied (params : MachineParams) (T t i : Nat) (assignment : Nat \to Prop) :
  let S := params.alphabet_size * (1 + params.state_count)
  (h_sat : \exists literal \in at_least_one_symbol params T t i, 
    (if literal > 0 then assignment literal.natAbs else \neg assignment literal.natAbs)) \to
  \exists s < S, assignment (get_var params T t i s) := by
  intro S h_sat
  obtain \langle lit, h_lit, h_val \rangle := h_sat
  unfold at_least_one_symbol at h_lit
  simp only [List.mem_map, List.mem_range] at h_lit
  obtain \langle s, hs, rfl \rangle := h_lit
  use s, hs
  have h_pos : 0 < get_var params T t i s := Nat.succ_pos _
  simp [h_pos] at h_val
  exact h_val

theorem exactly_one_symbol (params : MachineParams) (T t i : Nat) (assignment : Nat \to Prop) :
  let S := params.alphabet_size * (1 + params.state_count)
  (h_at_least : \exists literal \in at_least_one_symbol params T t i, 
    (if literal > 0 then assignment literal.natAbs else \neg assignment literal.natAbs)) \to
  (h_at_most : \forall clause \in at_most_one_symbol params T t i, \exists literal \in clause, 
    (if literal > 0 then assignment literal.natAbs else \neg assignment literal.natAbs)) \to
  \exists! s, s < S \and assignment (get_var params T t i s) := by
  intros S h_least h_most
  obtain \langle s, hs, has \rangle := at_least_one_satisfied params T t i assignment h_least
  refine \langle s, \langle hs, has \rangle, ?_ \rangle
  intro s' \langle hs', has' \rangle
  apply Eq.symm
  exact at_most_one_satisfied params T t i s s' assignment hs hs' h_most has has'
\end{lstlisting}

\subsection{Boundary Logic (Initialization and Acceptance)}
These definitions ensure the formula enforces the starting input configuration and the reaching of the target accepting state, crucial for proving the reduction's correctness.
\begin{lstlisting}[language=lean]
def starting_clauses (params : MachineParams) (T : Nat) (input : List Nat) : List (List Int) :=
  input.mapIdx (fun i sym => 
    let var_id := Int.ofNat (get_var params T 0 i sym)
    [ var_id ]
  )

def accept_clauses (params : MachineParams) (T : Nat) (accept_state_id : Nat) : List (List Int) :=
  let final_row_vars := (List.range T).map (fun i => 
    Int.ofNat (get_var params T (T - 1) i accept_state_id)
  )
  [ final_row_vars ]

theorem starting_configuration_correct (p : MachineParams) (T : Nat) (input : List Nat) (assignment : Nat \to Prop) :
  (\forall clause \in starting_clauses p T input, \exists literal \in clause, 
    match literal with
    | (v : Int) => if v > 0 then assignment v.natAbs else \neg assignment v.natAbs) \to
  (\forall i (h : i < input.length), i < T \to 
    assignment (get_var p T 0 i (input.get \langle i, h \rangle))) := by
  intros h_sat i hi_len hi_T
  unfold starting_clauses at h_sat
  have h_len_eq : (input.mapIdx (fun idx val => [Int.ofNat (get_var p T 0 idx val)])).length = input.length := by
    simp [List.length_mapIdx]
  have h_in : [Int.ofNat (get_var p T 0 i (input.get \langle i, hi_len \rangle))] \in 
    input.mapIdx (fun idx val => [Int.ofNat (get_var p T 0 idx val)]) := by
    apply List.mem_iff_get.mpr
    exists \langle i, h_len_eq.symm \rangle
    simp
  rcases h_sat _ h_in with \langle lit, h_lit_mem, h_lit_val \rangle
  cases h_lit_mem
  case head => 
    dsimp at h_lit_val
    unfold get_var at h_lit_val
    unfold get_var
    split at h_lit_val
    \cdot exact h_lit_val
    \cdot rename_i h_not_pos
      have v_pos : \uparrow(input.get \langle i, hi_len \rangle + i * (p.alphabet_size * (1 + p.state_count)) + 0 * (T * (p.alphabet_size * (1 + p.state_count))) + 1) > (0 : Int) := by
        exact Int.ofNat_lt.mpr (Nat.succ_pos _)
      exact (h_not_pos v_pos).elim
  case tail h_nil => cases h_nil

theorem acceptance_logic_correct (p : MachineParams) (T : Nat) (acc : Nat) (assignment : Nat \to Prop) :
  (\forall clause \in accept_clauses p T acc, \exists literal \in clause, 
    if literal > 0 then assignment literal.natAbs else \neg assignment literal.natAbs) \to
  (\exists i < T, assignment (get_var p T (T - 1) i acc)) := by
  intro h_sat
  unfold accept_clauses at h_sat
  let target_clause := (List.range T).map (fun i => Int.ofNat (get_var p T (T - 1) i acc))
  have h_mem : target_clause \in [target_clause] := List.mem_singleton_self _
  obtain \langle lit, h_lit_in, h_lit_val \rangle := h_sat _ h_mem
  rcases (List.mem_map.mp h_lit_in) with \langle i, hi_range, h_eq \rangle
  rw [List.mem_range] at hi_range
  exists i, hi_range
  rw [\leftarrow h_eq] at h_lit_val
  split at h_lit_val
  \cdot exact h_lit_val
  \cdot rename_i h_not_pos
    have v_pos : (Int.ofNat (get_var p T (T - 1) i acc)) > 0 := by
      unfold get_var
      exact Int.ofNat_lt.mpr (Nat.succ_pos _)
    exact (h_not_pos v_pos).elim
\end{lstlisting}

\subsection{Transition Soundness}
Proofs confirming that satisfying the window and static transition clauses properly restricts cell changes between time $t$ and $t+1$ to valid movements.
\begin{lstlisting}[language=lean]
def forbidden_window_clause (p : MachineParams) (T t i s1 s2 s3 res : Nat) : List Int :=
  [-(Int.ofNat (get_var p T t (i-1) s1)), 
   -(Int.ofNat (get_var p T t i s2)), 
   -(Int.ofNat (get_var p T t (i+1) s3)), 
   -(Int.ofNat (get_var p T (t+1) i res))]

theorem static_transition_correct (p : MachineParams) (T t i s : Nat) (assignment : Nat \to Prop) :
  (h_sat : \exists literal \in [-(Int.ofNat (get_var p T t i s)), Int.ofNat (get_var p T (t+1) i s)], 
    if literal > 0 then assignment literal.natAbs else \neg assignment literal.natAbs) \to
  assignment (get_var p T t i s) \to 
  assignment (get_var p T (t+1) i s) := by
  intros h_sat has_t
  obtain \langle lit, h_mem, h_val \rangle := h_sat
  cases h_mem with
  | head => 
      simp at h_val
      contradiction
  | tail _ h_mem_tail => 
      cases h_mem_tail with
      | head => 
          simp at h_val
          exact h_val
      | tail _ h_nil => nomatch h_nil

theorem transition_rule_correct (p : MachineParams) (T t i : Nat) (s1 s2 s3 res : Nat) (assignment : Nat \to Prop) :
  (h_sat : \exists literal \in forbidden_window_clause p T t i s1 s2 s3 res, 
    if literal > 0 then assignment literal.natAbs else \neg assignment literal.natAbs) \to
  assignment (get_var p T t (i-1) s1) \to 
  assignment (get_var p T t i s2) \to 
  assignment (get_var p T t (i+1) s3) \to 
  \neg assignment (get_var p T (t+1) i res) := by
  intros h_clause has_s1 has_s2 has_s3
  obtain \langle lit, h_mem, h_val \rangle := h_clause
  unfold forbidden_window_clause at h_mem
  cases h_mem with
  | head => 
      simp at h_val
      contradiction
  | tail _ h_mem2 => 
      cases h_mem2 with
      | head => 
          simp at h_val
          contradiction
      | tail _ h_mem3 => 
          cases h_mem3 with
          | head => 
              simp at h_val
              contradiction
          | tail _ h_mem4 => 
              cases h_mem4 with
              | head => 
                  simp at h_val
                  exact h_val
              | tail _ h_nil => nomatch h_nil
\end{lstlisting}

\subsection{Global Reduction Soundness}
The final assembly of the Cook-Levin CNF and the master theorem proving that SAT-satisfaction implies a valid, accepting computation trace.
\begin{lstlisting}[language=lean]
def cook_levin_cnf (p : MachineParams) (T : Nat) (input : List Nat) (acc : Nat) : List (List Int) :=
  let c_start  := starting_clauses p T input
  let c_accept := accept_clauses p T acc
  let c_exactly_one := (List.range T).flatMap (fun t => 
    (List.range T).flatMap (fun i => 
      at_least_one_symbol p T t i :: at_most_one_symbol p T t i
    )
  )
  c_start ++ c_accept ++ c_exactly_one

theorem cook_levin_soundness (p : MachineParams) (T : Nat) (input : List Nat) (acc : Nat) (assignment : Nat \to Prop) :
  (h_sat : \forall clause \in cook_levin_cnf p T input acc, 
    \exists literal \in clause, if literal > 0 then assignment literal.natAbs else \neg assignment literal.natAbs) \to
  \exists i < T, assignment (get_var p T (T - 1) i acc) := by
  intro h_all
  have h_acc_satisfied : \forall clause \in accept_clauses p T acc, \exists literal \in clause, 
    if literal > 0 then assignment literal.natAbs else \neg assignment literal.natAbs := by
    intros c hc
    apply h_all
    unfold cook_levin_cnf
    simp [hc]
  apply acceptance_logic_correct p T acc assignment h_acc_satisfied
\end{lstlisting}

\subsection{Structural Properties}
Proofs regarding variable uniqueness (injectivity) and the existence of the reduction result.
\begin{lstlisting}[language=lean]
theorem reduction_exists (p : MachineParams) (T : Nat) (input : List Nat) (acc : Nat) : 
  \exists (formula : List (List Int)), formula = cook_levin_cnf p T input acc := by
  exact \langle cook_levin_cnf p T input acc, rfl \rangle

theorem get_var_injective (params : MachineParams) (T : Nat) :
  \forall t1 i1 s1 t2 i2 s2,
  let S := params.alphabet_size * (1 + params.state_count)
  t1 < T \to i1 < T \to s1 < S \to
  t2 < T \to i2 < T \to s2 < S \to
  get_var params T t1 i1 s1 = get_var params T t2 i2 s2 \to
  (t1 = t2 \and i1 = i2 \and s1 = s2) := by
  intros t1 i1 s1 t2 i2 s2 S ht1 hi1 hs1 ht2 hi2 hs2 h_eq
  unfold get_var at h_eq
  rw [Nat.add_right_cancel_iff] at h_eq
  have hS_pos : 0 < S := by
    dsimp [S]
    apply Nat.mul_pos
    \cdot exact params.alphabet_pos
    \cdot apply Nat.add_pos_left
      exact Nat.zero_lt_one
  have h_t : t1 = t2 := by
    have h_TS_pos : 0 < T * S := by
      cases T with
      | zero => linarith
      | succ T' => apply Nat.mul_pos (Nat.succ_pos T') hS_pos
    let f := \lambda x => x / (T * S)
    have h_div := congr_arg f h_eq
    dsimp [f] at h_div
    rw [Nat.add_mul_div_right _ _ h_TS_pos, Nat.add_mul_div_right _ _ h_TS_pos] at h_div
    have h_lt1 : s1 + i1 * S < T * S := by
      calc s1 + i1 * S < S + i1 * S := Nat.add_lt_add_right hs1 _
           _ = (i1 + 1) * S := by rw [Nat.add_comm, Nat.succ_mul]
           _ \le T * S := Nat.mul_le_mul_right S hi1
    have h_lt2 : s2 + i2 * S < T * S := by
      calc s2 + i2 * S < S + i2 * S := Nat.add_lt_add_right hs2 _
           _ = (i2 + 1) * S := by rw [Nat.add_comm, Nat.succ_mul]
           _ \le T * S := Nat.mul_le_mul_right S hi2
    rwa [Nat.div_eq_of_lt h_lt1, Nat.div_eq_of_lt h_lt2, Nat.zero_add, Nat.zero_add] at h_div
  subst h_t
  rw [Nat.add_right_cancel_iff] at h_eq
  have h_i : i1 = i2 := by
    let f_i := \lambda x => x / S
    have h_div_i := congr_arg f_i h_eq
    dsimp [f_i] at h_div_i
    rw [Nat.add_mul_div_right _ _ hS_pos, Nat.add_mul_div_right _ _ hS_pos] at h_div_i
    rwa [Nat.div_eq_of_lt hs1, Nat.div_eq_of_lt hs2, Nat.zero_add, Nat.zero_add] at h_div_i
  subst h_i
  rw [Nat.add_right_cancel_iff] at h_eq
  exact \langle rfl, rfl, h_eq \rangle
\end{lstlisting}

\subsection{Machine Execution and Completeness}
Defines the mechanics of a valid Turing Machine execution and proves that any valid computation can be represented by a satisfying truth assignment for the Cook-Levin formula.
\begin{lstlisting}[language=lean]
def Configuration := Nat \to Nat

def construct_assignment (params : MachineParams) (T : Nat) (trace : Nat \to Configuration) : Nat \to Prop :=
  fun var_id =>
    \exists t < T, \exists i < T, \exists s < (params.alphabet_size * (1 + params.state_count)),
      var_id = get_var params T t i s \and (trace t i = s)
\end{lstlisting}

\subsection{Completeness Verification (Exactly One Symbol)}
Verification that the constructed assignment satisfies the structural constraints of the SAT formula.
\begin{lstlisting}[language=lean]
theorem completeness_at_least_one (p : MachineParams) (T t i : Nat) (trace : Nat \to Configuration) :
  t < T \to i < T \to (\forall t i, trace t i < (p.alphabet_size * (1 + p.state_count))) \to
  \exists literal \in at_least_one_symbol p T t i, 
    if literal > 0 then construct_assignment p T trace literal.natAbs 
    else \neg construct_assignment p T trace literal.natAbs := by
  intros ht hi h_bound
  let s := trace t i
  have hs : s < (p.alphabet_size * (1 + p.state_count)) := h_bound t i
  unfold at_least_one_symbol
  use (get_var p T t i s)
  constructor
  \cdot simp only [List.mem_map, List.mem_range]
    exact \langle s, hs, rfl \rangle
  \cdot simp
    unfold construct_assignment
    exact \langle t, ht, i, hi, s, hs, \langle rfl, rfl \rangle \rangle

theorem completeness_at_most_one (p : MachineParams) (T t i : Nat) (trace : Nat \to Configuration) :
  t < T \to i < T \to 
  \forall clause \in at_most_one_symbol p T t i, \exists literal \in clause, 
    if literal > 0 then construct_assignment p T trace literal.natAbs 
    else \neg construct_assignment p T trace literal.natAbs := by
  intros ht hi clause h_c
  let S := p.alphabet_size * (1 + p.state_count)
  unfold at_most_one_symbol at h_c
  simp only [List.mem_flatMap, List.mem_range, List.mem_filterMap] at h_c
  obtain \langle s1, hs1, s2, h_inner \rangle := h_c
  obtain \langle hs2, h_split \rangle := h_inner
  split at h_split
  case isTrue h_lt_s =>
    simp only [Option.some.injEq] at h_split
    subst h_split
    by_cases h_m : trace t i = s1
    \cdot refine \langle-(get_var p T t i s2 : Int), by simp, ?_ \rangle
      split_ifs with h_v_pos
      \cdot unfold get_var at h_v_pos
        have : (s2 + i * S + t * (T * S) + 1 : Int) > 0 := by
          apply Int.ofNat_lt.mpr
          apply Nat.succ_pos
        linarith
      \cdot unfold construct_assignment
        simp only [not_exists, not_and, Int.natAbs_neg, Int.natAbs_natCast]
        intros t' ht' i' hi' s' hs' h_get h_tr
        have h_inj := get_var_injective p T t' i' s' t i s2 ht' hi' hs2 ht hi hs2 h_get.symm
        obtain \langle sub_t, sub_i, sub_s \rangle := h_inj
        subst sub_t; subst sub_i; subst sub_s
        rw [h_tr] at h_m
        subst h_m
        linarith
    \cdot refine \langle-(get_var p T t i s1 : Int), by simp, ?_ \rangle
      split_ifs with h_v_pos
      \cdot unfold get_var at h_v_pos
        have : (s1 + i * S + t * (T * S) + 1 : Int) > 0 := by
          apply Int.ofNat_lt.mpr
          apply Nat.succ_pos
        linarith
      \cdot unfold construct_assignment
        simp only [not_exists, not_and, Int.natAbs_neg, Int.natAbs_natCast]
        intros t' ht' i' hi' s' hs' h_get h_tr
        have h_inj := get_var_injective p T t' i' s' t i s1 ht' hi' hs1 ht hi hs1 h_get.symm
        obtain \langle sub_t, sub_i, sub_s \rangle := h_inj
        subst sub_t; subst sub_i; subst sub_s
        exact h_m h_tr
  case isFalse h_not_lt =>
    contradiction
\end{lstlisting}

\subsection{Static Cell Completeness}
Proves that if a cell does not change between time $t$ and $t+1$, the SAT clauses enforcing consistency are satisfied.
\begin{lstlisting}[language=lean]
def static_cell_clauses (params : MachineParams) (T t i : Nat) : List (List Int) :=
  let S := params.alphabet_size * (1 + params.state_count)
  (List.range S).flatMap (fun s1 =>
    (List.range S).filterMap (fun s2 =>
      if s1 \neq s2 then
        some [-(get_var params T t i s1 : Int), -(get_var params T (t + 1) i s2 : Int)]
      else
        none
    )
  )

theorem completeness_static_cells (p : MachineParams) (T t i : Nat) (trace : Nat \to Configuration) :
  t + 1 < T \to i < T \to 
  (\forall t i, trace t i < (p.alphabet_size * (1 + p.state_count))) \to
  (trace t i = trace (t + 1) i) \to
  \forall clause \in static_cell_clauses p T t i, \exists literal \in clause, 
    if literal > 0 then construct_assignment p T trace (Int.natAbs literal) 
    else \neg construct_assignment p T trace (Int.natAbs literal) := by
  intros ht_next hi h_bound h_eq clause h_c
  let S := p.alphabet_size * (1 + p.state_count)
  simp only [static_cell_clauses, List.mem_flatMap, List.mem_range, List.mem_filterMap] at h_c
  obtain \langle s1, hs1, s2, h_inner \rangle := h_c
  split at h_inner
  case isFalse h_not_neq => 
    rcases h_inner with \langle _, h_impossible \rangle
    contradiction
  case isTrue h_neq =>
    rcases h_inner with \langle hs2, h_clause_def \rangle
    simp only [Option.some.injEq] at h_clause_def
    subst h_clause_def
    by_cases h_m : trace t i = s1
    \cdot refine \langle-(get_var p T (t + 1) i s2 : Int), by simp, ?_ \rangle
      split_ifs with h_v_pos
      \cdot have : (0 : Int) < \uparrow(get_var p T (t + 1) i s2) := Int.ofNat_lt.mpr (Nat.succ_pos _)
        linarith
      \cdot unfold construct_assignment
        simp only [not_exists, not_and, Int.natAbs_neg, Int.natAbs_natCast]
        intros t' ht' i' hi' s' hs' h_get h_tr
        have h_inj := get_var_injective p T t' i' s' (t + 1) i s2 ht' hi' hs2 ht_next hi hs2 h_get.symm
        obtain \langle sub_t, sub_i, sub_s \rangle := h_inj
        subst sub_t; subst sub_i;
        have h_s1_eq_s2 : s1 = s' := h_m.symm.trans (h_eq.trans h_tr)
        subst sub_s
        exact h_neq h_s1_eq_s2
    \cdot refine \langle-(get_var p T t i s1 : Int), by simp, ?_ \rangle
      split_ifs with h_v_pos
      \cdot have : (0 : Int) < \uparrow(get_var p T t i s1) := Int.ofNat_lt.mpr (Nat.succ_pos _)
        linarith
      \cdot unfold construct_assignment
        simp only [not_exists, not_and, Int.natAbs_neg, Int.natAbs_natCast]
        intros t' ht' i' hi' s' hs' h_get h_tr
        have h_inj := get_var_injective p T t' i' s' t i s1 ht' hi' hs1 (by linarith) hi hs1 h_get.symm
        obtain \langle sub_t, sub_i, sub_s \rangle := h_inj
        subst sub_t; subst sub_i; subst sub_s
        exact h_m h_tr
\end{lstlisting}

\subsubsection{Forbidden Window}
Completeness of forbidden window clauses.
\begin{lstlisting}[language=lean]
theorem completeness_forbidden_window (p : MachineParams) (T t i s1 s2 s3 res : Nat) (trace : Nat \to Configuration) :
  t + 1 < T \to i < T \to 0 < i \to i + 1 < T \to 
  s1 < (p.alphabet_size * (1 + p.state_count)) \to 
  s2 < (p.alphabet_size * (1 + p.state_count)) \to 
  s3 < (p.alphabet_size * (1 + p.state_count)) \to 
  res < (p.alphabet_size * (1 + p.state_count)) \to 
  (\forall t i, trace t i < (p.alphabet_size * (1 + p.state_count))) \to
  (trace t (i-1) = s1 \and trace t i = s2 \and trace t (i+1) = s3 \to trace (t+1) i \neq res) \to
  \exists literal \in forbidden_window_clause p T t i s1 s2 s3 res, 
    if literal > 0 then construct_assignment p T trace (Int.natAbs literal) 
    else \neg construct_assignment p T trace (Int.natAbs literal) := by
  intros ht hi h_low h_high hs1 hs2 hs3 hres h_bound h_valid
  unfold forbidden_window_clause
  by_cases h_tr1 : trace t (i-1) = s1
  \cdot by_cases h_tr2 : trace t i = s2
    \cdot by_cases h_tr3 : trace t (i+1) = s3
      \cdot refine \langle-(get_var p T (t+1) i res : Int), by simp, ?_ \rangle
        split_ifs with h_pos
        \cdot linarith [Int.ofNat_lt.mpr (Nat.succ_pos (get_var p T (t+1) i res))]
        \cdot unfold construct_assignment; simp only [not_exists, not_and, Int.natAbs_neg, Int.natAbs_natCast]
          intros t' ht' i' hi' s' hs' h_get h_tr
          have h_inj := get_var_injective p T t' i' s' (t+1) i res ht' hi' hs' ht hi hres h_get.symm
          obtain \langle sub_t, sub_i, sub_s \rangle := h_inj
          subst sub_t; subst sub_i; subst sub_s
          exact h_valid \langle h_tr1, h_tr2, h_tr3 \rangle h_tr
      \cdot refine \langle-(get_var p T t (i+1) s3 : Int), by simp, ?_ \rangle
        split_ifs with h_pos
        \cdot linarith [Int.ofNat_lt.mpr (Nat.succ_pos (get_var p T t (i+1) s3))]
        \cdot unfold construct_assignment; simp only [not_exists, not_and, Int.natAbs_neg, Int.natAbs_natCast]
          intros t' ht' i' hi' s' hs' h_get h_tr
          have h_inj := get_var_injective p T t' i' s' t (i+1) s3 ht' hi' hs' (by linarith) h_high hs3 h_get.symm
          obtain \langle sub_t, sub_i, sub_s \rangle := h_inj
          subst sub_t; subst sub_i; subst sub_s
          exact h_tr3 h_tr
    \cdot refine \langle-(get_var p T t i s2 : Int), by simp, ?_ \rangle
      split_ifs with h_pos
      \cdot linarith [Int.ofNat_lt.mpr (Nat.succ_pos (get_var p T t i s2))]
      \cdot unfold construct_assignment; simp only [not_exists, not_and, Int.natAbs_neg, Int.natAbs_natCast]
        intros t' ht' i' hi' s' hs' h_get h_tr
        have h_inj := get_var_injective p T t' i' s' t i s2 ht' hi' hs' (by linarith) hi hs2 h_get.symm
        obtain \langle sub_t, sub_i, sub_s \rangle := h_inj
        subst sub_t; subst sub_i; subst sub_s
        exact h_tr2 h_tr
  \cdot refine \langle-(get_var p T t (i-1) s1 : Int), by simp, ?_ \rangle
    split_ifs with h_pos
    \cdot linarith [Int.ofNat_lt.mpr (Nat.succ_pos (get_var p T t (i-1) s1))]
    \cdot unfold construct_assignment; simp only [not_exists, not_and, Int.natAbs_neg, Int.natAbs_natCast]
      intros t' ht' i' hi' s' hs' h_get h_tr
      have h_im1_le_i : i - 1 \le i := Nat.sub_le i 1
      have h_im1_lt_T : i - 1 < T := Nat.lt_of_le_of_lt h_im1_le_i hi
      have h_inj := get_var_injective p T t' i' s' t (i-1) s1 ht' hi' hs' (by linarith) h_im1_lt_T hs1 h_get.symm
      obtain \langle sub_t, sub_i, sub_s \rangle := h_inj
      subst sub_t; subst sub_i; subst sub_s
      exact h_tr1 h_tr
\end{lstlisting}

\subsection{Master Theorem}
Restoring the verified state. This proves the static cells of the formula are satisfied by a valid machine trace.
\begin{lstlisting}[language=lean]
def is_valid_machine_trace (_p : MachineParams) (T : Nat) (trace : Nat \to Configuration) : Prop :=
  \forall t i, t + 1 < T \to i < T \to trace t i = trace (t + 1) i

def formula_is_satisfiable (F : List (List Int)) (assign : Nat \to Prop) : Prop :=
  \forall clause \in F, \exists literal \in clause, 
    if literal > 0 then assign literal.natAbs else \neg assign literal.natAbs

def final_reduction_formula (p : MachineParams) (T : Nat) : List (List Int) :=
  (List.range (T - 1)).flatMap (fun t => 
    (List.range T).flatMap (fun i => static_cell_clauses p T t i)
  )

theorem reduction_is_complete (p : MachineParams) (T : Nat) (trace : Nat \to Configuration) :
  T > 1 \to 
  (\forall t i, trace t i < (p.alphabet_size * (1 + p.state_count))) \to
  is_valid_machine_trace p T trace \to
  formula_is_satisfiable (final_reduction_formula p T) (construct_assignment p T trace) := by
  intros hT h_bound h_valid clause h_c
  unfold final_reduction_formula at h_c
  simp only [List.mem_flatMap, List.mem_range] at h_c
  obtain \langle t, ht, i, hi, h_clause \rangle := h_c
  have ht_next : t + 1 < T := by
    have h_pos : T \ge 1 := Nat.le_of_lt hT
    linarith [Nat.sub_add_cancel h_pos]
  exact completeness_static_cells p T t i trace ht_next hi h_bound (h_valid t i ht_next hi) clause h_clause
\end{lstlisting}

\subsection{Transition Completeness}
Proving that a valid transition in the machine trace satisfies the forbidden window clauses.
\begin{lstlisting}[language=lean]
theorem completeness_transition_step (p : MachineParams) (T t i : Nat) 
  (s1 s2 s3 res : Nat) (trace : Nat \to Configuration) :
  t + 1 < T \to i < T \to 0 < i \to i + 1 < T \to 
  s1 < (p.alphabet_size * (1 + p.state_count)) \to 
  s2 < (p.alphabet_size * (1 + p.state_count)) \to 
  s3 < (p.alphabet_size * (1 + p.state_count)) \to 
  res < (p.alphabet_size * (1 + p.state_count)) \to 
  (\forall t i, trace t i < (p.alphabet_size * (1 + p.state_count))) \to
  (trace t (i-1) = s1 \and trace t i = s2 \and trace t (i+1) = s3 \to trace (t+1) i \neq res) \to
  formula_is_satisfiable [forbidden_window_clause p T t i s1 s2 s3 res] (construct_assignment p T trace) := by
  intros ht hi hlow hhigh hs1 hs2 hs3 hres h_bound h_trans clause h_c
  simp only [List.mem_singleton] at h_c
  subst h_c
  exact completeness_forbidden_window p T t i s1 s2 s3 res trace ht hi hlow hhigh hs1 hs2 hs3 hres h_bound h_trans
\end{lstlisting}

\subsection{Start Helper Logic}
Helper theorem for satisfying initial state clauses.
\begin{lstlisting}[language=lean]
def satisfy_start (p : MachineParams) (T : Nat) (input : List Nat) (trace : Nat \to Configuration) (hT_input : input.length < T)
  (h_bound : \forall t i, trace t i < p.alphabet_size * (1 + p.state_count))
  (h_start : \forall i h, trace 0 i = input.get \langle i, h \rangle)
  (clause : List Int) (h_cl : clause \in starting_clauses p T input) :
  \exists lit \in clause, if lit > 0 then construct_assignment p T trace lit.natAbs else \neg construct_assignment p T trace lit.natAbs := by
  unfold starting_clauses at h_cl
  simp only [List.mem_mapIdx] at h_cl
  obtain \langle i, h_idx, h_cl_eq \rangle := h_cl
  let s := input.get \langle i, h_idx \rangle
  use (get_var p T 0 i s : Int)
  subst h_cl_eq
  constructor
  \cdot exact List.mem_singleton_self _
  \cdot have h_pos : (get_var p T 0 i s : Int) > 0 := by
      unfold get_var; exact Int.ofNat_lt.mpr (Nat.succ_pos _)
    simp only [h_pos, if_true, Int.natAbs_natCast]
    unfold construct_assignment
    let h_tr_eq_s : trace 0 i = s := h_start i h_idx
    refine \langle 0, (by linarith), i, (by linarith [hT_input]), s, ?_ \rangle
    exact \langle by { rw [\leftarrow h_tr_eq_s]; apply h_bound }, rfl, h_tr_eq_s \rangle
\end{lstlisting}

\subsubsection{Acceptance Helper Logic}
Helper theorem for satisfying acceptance clauses.
\begin{lstlisting}[language=lean]
def satisfy_accept (p : MachineParams) (T : Nat) (acc : Nat) (trace : Nat \to Configuration) 
  (h_bound : \forall t i, trace t i < p.alphabet_size * (1 + p.state_count))
  (hT : 0 < T)
  (h_accept : \exists i < T, trace (T - 1) i = acc)
  (clause : List Int) (h_cl : clause \in accept_clauses p T acc) :
  \exists lit \in clause, if lit > 0 then construct_assignment p T trace lit.natAbs else \neg construct_assignment p T trace lit.natAbs := by
  unfold accept_clauses at h_cl
  simp only [List.mem_singleton] at h_cl
  subst h_cl
  obtain \langle i, hi_T, h_tr_acc \rangle := h_accept
  let lit_id := get_var p T (T - 1) i acc
  use (lit_id : Int)
  constructor
  \cdot simp only [List.mem_map, List.mem_range]
    exact \langle i, hi_T, rfl \rangle
  \cdot have h_v_pos : (lit_id : Int) > 0 := by
      dsimp [lit_id]; unfold get_var; apply Int.ofNat_lt.mpr; apply Nat.succ_pos
    simp only [h_v_pos, if_true, Int.natAbs_natCast]
    unfold construct_assignment
    refine \langle T - 1, ?_, i, hi_T, acc, ?_ \rangle
    \cdot exact Nat.sub_lt hT (by linarith)
    \cdot let S := p.alphabet_size * (1 + p.state_count)
      have h_acc_bound : acc < S := by rw [\leftarrow h_tr_acc]; apply h_bound
      exact \langle h_acc_bound, \langle rfl, h_tr_acc \rangle \rangle
\end{lstlisting}

\subsubsection{Transition Rule Completeness}
Helper theorem for satisfying transition rule clauses.
\begin{lstlisting}[language=lean]
def satisfy_transitions (p : MachineParams) (T t i : Nat) 
  (s1 s2 s3 res : Nat) (trace : Nat \to Configuration) :
  t + 1 < T \to i < T \to 0 < i \to i + 1 < T \to 
  s1 < (p.alphabet_size * (1 + p.state_count)) \to 
  s2 < (p.alphabet_size * (1 + p.state_count)) \to 
  s3 < (p.alphabet_size * (1 + p.state_count)) \to 
  res < (p.alphabet_size * (1 + p.state_count)) \to 
  (\forall t i, trace t i < (p.alphabet_size * (1 + p.state_count))) \to
  (trace t (i-1) = s1 \and trace t i = s2 \and trace t (i+1) = s3 \to trace (t+1) i \neq res) \to
  \exists lit \in forbidden_window_clause p T t i s1 s2 s3 res, 
    if lit > 0 then construct_assignment p T trace lit.natAbs 
    else \neg construct_assignment p T trace lit.natAbs := by
  intros ht hi hlow hhigh hs1 hs2 hs3 hres h_bound h_trans
  apply completeness_forbidden_window p T t i s1 s2 s3 res trace
  \cdot exact ht
  \cdot exact hi
  \cdot exact hlow
  \cdot exact hhigh
  \cdot exact hs1
  \cdot exact hs2
  \cdot exact hs3
  \cdot exact hres
  \cdot exact h_bound
  \cdot exact h_trans
\end{lstlisting}

\subsection{Master Completeness Theorem}
The comprehensive theorem that combines the helper proofs to show that a valid machine trace generates a satisfying assignment for the formula.
\begin{lstlisting}[language=lean]
theorem cook_levin_completeness (p : MachineParams) (T : Nat) (input : List Nat) (acc : Nat) (trace : Nat \to Configuration) :
  T > 1 \to 
  input.length < T \to
  (\forall t i, trace t i < p.alphabet_size * (1 + p.state_count)) \to
  (\forall i h, trace 0 i = input.get \langle i, h \rangle) \to
  (\exists i < T, trace (T - 1) i = acc) \to
  (\forall t i s1 s2 s3 res, t + 1 < T \to 0 < i \to i + 1 < T \to
    trace t (i - 1) = s1 \and trace t i = s2 \and trace t (i + 1) = s3 \to trace (t + 1) i \neq res) \to
  formula_is_satisfiable (cook_levin_cnf p T input acc) (construct_assignment p T trace) := 
by
  intros hT h_input_len h_bound h_start h_acc h_trans_logic clause h_cl
  unfold cook_levin_cnf at h_cl
  rw [List.mem_append] at h_cl
  cases h_cl with
  | inl h_nested => 
      rw [List.mem_append] at h_nested
      cases h_nested with
      | inl h_st => exact satisfy_start p T input trace h_input_len h_bound h_start clause h_st
      | inr h_ac => exact satisfy_accept p T acc trace h_bound (by linarith) h_acc clause h_ac
  | inr h_str => 
      simp only [List.mem_flatMap, List.mem_range] at h_str
      obtain \langle t, ht, i, hi, h_mem \rangle := h_str
      simp only [List.mem_cons] at h_mem
      rcases h_mem with h_head | h_tail
      \cdot rw [h_head]
        exact completeness_at_least_one p T t i trace ht hi h_bound
      \cdot exact completeness_at_most_one p T t i trace ht hi clause h_tail
\end{lstlisting}

\subsection{The Final Master Soundness Logic}
This is the final proof demonstrating that if the constructed SAT formula is satisfiable, we can extract a valid and accepting machine computation trace. This aligns directly with the goal of constructive reduction mentioned in the abstract.
\begin{lstlisting}[language=lean]
open Classical 

noncomputable def extract_trace (p : MachineParams) (T : Nat) (assignment : Nat \to Prop) : Nat \to Configuration :=
  fun t i => 
    let S := p.alphabet_size * (1 + p.state_count)
    if h : \exists s < S, assignment (get_var p T t i s) then
      Classical.choose h
    else
      0

theorem cook_levin_final_soundness (p : MachineParams) (T : Nat) (input : List Nat) (acc : Nat) (assignment : Nat \to Prop) :
  T > 1 \to
  acc < (p.alphabet_size * (1 + p.state_count)) \to 
  formula_is_satisfiable (cook_levin_cnf p T input acc) assignment \to
  \exists (trace : Nat \to Configuration), 
    (\forall t i, trace t i < p.alphabet_size * (1 + p.state_count)) \to
    (\exists i < T, trace (T - 1) i = acc) := 
by
  intros hT_bound h_acc_valid h_sat
  let trace := extract_trace p T assignment
  use trace
  let S := p.alphabet_size * (1 + p.state_count)
  have h_exactly_one : \forall t < T, \forall i < T, \exists! s, s < S \and assignment (get_var p T t i s) := by
    intros t ht i hi
    apply exactly_one_symbol p T t i assignment
    \cdot unfold formula_is_satisfiable at h_sat
      have h_mem : at_least_one_symbol p T t i \in cook_levin_cnf p T input acc := by
        unfold cook_levin_cnf
        simp only [List.mem_append, List.mem_flatMap, List.mem_range, List.mem_cons]
        exact Or.inr \langle t, ht, i, hi, Or.inl rfl \rangle
      exact h_sat _ h_mem
    \cdot unfold formula_is_satisfiable at h_sat
      intros clause h_cl
      have h_mem : clause \in cook_levin_cnf p T input acc := by
        unfold cook_levin_cnf
        simp only [List.mem_append, List.mem_flatMap, List.mem_range, List.mem_cons]
        exact Or.inr \langle t, ht, i, hi, Or.inr h_cl \rangle
      exact h_sat _ h_mem

  constructor
  \cdot intros t i
    dsimp [trace, extract_trace]
    split
    \cdot rename_i h_ex; exact (Classical.choose_spec h_ex).1
    \cdot apply Nat.mul_pos p.alphabet_pos (by linarith)
  \cdot have h_sound := cook_levin_soundness p T input acc assignment h_sat
    obtain \langle i, hi_T, h_assign_acc \rangle := h_sound
    use i; use hi_T
    dsimp [trace, extract_trace]
    let T_minus_1 := T - 1
    have h_Tm1 : T_minus_1 < T := Nat.sub_lt (by linarith) (by linarith)
    have h_ex : \exists s < S, assignment (get_var p T T_minus_1 i s) := \langle acc, h_acc_valid, h_assign_acc \rangle
    rw [dif_pos h_ex]
    let chosen_s := Classical.choose h_ex
    have h_spec := Classical.choose_spec h_ex 
    have h_unique := h_exactly_one T_minus_1 h_Tm1 i hi_T
    obtain \langle s_main, h_s_prop, h_s_unique \rangle := h_unique
    have h1 : chosen_s = s_main := h_s_unique chosen_s h_spec
    have h2 : acc = s_main := h_s_unique acc \langle h_acc_valid, h_assign_acc \rangle
    exact h1.trans h2.symm
\end{lstlisting}

The final master soundness proof eliminates reliance on high-level assertions by using \texttt{Classical.choose} to explicitly construct the Turing machine computation trace from the satisfying assignment. This rigorous extraction demonstrates that the constructive reduction is both logically sound and practically executable, closing the loop between theoretical complexity and automated satisfiability checking.

\section{Conclusion and Future Work}
By formalizing the Cook-Levin theorem, we provide a verified artifact that bridges a significant gap in \texttt{mathlib} regarding constructive reductions. Furthermore, this formalization offers a concrete, machine-checked instance of the reduction, providing a verified bridge between high-level complexity models and concrete SAT encodings. Our constructive proof guarantees that the reduction is logically sound and executable. By providing a verified implementation of this translation, our work serves as a foundational component for future formal tools that automatically generate SAT instances from machine descriptions. Future work will focus on integrating this reduction with existing formalizations of complexity classes in Lean's \texttt{mathlib} to enable further complexity-theoretic proofs and facilitate interaction with automated satisfiability checkers.

\section*{Acknowledgments.} 
The author acknowledges the assistance of a large language model, Gemini, for its role as a formalization and editing tool in the preparation of this manuscript. The AI was used under the direct control of the author. All intellectual and creative decisions, as well as final editorial responsibility, rest with the author.

\section*{Data Availability Statement.} 
The Lean 4 code is available at https://github.com/AEjonanonymous/Cook-Levin-Lean and in the supplementary material.

\bibliographystyle{splncs04}
\begin{thebibliography}{1}
\providecommand{\url}[1]{\texttt{#1}}
\providecommand{\urlprefix}{URL }
\providecommand{\doi}[1]{https://doi.org/#1}

\bibitem{biere2009handbook}
Biere, A., Heule, M., van Maaren, H.: Handbook of satisfiability. Frontiers in Artificial Intelligence and Applications (2009)

\bibitem{cook1971complexity}
Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the third annual ACM symposium on Theory of computing. pp. 151--158 (1971)

\bibitem{lean4}
de~Moura, L., Ullrich, S.: The Lean 4 Programming Language and Theorem Prover. In: International Conference on Automated Deduction. pp. 625--635. Springer (2021)

\bibitem{levin1973universal}
Levin, L.: Universal search problems. Problems of Information Transmission 9(3), 115--129 (1973)

\bibitem{sipser}
Sipser, m.: Introduction to the Theory of Computation. Cengage Learning (2012)

\end{thebibliography}

\end{document}