inductive NPCompleteness.BoolFormula : Type

Syntax of propositional Boolean formulas over variables indexed by ℕ. A BoolFormula is built from variables, the constants true and false, and the connectives ¬, ∧, ∨.

• var : ℕ → BoolFormula
• trueConst : BoolFormula
• falseConst : BoolFormula
• not : BoolFormula → BoolFormula
• and : BoolFormula → BoolFormula → BoolFormula
• or : BoolFormula → BoolFormula → BoolFormula

def NPCompleteness.instDecidableEqBoolFormula.decEq (x✝ x✝¹ : BoolFormula) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance NPCompleteness.instDecidableEqBoolFormula : DecidableEq BoolFormula

@[implicit_reducible]

instance NPCompleteness.instReprBoolFormula : Repr BoolFormula

def NPCompleteness.instReprBoolFormula.repr : BoolFormula → ℕ → Std.Format

@[reducible, inline]

abbrev NPCompleteness.BoolAssignment : Type

A truth assignment is a function from variable indices ℕ to Bool.

def NPCompleteness.BoolFormula.eval (σ : BoolAssignment) : BoolFormula → Bool

Evaluation of a Boolean formula under an assignment σ : ℕ → Bool. Returns the standard truth value of the formula under σ.

def NPCompleteness.BoolFormula.Satisfiable (φ : BoolFormula) : Prop

A formula φ is satisfiable if there exists an assignment σ with φ.eval σ = true.

def NPCompleteness.SAT : Set BoolFormula

SAT = {φ | φ is a satisfiable Boolean formula}.

def NPCompleteness.BoolFormula.IsLiteral : BoolFormula → Prop

A literal is a variable or the negation of a variable.

def NPCompleteness.BoolFormula.IsClause : BoolFormula → Prop

A clause is a disjunction of literals: either a single literal, or l ∨ (rest) where rest is itself a clause.

def NPCompleteness.BoolFormula.IsCNF : BoolFormula → Prop

A formula is in Conjunctive Normal Form (CNF) if it is a conjunction of clauses.

def NPCompleteness.BoolFormula.clauseLength : BoolFormula → ℕ

The length (number of literals) of a clause, counted by walking through the ors.

def NPCompleteness.BoolFormula.Is3Clause (φ : BoolFormula) : Prop

A 3-clause is a clause containing exactly 3 literals.

def NPCompleteness.BoolFormula.Is3CNF : BoolFormula → Prop

A formula is in 3CNF if it is a conjunction of 3-clauses.

def NPCompleteness.ThreeSAT : Set BoolFormula

3SAT = {φ | φ is a satisfiable 3CNF formula}.

theorem NPCompleteness.ThreeSAT.mk {φ : BoolFormula} (h3 : φ.Is3CNF) (hsat : φ.Satisfiable) : φ ∈ ThreeSAT

Membership in ThreeSAT from the conjunction of being 3CNF and being satisfiable.

def IsNPHard {Γ : Type} (B : Set (List Γ)) : Prop

A language B is NP-hard if every A ∈ NP is polynomial-time reducible to B, i.e. for all A ∈ NP, A ≤_P B.

def IsNPComplete {Γ : Type} (B : Set (List Γ)) : Prop

A language B is NP-complete if (1) B ∈ NP and (2) B is NP-hard, i.e. for every A ∈ NP, A ≤_P B.

def SATLang : Set (List NPCompleteness.BoolFormula)

The SAT language presented as a language of one-symbol input words [φ] where the singleton list contains a satisfiable Boolean formula.

theorem CookLevin.tableau_from_accepting_branch {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.NTM Q Γ) (w : List Γ) (n : ℕ) (branch : Fin (n + 1) → TuringMachine.Config Q Γ) (k : ℕ) (hstart : branch ⟨0, ⋯⟩ = M.initConfig w) (hsteps : ∀ (i : Fin n), M.step (branch i.castSucc) (branch i.succ)) (haccept : M.isAcceptConfig (branch ⟨n, ⋯⟩)) (hk : M.runsInTime fun (n : ℕ) => n ^ k) : Nonempty (TuringMachine.Tableau M w)

