Sundogcert/SATNPHard.lean — MILESTONE 1 of the 3SAT ≤ 3DM marathon.

WHAT THIS FILE PROVIDES (the FOUNDATION — definitions + concrete validation, no reduction yet): * Literal n — a variable index Fin n plus a sign (true = xᵢ, false = ¬xᵢ). * Assignment n — a Boolean assignment Fin n → Bool. * evalLiteral — evaluate one literal under an assignment. * Clause n — an ORDERED triple of literals (Fin 3 → Literal n; cleaner than a Finset for the downstream gadget's variable-wheel / clause indexing). * clauseSat — a clause is satisfied iff at least one of its 3 literals is true. * Formula n m — a 3-CNF formula: m indexed clauses. * formulaSat — every clause holds. * Satisfiable — 3-SAT: some assignment satisfies the formula.

Decidability of clauseSat/formulaSat/Satisfiable on concrete instances is AUTOMATIC: the ∃/∀ range over Fin _ and Assignment n = Fin n → Bool (Fintypes with DecidableEq), and evalLiteral … = true is decidable. This lets decide kernel-reduce the two concrete examples below — AXIOM-CLEAN (no Lean.ofReduceBool; we use decide, never native_decide).

CONCRETE VALIDATION (locks the encoding): * ex_sat — Satisfiable fSat for fSat (n=2, m=1, clause x₀ ∨ x₁ ∨ x₀). * ex_unsat — ¬ Satisfiable fUnsat for fUnsat (n=1, m=2, clauses x₀∨x₀∨x₀, ¬x₀∨¬x₀∨¬x₀).

THE IMPORTED WALL (named, NOT proved — mathlib has no complexity framework): * the NP complexity class itself, and poly-time-ness of any reduction; * 3SAT's OWN NP-hardness — Cook–Levin, the DEEP TERMINAL WALL, a multi-year formalization, named forever as the ultimate source of every Karp-reduction hardness claim in this chain. STANDING LIMIT: this file defines the 3SAT problem and validates the encoding. The gadget reduction (variable wheel, clause gadget, garbage) landing on Sundog.MatchingNPHard.ThreeDM, and its correctness, is the work to come — milestones 2+ of 3SAT ≤ 3DM ≤ X3C ≤ Decodes.

@[reducible, inline]

abbrev Sundog.SATNPHard.Literal (n : ℕ) : Type

A literal: a variable index plus a sign (true = positive xᵢ, false = negated).

Equations

• Sundog.SATNPHard.Literal n = (Fin n × Bool)

@[reducible, inline]

abbrev Sundog.SATNPHard.Assignment (n : ℕ) : Type

A Boolean assignment.

Equations

• Sundog.SATNPHard.Assignment n = (Fin n → Bool)

def Sundog.SATNPHard.evalLiteral {n : ℕ} (a : Assignment n) (l : Literal n) : Bool

Evaluate a literal under an assignment.

Equations

• Sundog.SATNPHard.evalLiteral a l = if l.2 = true then a l.1 else !a l.1

@[reducible, inline]

abbrev Sundog.SATNPHard.Clause (n : ℕ) : Type

A 3-clause: an ORDERED triple of literals (Fin 3 → Literal — cleaner than a Finset for the downstream gadget's indexing).

Equations

• Sundog.SATNPHard.Clause n = (Fin 3 → Sundog.SATNPHard.Literal n)

def Sundog.SATNPHard.clauseSat {n : ℕ} (a : Assignment n) (c : Clause n) : Prop

A clause is satisfied iff at least one of its 3 literals is true.

Equations

• Sundog.SATNPHard.clauseSat a c = ∃ (k : Fin 3), Sundog.SATNPHard.evalLiteral a (c k) = true

@[reducible, inline]

abbrev Sundog.SATNPHard.Formula (n m : ℕ) : Type

A 3-CNF formula: m clauses, indexed.

Equations

• Sundog.SATNPHard.Formula n m = (Fin m → Sundog.SATNPHard.Clause n)

def Sundog.SATNPHard.formulaSat {n m : ℕ} (a : Assignment n) (f : Formula n m) : Prop

A formula is satisfied iff every clause is.

Equations

• Sundog.SATNPHard.formulaSat a f = ∀ (k : Fin m), Sundog.SATNPHard.clauseSat a (f k)

def Sundog.SATNPHard.Satisfiable {n m : ℕ} (f : Formula n m) : Prop

3-SAT: a formula is satisfiable iff some assignment satisfies it.

Equations

• Sundog.SATNPHard.Satisfiable f = ∃ (a : Sundog.SATNPHard.Assignment n), Sundog.SATNPHard.formulaSat a f

Decidability.

`evalLiteral … = true` is decidable (`DecidableEq Bool`); the bounded `∃`/`∀` over `Fin _`
and `Assignment n = Fin n → Bool` (a Fintype) then make `clauseSat`/`formulaSat`/`Satisfiable`
decidable via `Fintype.decidableExistsFintype` / `Fintype.decidableForallFintype`.  These
instances let `decide` kernel-reduce the concrete examples below — no `native_decide`. 

@[implicit_reducible]

instance Sundog.SATNPHard.instDecidableClauseSat {n : ℕ} (a : Assignment n) (c : Clause n) : Decidable (clauseSat a c)

Equations

• Sundog.SATNPHard.instDecidableClauseSat a c = Sundog.SATNPHard.instDecidableClauseSat._aux_1 a c

@[implicit_reducible]

instance Sundog.SATNPHard.instDecidableFormulaSat {n m : ℕ} (a : Assignment n) (f : Formula n m) : Decidable (formulaSat a f)

Equations

• Sundog.SATNPHard.instDecidableFormulaSat a f = Sundog.SATNPHard.instDecidableFormulaSat._aux_1 a f

@[implicit_reducible]

instance Sundog.SATNPHard.instDecidableSatisfiable {n m : ℕ} (f : Formula n m) : Decidable (Satisfiable f)

Equations

• Sundog.SATNPHard.instDecidableSatisfiable f = Sundog.SATNPHard.instDecidableSatisfiable._aux_1 f

Concrete validation (A): a SATISFIABLE formula.

`n = 2, m = 1`; the single clause is `x₀ ∨ x₁ ∨ x₀`, i.e. literals
`(0, true), (1, true), (0, true)`.  Satisfiable: take `a = ![true, true]` (or any `a` with
`a 0 = true`).  `∃` ranges over the 4 assignments of `Fin 2 → Bool` — decidable. 

def Sundog.SATNPHard.cSat : Clause 2

The single satisfiable clause x₀ ∨ x₁ ∨ x₀.

Equations

• Sundog.SATNPHard.cSat = ![(0, true), (1, true), (0, true)]

def Sundog.SATNPHard.fSat : Formula 2 1

The satisfiable formula with one clause.

Equations

• Sundog.SATNPHard.fSat = ![Sundog.SATNPHard.cSat]

theorem Sundog.SATNPHard.ex_sat : Satisfiable fSat

Concrete validation (B): an UNSATISFIABLE formula.

`n = 1, m = 2`; clauses `x₀ ∨ x₀ ∨ x₀` and `¬x₀ ∨ ¬x₀ ∨ ¬x₀`.  No assignment of the single
variable can satisfy both.  `¬∃` ranges over the 2 assignments of `Fin 1 → Bool` —
decidable. 

def Sundog.SATNPHard.cPos : Clause 1

The all-positive clause x₀ ∨ x₀ ∨ x₀.

Equations

• Sundog.SATNPHard.cPos = ![(0, true), (0, true), (0, true)]

def Sundog.SATNPHard.cNeg : Clause 1

The all-negative clause ¬x₀ ∨ ¬x₀ ∨ ¬x₀.

Equations

• Sundog.SATNPHard.cNeg = ![(0, false), (0, false), (0, false)]

def Sundog.SATNPHard.fUnsat : Formula 1 2

The unsatisfiable formula with the two contradictory clauses.

Equations

• Sundog.SATNPHard.fUnsat = ![Sundog.SATNPHard.cPos, Sundog.SATNPHard.cNeg]

theorem Sundog.SATNPHard.ex_unsat : ¬Satisfiable fUnsat

Axiom audit.

Expect `[propext, Classical.choice, Quot.sound]` (or a subset) — NO `sorryAx`, and NO
`Lean.ofReduceBool` (the latter would signal a `native_decide`, which we deliberately avoid).