Correctness of Tseitin clause splitting

The backward direction holds under every total assignment: the emitted chain logically implies its source clause. For the forward direction, fresh variables are chosen recursively while preserving all earlier variable values. The CNF proof threads those extensions across disjoint fresh ranges.

theorem Complexity.SAT.Clause.evalTotal_to3CNF_sound_internal (α : TotalAssignment) (next : ℕ) (c : Clause) (h : CNF.evalTotal α (to3CNF next c) = true) : evalTotal α c = true

Every assignment satisfying a split clause chain satisfies the original clause, independently of freshness.

theorem Complexity.SAT.Clause.exists_evalTotal_to3CNF_internal (next : ℕ) (c : Clause) (α : TotalAssignment) (hsource : ∀ ℓ ∈ c, ℓ.var < next) (h : evalTotal α c = true) : ∃ (β : TotalAssignment), (∀ v < next, β v = α v) ∧ CNF.evalTotal β (to3CNF next c) = true

If every source variable precedes next, a satisfying assignment for one source clause extends to a satisfying assignment for its exact-3 split while preserving every variable below next.

theorem Complexity.SAT.CNF.evalTotal_to3Aux_sound_internal (α : TotalAssignment) (next : ℕ) (φ : CNF) (h : evalTotal α (to3Aux next φ).1 = true) : evalTotal α φ = true

A satisfying assignment for a transformed CNF satisfies the source CNF.

theorem Complexity.SAT.CNF.exists_evalTotal_to3Aux_internal (next : ℕ) (φ : CNF) (α : TotalAssignment) (hsource : ∀ c ∈ φ, ∀ ℓ ∈ c, ℓ.var < next) (h : evalTotal α φ = true) : ∃ (β : TotalAssignment), (∀ v < next, β v = α v) ∧ evalTotal β (to3Aux next φ).1 = true

A satisfying assignment for a source CNF extends across all fresh ranges to satisfy the transformed CNF, preserving every variable below next.

theorem Complexity.SAT.CNF.functionSatisfiable_to3Aux_iff_internal (next : ℕ) (φ : CNF) (hsource : ∀ c ∈ φ, ∀ ℓ ∈ c, ℓ.var < next) : (to3Aux next φ).1.FunctionSatisfiable ↔ φ.FunctionSatisfiable

Function-valued satisfiability is preserved and reflected by to3Aux whenever its initial counter is fresh for every source variable.

theorem Complexity.SAT.CNF.satisfiable_to3Aux_iff_internal (next : ℕ) (φ : CNF) (hsource : ∀ c ∈ φ, ∀ ℓ ∈ c, ℓ.var < next) : (to3Aux next φ).1.Satisfiable ↔ φ.Satisfiable

Existing finite-list satisfiability is preserved and reflected by to3Aux whenever its initial counter is fresh for every source variable.

theorem Complexity.SAT.CNF.functionSatisfiable_to3_iff_internal (φ : CNF) : φ.to3.FunctionSatisfiable ↔ φ.FunctionSatisfiable

Function-valued satisfiability is preserved and reflected by to3.

theorem Complexity.SAT.CNF.satisfiable_to3_iff_internal (φ : CNF) : φ.to3.Satisfiable ↔ φ.Satisfiable

Existing finite-list satisfiability is preserved and reflected by to3.