Given an accepting computation branch of an NTM M on input w of length at most n^k steps, we can produce a Tableau (an n^k × n^k array of cells representing the computation history) for M on w. This is the bridge from an accepting branch to the combinatorial object that the Cook–Levin formula encodes.

theorem CookLevin.accepts_from_tableau {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.NTM Q Γ) (w : List Γ) (tab : TuringMachine.Tableau M w) : M.accepts w

The converse direction: from any (accepting) tableau for M on w, the machine M accepts w.

@[inline]

def CookLevin.tableau_var_idx (i j σIdx dim numSymbols : ℕ) : ℕ

Index of the propositional variable x_{i,j,σ} indicating that cell (i,j) of a dim × dim tableau contains the symbol with index σIdx (out of numSymbols).

def CookLevin.build_conjunction : List NPCompleteness.BoolFormula → NPCompleteness.BoolFormula

Conjoin a list of Boolean formulas into a single BoolFormula. Empty list returns true; a singleton returns the formula itself.

def CookLevin.build_disjunction : List NPCompleteness.BoolFormula → NPCompleteness.BoolFormula

Disjoin a list of Boolean formulas into a single BoolFormula. Empty list returns false; a singleton returns the formula itself.

def CookLevin.build_phi_cell (dim numSymbols : ℕ) : NPCompleteness.BoolFormula

The Cook–Levin sub-formula φ_cell: enforces that each cell (i,j) of the tableau contains exactly one symbol — encoded as the conjunction of "at least one symbol" and "no two distinct symbols simultaneously".

def CookLevin.build_phi_start (dim numSymbols q₀Idx blankIdx : ℕ) (inputIdxs : List ℕ) : NPCompleteness.BoolFormula

The Cook–Levin sub-formula φ_start: enforces that the first row of the tableau encodes the initial configuration of M on input w — starting state q₀ in the left cell, then the input symbols, padded with blanks.

def CookLevin.build_phi_accept (dim numSymbols qAcceptIdx : ℕ) : NPCompleteness.BoolFormula

The Cook–Levin sub-formula φ_accept: enforces that the accepting state q_accept appears somewhere in the final row of the tableau.

def CookLevin.build_phi_move (dim numSymbols : ℕ) (legalWindows : List (List ℕ)) : NPCompleteness.BoolFormula

The Cook–Levin sub-formula φ_move: enforces that every consecutive pair of rows of the tableau differs only in a way consistent with one step of M — encoded by requiring that every 2 × 3 window matches one of the legal windows (determined from the transition function δ).

noncomputable def CookLevin.buildTableauFormula {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.NTM Q Γ) (k : ℕ) (w : List Γ) : NPCompleteness.BoolFormula

The Cook–Levin formula φ_{M,w} = φ_cell ∧ φ_start ∧ φ_move ∧ φ_accept. Given an NTM M, a polynomial-time exponent k, and an input w, this builds a Boolean formula that is satisfiable iff M has an accepting computation on w of length at most (|w|+1)^k.

theorem CookLevin.buildTableauFormula_correct {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.NTM Q Γ) (k : ℕ) (w : List Γ) : (buildTableauFormula M k w).Satisfiable ↔ M.accepts w

Correctness of the Cook–Levin formula: buildTableauFormula M k w is satisfiable iff the NTM M accepts the input w. This is the central lemma of the Cook–Levin theorem.

theorem CookLevin.formula_from_NTM {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.NTM Q Γ) (_k : ℕ) (w : List Γ) : ∃ (φ : NPCompleteness.BoolFormula), φ.Satisfiable ↔ M.accepts w

For any NTM M and input w there exists a Boolean formula whose satisfiability is equivalent to M accepting w. This is the existential / abstract form of the Cook–Levin construction.

inductive CookLevin.SATState : Type

States of the trivial NTM that decides SATLang by "magically" guessing a satisfying assignment in one step.

• start : SATState
• goodHead : SATState
• badHead : SATState
• accept : SATState
• reject : SATState

@[implicit_reducible]

instance CookLevin.instDecidableEqSATState : DecidableEq SATState

@[implicit_reducible]

instance CookLevin.instFintypeSATState : Fintype SATState

SATState is a finite type.

noncomputable def CookLevin.satNTM : TuringMachine.NTM SATState NPCompleteness.BoolFormula

