Introduction

The Cook-Levin theorem states that CNF SAT is NP-complete. This mission formalizes the theorem over a multi-tape Turing machine model in Lean 4.

Main Goal

Prove CookLevin.cook_levin_theorem:

$$NPComplete SAT$$

under the decider and reduction hypotheses.

Reversible Binary 2D Cellular Automata: Disproof of $R = 18$ and Lower Bound $R \ge 33,076,358$

Problem Statement & Context

A two-dimensional binary cellular automaton (CA) on the infinite grid $\mathbb{Z}^2$ with the standard $3 \times 3$ Moore neighborhood $M = \{-1,0,1\}^2$ updates configurations $c : \mathbb{Z}^2 \to \{0,1\}$ via a local rule $f : \{0,1\}^M \to \{0,1\}$ according to:

$$F_f(c)(z) = f\Big(\big(c(z + u)\big)_{u \in M}\Big)$$

A local rule $f$ is reversible (or bijective) if its global map $F_f$ is a bijection of the configuration space $\{0,1\}^{\mathbb{Z}^2}$.

Let $R$ denote the exact number of reversible binary local rules on the $3 \times 3$ Moore neighborhood. A longstanding open conjecture asserted that $R = 18$, corresponding solely to the 18 trivial single-cell shifts and complemented shifts:

$$f(c) = c(z + u) \quad \text{or} \quad f(c) = 1 - c(z + u) \quad (u \in M)$$

In this mission, we formally disprove $R = 18$ by constructing an explicit non-trivial conserved-landscape rule $f_\star$ whose global map $F_{f_\star}$ is an involution on $\mathbb{Z}^2$, proving $19 \le R$. We further extend this result to establish $R \ge 33,076,358$.

---

Ladder of Proven Bounds

Bound Level	Proven Bound	Description / Mathematical Mechanism
$\mathbf{L_0}$	$R \ge 18$	Trivial single-cell shifts and complemented shifts ($2 \times 9 = 18$).
$\mathbf{L_1}$	$R \ge 19$	Disproof of $R = 18$ via explicit non-trivial conserved-landscape rule $f_\star$.
$\mathbf{L_2}$	$R \ge 33,070,982$	Conserved-landscape marker rule family ($24,576$ centered rules).
$\mathbf{L_3}$	$R \ge 33,076,358$	Incorporation of $5,376$ off-centre marker rules reading center cell $x_0$.
Symmetry	$R_{\text{rot90}} = 74$	Exactly 74 rules invariant under $90^\circ$ spatial rotations.
Torus	$	\mathcal{R}_{2,3}
Upper Limit	$R \le 2^{511}$	Derived from constant divergence condition $f(\mathbf{0}) \ne f(\mathbf{1})$.

---

Key Milestone Theorems

1. Theorem 1 (Trivial Rule Reversibility): All 18 single-cell shift and negated-shift rules are bijective global maps.
2. Theorem 2 (Conserved-Landscape Involution $f_\star$): The rule $f_\star$ complements a cell iff its W and SE neighbors are $1$ and the other six are $0$. $F_{f_\star} \circ F_{f_\star} = \text{id}$.
3. Theorem 3 (Non-Triviality & $19 \le R$): $f_\star$ differs from every trivial rule, establishing $19 \le R$ and disproving $R = 18$.
4. Theorem 4 (Constant Divergence Condition): Every reversible rule satisfies $f(\mathbf{0}) \ne f(\mathbf{1})$.