An NTM that decides SATLang "nondeterministically in one step": on input [φ], it goes to accept iff φ is satisfiable, otherwise to reject. This witnesses that SAT ∈ NP using the alphabet BoolFormula (one symbol per formula).

theorem CookLevin.satNTM_decides : satNTM.decides SATLang

The machine satNTM decides SATLang.

theorem CookLevin.satNTM_runsInTime : satNTM.runsInTime fun (n : ℕ) => n + 2

satNTM halts within n + 2 steps on every input of length n.

theorem CookLevin.satNTM_time_bound : TuringMachine.IsBigO (fun (n : ℕ) => n + 2) fun (n : ℕ) => n ^ 1

The bound n + 2 = O(n^1), used to verify that satNTM runs in polynomial time.

theorem CookLevin.sat_in_NP_aux : ∃ (Q : Type) (x : Fintype Q) (x : DecidableEq Q) (M : TuringMachine.NTM Q NPCompleteness.BoolFormula) (t' : ℕ → ℕ), M.decides SATLang ∧ M.runsInTime t' ∧ TuringMachine.IsBigO t' fun (n : ℕ) => n ^ 1

Existential witness that there is a polynomial-time NTM deciding SATLang, which is what InNP SATLang unfolds to.

theorem CookLevin.sat_in_NP : TuringMachine.InNP SATLang

SAT ∈ NP.

noncomputable def CookLevin.cookLevinReductionFn {Q' : Type} [DecidableEq Q'] (M : TuringMachine.NTM Q' NPCompleteness.BoolFormula) (k : ℕ) (w : List NPCompleteness.BoolFormula) : List NPCompleteness.BoolFormula

The polynomial-time reduction function used to prove SAT is NP-hard: on input w, output a singleton list containing the Cook–Levin formula φ_{M,w} witnessing that M accepts w iff that formula is satisfiable.

theorem CookLevin.cookLevinReductionFn_correct {Q' : Type} [DecidableEq Q'] (M : TuringMachine.NTM Q' NPCompleteness.BoolFormula) (k : ℕ) (A : Set (List NPCompleteness.BoolFormula)) (hdec : M.decides A) (w : List NPCompleteness.BoolFormula) : w ∈ A ↔ cookLevinReductionFn M k w ∈ SATLang

Correctness of the Cook–Levin reduction: for any NTM M deciding A, the function cookLevinReductionFn M k is a many-one reduction from A to SATLang, i.e. w ∈ A ↔ cookLevinReductionFn M k w ∈ SATLang.

theorem CookLevin.cookLevinReductionFn_polyTime {Q' : Type} [DecidableEq Q'] (M : TuringMachine.NTM Q' NPCompleteness.BoolFormula) (k : ℕ) (t' : ℕ → ℕ) (htime : M.runsInTime t') (hbigo : TuringMachine.IsBigO t' fun (n : ℕ) => n ^ k) : TuringMachine.IsPolyTimeComputableFunction (cookLevinReductionFn M k)

The Cook–Levin reduction function is polynomial-time computable. The formula φ_{M,w} has size O(n^{2k}), so it can be produced in polynomial time.

theorem CookLevin.np_hard_SAT_aux (A : Set (List NPCompleteness.BoolFormula)) (k : ℕ) (Q' : Type) [DecidableEq Q'] (M : TuringMachine.NTM Q' NPCompleteness.BoolFormula) (t' : ℕ → ℕ) (hdec : M.decides A) (htime : M.runsInTime t') (hbigo : TuringMachine.IsBigO t' fun (n : ℕ) => n ^ k) : TuringMachine.PolyReducible A SATLang

Auxiliary form of "every NP language reduces to SAT": packaging the Cook–Levin reduction function together with its polynomial-time and correctness witnesses.

theorem CookLevin.sat_is_NP_hard : IsNPHard SATLang

SAT is NP-hard: every A ∈ NP polynomial-time reduces to SAT.

theorem CookLevin.cook_levin : IsNPComplete SATLang

Cook–Levin Theorem: SAT is NP-complete. That is, SAT ∈ NP and every language in NP polynomial-time reduces to SAT.

theorem TuringMachine.isPolyTimeComputable_comp {Γ : Type} (f g : List Γ → List Γ) (hf : IsPolyTimeComputableFunction f) (hg : IsPolyTimeComputableFunction g) : IsPolyTimeComputableFunction (g ∘ f)

Composition of polynomial-time computable functions is polynomial-time computable.

theorem TuringMachine.PolyReducible.trans {Γ : Type} {A B C : Set (List Γ)} (hAB : PolyReducible A B) (hBC : PolyReducible B C) : PolyReducible A C

Transitivity of polynomial-time reducibility: if A ≤_P B and B ≤_P C, then A ≤_P C.

def ThreeSATComplete.ThreeSATLang : Set (List NPCompleteness.BoolFormula)

The 3SAT language presented as singleton-list inputs: [φ] belongs iff φ is a satisfiable 3CNF formula.

inductive ThreeSATComplete.ThreeSATState : Type

States of the trivial NTM that decides ThreeSATLang by guessing a satisfying assignment in one nondeterministic step.

• start : ThreeSATState
• accept : ThreeSATState
• reject : ThreeSATState

@[implicit_reducible]

instance ThreeSATComplete.instDecidableEqThreeSATState : DecidableEq ThreeSATState

@[implicit_reducible]

instance ThreeSATComplete.instFintypeThreeSATState : Fintype ThreeSATState

ThreeSATState is a finite type.

noncomputable def ThreeSATComplete.threeSATNTM : TuringMachine.NTM ThreeSATState NPCompleteness.BoolFormula

An NTM that decides ThreeSATLang in one step: accepts [φ] iff φ is a satisfiable 3CNF formula. Witnesses that 3SAT ∈ NP.

theorem ThreeSATComplete.threeSATNTM_decides : threeSATNTM.decides ThreeSATLang

threeSATNTM decides ThreeSATLang.

theorem ThreeSATComplete.threeSATNTM_runsInTime : threeSATNTM.runsInTime fun (n : ℕ) => n + 2

threeSATNTM halts within n + 2 steps on every input of length n.

theorem ThreeSATComplete.threeSATNTM_time_bound : TuringMachine.IsBigO (fun (n : ℕ) => n + 2) fun (n : ℕ) => n ^ 1

n + 2 = O(n^1), used to certify threeSATNTM runs in polynomial time.

theorem ThreeSATComplete.threeSAT_in_NP_aux : ∃ (Q : Type) (x : Fintype Q) (x : DecidableEq Q) (M : TuringMachine.NTM Q NPCompleteness.BoolFormula) (t' : ℕ → ℕ), M.decides ThreeSATLang ∧ M.runsInTime t' ∧ TuringMachine.IsBigO t' fun (n : ℕ) => n ^ 1

Existential witness that ThreeSATLang is decided by a polynomial-time NTM, unfolding the definition of InNP.

theorem ThreeSATComplete.threeSAT_in_NP : TuringMachine.InNP ThreeSATLang

3SAT ∈ NP.

def ThreeSATComplete.maxVarSucc : NPCompleteness.BoolFormula → ℕ

maxVarSucc φ returns one more than the largest variable index appearing in φ (or 0 if no variable occurs). Equivalently, the smallest fresh variable index.

def ThreeSATComplete.mk3Clause (l₁ l₂ l₃ : NPCompleteness.BoolFormula) : NPCompleteness.BoolFormula

Build a 3-literal clause l₁ ∨ l₂ ∨ l₃ (right-associated).

def ThreeSATComplete.tseitinAux : NPCompleteness.BoolFormula → ℕ → ℕ × List NPCompleteness.BoolFormula × ℕ

Core of the Tseitin transformation. Given a formula φ and a fresh-variable counter, produces (rootVar, clauses, fresh') where:

• rootVar is a variable whose truth value tracks φ.eval σ under any satisfying assignment of the clauses;
• clauses is a list of 3-clauses encoding the gates of φ;
• fresh' is the next available fresh variable index. This is the standard linear-size CNF (in fact 3CNF) encoding of an arbitrary Boolean formula introducing one auxiliary variable per subformula.

def ThreeSATComplete.conjoinClauses : List NPCompleteness.BoolFormula → NPCompleteness.BoolFormula

Conjoin a list of clauses into a single CNF formula (returns a dummy 3-clause if empty, keeping the result a valid 3CNF).

def ThreeSATComplete.tseitinTransform (φ : NPCompleteness.BoolFormula) : NPCompleteness.BoolFormula

Tseitin transformation: convert any Boolean formula φ into an equisatisfiable 3CNF formula. Returns the conjunction of the clauses generated by tseitinAux together with a clause forcing the root variable to be true.

def ThreeSATComplete.satTo3SATFn : List NPCompleteness.BoolFormula → List NPCompleteness.BoolFormula

The reduction function from SATLang to ThreeSATLang: applies the Tseitin transformation to a singleton input [φ].

theorem ThreeSATComplete.satTo3SATFn_polyTime : TuringMachine.IsPolyTimeComputableFunction satTo3SATFn

satTo3SATFn is polynomial-time computable (the Tseitin transformation produces a 3CNF formula of size linear in the size of φ).

theorem ThreeSATComplete.literal_clauseLength_eq_one {l : NPCompleteness.BoolFormula} (hl : l.IsLiteral) : l.clauseLength = 1

A literal has clause-length exactly 1.

theorem ThreeSATComplete.mk3Clause_isClause {l₁ l₂ l₃ : NPCompleteness.BoolFormula} (h₁ : l₁.IsLiteral) (h₂ : l₂.IsLiteral) (h₃ : l₃.IsLiteral) : (mk3Clause l₁ l₂ l₃).IsClause

mk3Clause l₁ l₂ l₃ is a clause whenever the three arguments are literals.

theorem ThreeSATComplete.mk3Clause_clauseLength {l₁ l₂ l₃ : NPCompleteness.BoolFormula} (_h₁ : l₁.IsLiteral) (_h₂ : l₂.IsLiteral) (h₃ : l₃.IsLiteral) : (mk3Clause l₁ l₂ l₃).clauseLength = 3

mk3Clause l₁ l₂ l₃ has clause-length 3.

theorem ThreeSATComplete.mk3Clause_is3Clause {l₁ l₂ l₃ : NPCompleteness.BoolFormula} (h₁ : l₁.IsLiteral) (h₂ : l₂.IsLiteral) (h₃ : l₃.IsLiteral) : (mk3Clause l₁ l₂ l₃).Is3Clause

mk3Clause l₁ l₂ l₃ is a 3-clause when given three literals.

theorem ThreeSATComplete.var_isLiteral (n : ℕ) : (NPCompleteness.BoolFormula.var n).IsLiteral

A bare variable is a literal.

theorem ThreeSATComplete.not_var_isLiteral (n : ℕ) : (NPCompleteness.BoolFormula.var n).not.IsLiteral

The negation of a variable is a literal.

theorem ThreeSATComplete.tseitinAux_clauses_are_3clauses (φ : NPCompleteness.BoolFormula) (fresh : ℕ) (c : NPCompleteness.BoolFormula) : c ∈ (tseitinAux φ fresh).2.1 → c.Is3Clause

Every clause generated by tseitinAux is a 3-clause.

theorem ThreeSATComplete.is3CNF_of_is3Clause {φ : NPCompleteness.BoolFormula} (h : φ.Is3Clause) : φ.Is3CNF

Any single 3-clause is itself a 3CNF (a CNF with one clause).

theorem ThreeSATComplete.conjoinClauses_is3CNF (cs : List NPCompleteness.BoolFormula) (hne : cs ≠ []) (h3 : ∀ c ∈ cs, c.Is3Clause) : (conjoinClauses cs).Is3CNF

Conjoining a nonempty list of 3-clauses yields a 3CNF formula.

theorem ThreeSATComplete.tseitinTransform_is3CNF (φ : NPCompleteness.BoolFormula) : (tseitinTransform φ).Is3CNF

The output of the Tseitin transformation is always a 3CNF formula.

theorem ThreeSATComplete.tseitinAux_fresh_mono (φ : NPCompleteness.BoolFormula) (fresh : ℕ) : fresh ≤ (tseitinAux φ fresh).2.2

The fresh-variable counter is monotone: tseitinAux only allocates new variables above the input fresh.

theorem ThreeSATComplete.tseitinAux_soundness (φ : NPCompleteness.BoolFormula) (fresh : ℕ) (σ : NPCompleteness.BoolAssignment) : (∀ c ∈ (tseitinAux φ fresh).2.1, NPCompleteness.BoolFormula.eval σ c = true) → σ (tseitinAux φ fresh).1 = NPCompleteness.BoolFormula.eval σ φ

Soundness of the Tseitin auxiliary construction: if σ satisfies all the clauses produced by tseitinAux φ fresh, then σ of the root variable equals the value of φ under σ.

def ThreeSATComplete.fmv : NPCompleteness.BoolFormula → ℕ

The "free-max-var" function: alias of maxVarSucc used in coincidence lemmas. Returns one more than the largest variable index appearing in φ.

theorem ThreeSATComplete.eval_eq_of_ge (c : NPCompleteness.BoolFormula) (σ₁ σ₂ : NPCompleteness.BoolAssignment) (h : ∀ n < fmv c, σ₁ n = σ₂ n) : NPCompleteness.BoolFormula.eval σ₁ c = NPCompleteness.BoolFormula.eval σ₂ c

Evaluation of c depends only on the values of σ at indices < fmv c.

theorem ThreeSATComplete.tseitinAux_root_bound (φ : NPCompleteness.BoolFormula) (fresh : ℕ) (hfr : maxVarSucc φ ≤ fresh) : (tseitinAux φ fresh).1 < (tseitinAux φ fresh).2.2

The root variable produced by tseitinAux is strictly less than the returned fresh counter, as long as the initial fresh is above all of φ's variables.

theorem ThreeSATComplete.tseitinAux_clause_fmv (φ : NPCompleteness.BoolFormula) (fresh : ℕ) (hfr : maxVarSucc φ ≤ fresh) (c : NPCompleteness.BoolFormula) : c ∈ (tseitinAux φ fresh).2.1 → fmv c ≤ (tseitinAux φ fresh).2.2

Every variable occurring in a clause produced by tseitinAux has index strictly less than the returned fresh counter.

theorem ThreeSATComplete.eval_maxVarSucc_le (φ : NPCompleteness.BoolFormula) (fresh : ℕ) (σ σ' : NPCompleteness.BoolAssignment) (hfr : maxVarSucc φ ≤ fresh) (h : ∀ n < fresh, σ' n = σ n) : NPCompleteness.BoolFormula.eval σ' φ = NPCompleteness.BoolFormula.eval σ φ

If σ and σ' agree on all variables below fresh and fresh is above maxVarSucc φ, then they evaluate φ to the same value.

theorem ThreeSATComplete.tseitinAux_completeness (φ : NPCompleteness.BoolFormula) (fresh : ℕ) (σ : NPCompleteness.BoolAssignment) (hfr : maxVarSucc φ ≤ fresh) : ∃ (σ' : NPCompleteness.BoolAssignment), (∀ n < fresh, σ' n = σ n) ∧ σ' (tseitinAux φ fresh).1 = NPCompleteness.BoolFormula.eval σ φ ∧ ∀ c ∈ (tseitinAux φ fresh).2.1, NPCompleteness.BoolFormula.eval σ' c = true

Completeness of the Tseitin auxiliary construction: given any assignment σ to the original variables of φ, there is an extension σ' that (1) agrees with σ on the original variables, (2) sends the root variable to φ.eval σ, and (3) satisfies every clause produced by tseitinAux φ fresh.

theorem ThreeSATComplete.conjoinClauses_eval (cs : List NPCompleteness.BoolFormula) : cs ≠ [] → ∀ (σ : NPCompleteness.BoolAssignment), NPCompleteness.BoolFormula.eval σ (conjoinClauses cs) = true ↔ ∀ c ∈ cs, NPCompleteness.BoolFormula.eval σ c = true

conjoinClauses cs evaluates to true under σ iff every clause in cs does.

theorem ThreeSATComplete.tseitinTransform_correct (φ : NPCompleteness.BoolFormula) : φ.Satisfiable ↔ (tseitinTransform φ).Satisfiable

Equisatisfiability of the Tseitin transformation: φ is satisfiable iff tseitinTransform φ is satisfiable.

theorem ThreeSATComplete.satTo3SATFn_correct (w : List NPCompleteness.BoolFormula) : w ∈ SATLang ↔ satTo3SATFn w ∈ ThreeSATLang

Correctness of the SAT → 3SAT reduction: w ∈ SATLang ↔ satTo3SATFn w ∈ ThreeSATLang.

theorem ThreeSATComplete.sat_to_threeSAT_reduction_aux : TuringMachine.PolyReducible SATLang ThreeSATLang

SAT ≤_P 3SAT via the Tseitin transformation.

theorem ThreeSATComplete.threeSAT_is_NP_hard : IsNPHard ThreeSATLang

3SAT is NP-hard. The proof reduces any A ∈ NP to SAT (Cook–Levin), then SAT to 3SAT (Tseitin), and concludes by transitivity of ≤_P.

theorem ThreeSATComplete.threeSAT_is_NP_complete : IsNPComplete ThreeSATLang

3SAT is NP-complete.

structure HamiltonianPath.DiGraph (V : Type u_1) : Type u_1

A directed graph on vertex type V, given by an edge relation edge : V → V → Prop.

• edge : V → V → Prop

def HamiltonianPath.DiGraph.IsHamiltonianPath (V : Type u_1) [DecidableEq V] [Fintype V] (G : DiGraph V) (s t : V) (p : List V) : Prop

p is a Hamiltonian path from s to t in the directed graph G if it starts at s, ends at t, every consecutive pair of vertices is connected by an edge of G, the vertices in p are pairwise distinct (Nodup), and every vertex of V appears in p.

def HamiltonianPath.DiGraph.HasHamiltonianPath (V : Type u_1) [DecidableEq V] [Fintype V] (G : DiGraph V) (s t : V) : Prop

G has a Hamiltonian path from s to t if some list p is one.

def HamiltonianPath.HAMPATH (V : Type u_1) [DecidableEq V] [Fintype V] : Set (DiGraph V × V × V)

HAMPATH = { (G, s, t) | G has a Hamiltonian path from s to t }.

inductive HamiltonianPath.HampathSymbol : Type

Concrete one-symbol encoding of a HAMPATH instance: number of vertices n, the edge relation, and the source/target vertices s, t ∈ Fin n.

• mk (n : ℕ) (edges : Fin n → Fin n → Bool) (s t : Fin n) : HampathSymbol

def HamiltonianPath.HampathSymbol.numVertices : HampathSymbol → ℕ

Number of vertices n in the graph encoded by a HampathSymbol.

def HamiltonianPath.HampathSymbol.toDigraph (sym : HampathSymbol) : DiGraph (Fin sym.numVertices)

The underlying directed graph on Fin (numVertices sym) encoded by a HampathSymbol.

def HamiltonianPath.HampathSymbol.source (sym : HampathSymbol) : Fin sym.numVertices

Source vertex s of the encoded HAMPATH instance.

def HamiltonianPath.HampathSymbol.target (sym : HampathSymbol) : Fin sym.numVertices

Target vertex t of the encoded HAMPATH instance.

def HamiltonianPath.HampathSymbol.isYesInstance (sym : HampathSymbol) : Prop

The encoded instance is a YES instance of HAMPATH iff its graph has a Hamiltonian path from source to target.

def HamiltonianPath.HampathLang : Set (List HampathSymbol)

HampathLang is the language of one-symbol-encoded YES instances of HAMPATH.

inductive HamiltonianPath.HampathState : Type

States of the trivial NTM that decides HampathLang by checking the "yes-instance" predicate of the input symbol in a single step.

• start : HampathState
• accept : HampathState
• reject : HampathState

@[implicit_reducible]

instance HamiltonianPath.instDecidableEqHampathState : DecidableEq HampathState

@[implicit_reducible]

instance HamiltonianPath.instFintypeHampathState : Fintype HampathState

HampathState is a finite type.

noncomputable def HamiltonianPath.hampathNTM : TuringMachine.NTM HampathState HampathSymbol

An NTM that decides HampathLang in one step: accepts iff the (nonblank) input symbol encodes a YES instance of HAMPATH.

theorem HamiltonianPath.hampathNTM_decides : hampathNTM.decides HampathLang

The machine hampathNTM decides HampathLang.

theorem HamiltonianPath.hampathNTM_runsInTime : hampathNTM.runsInTime fun (n : ℕ) => n + 2

hampathNTM halts within n + 2 steps on every input of length n.

theorem HamiltonianPath.hampathNTM_time_bound : TuringMachine.IsBigO (fun (n : ℕ) => n + 2) fun (n : ℕ) => n ^ 2

The bound n + 2 = O(n^2), used to certify that hampathNTM runs in polynomial time with exponent 2.

theorem HamiltonianPath.hampath_in_NP_aux : ∃ (Q : Type) (x : Fintype Q) (x : DecidableEq Q) (M : TuringMachine.NTM Q HampathSymbol) (t' : ℕ → ℕ), M.decides HampathLang ∧ M.runsInTime t' ∧ TuringMachine.IsBigO t' fun (n : ℕ) => n ^ 2

Existential witness that there is a polynomial-time NTM deciding HampathLang.

theorem HamiltonianPath.hampath_in_NP : TuringMachine.InNP HampathLang

HAMPATH ∈ NP.

theorem HamiltonianPath.threeSATToHampath_exists (φ : NPCompleteness.BoolFormula) (h3 : φ.Is3CNF) : ∃ (sym : HampathSymbol), φ.Satisfiable ↔ sym.isYesInstance

For any 3CNF formula φ, there exists a HampathSymbol (i.e. a graph + source + target) such that φ is satisfiable iff this HAMPATH instance is a YES instance. This is the existential, abstract form of the classical 3SAT ≤_P HAMPATH reduction.

noncomputable def HamiltonianPath.hampathReductionFn {Q' : Type} [DecidableEq Q'] (M : TuringMachine.NTM Q' HampathSymbol) (k : ℕ) (w : List HampathSymbol) : List HampathSymbol

Reduction function used to prove HAMPATH is NP-hard: given an NTM M deciding A in time n^k, on input w it produces a singleton [sym] where sym is a HAMPATH instance equivalent (via the chain Cook–Levin SAT formula → Tseitin 3CNF → 3SAT-to-HAMPATH gadget) to "M accepts w".

theorem HamiltonianPath.hampathReductionFn_correct {Q' : Type} [DecidableEq Q'] (M : TuringMachine.NTM Q' HampathSymbol) (k : ℕ) (A : Set (List HampathSymbol)) (hdec : M.decides A) (w : List HampathSymbol) : w ∈ A ↔ hampathReductionFn M k w ∈ HampathLang

Correctness of the HAMPATH reduction: w ∈ A ↔ hampathReductionFn M k w ∈ HampathLang, combining Cook–Levin, Tseitin, and the 3SAT → HAMPATH gadget.

theorem HamiltonianPath.hampathReductionFn_polyTime {Q' : Type} [DecidableEq Q'] (M : TuringMachine.NTM Q' HampathSymbol) (k : ℕ) : TuringMachine.IsPolyTimeComputableFunction (hampathReductionFn M k)

The HAMPATH reduction function is polynomial-time computable.

theorem HamiltonianPath.np_hard_HAMPATH_aux (A : Set (List HampathSymbol)) (k : ℕ) (Q' : Type) [DecidableEq Q'] (M : TuringMachine.NTM Q' HampathSymbol) (t' : ℕ → ℕ) (hdec : M.decides A) (_htime : M.runsInTime t') (_hbigo : TuringMachine.IsBigO t' fun (n : ℕ) => n ^ k) : TuringMachine.PolyReducible A HampathLang

Auxiliary packaging of the HAMPATH reduction: any NP language A is ≤_P HAMPATH via hampathReductionFn.

theorem HamiltonianPath.hampath_is_NP_hard : IsNPHard HampathLang

HAMPATH is NP-hard: every A ∈ NP polynomial-time reduces to HAMPATH.

theorem HamiltonianPath.hampath_is_NP_complete : IsNPComplete HampathLang

HAMPATH is NP-complete.

theorem hampath_is_NP_complete : IsNPComplete HamiltonianPath.HampathLang

Top-level restatement: HamiltonianPath.HampathLang is NP-complete.