Structural properties of Tseitin clause splitting

This internal module proves that the fresh-variable-threaded splitter produces exact-width-three clauses, accounts exactly for its fresh counter, keeps every generated variable below the first unused counter, and has linear structural size in the source literal and clause counts.

theorem Complexity.SAT.CNF.is3CNF_append_internal {φ ψ : CNF} (hφ : φ.Is3CNF) (hψ : ψ.Is3CNF) : (φ ++ ψ).Is3CNF

Exact-width-three shape is preserved by concatenating formulas.

theorem Complexity.SAT.Clause.tseitinFreshCount_eq_length_sub_three_internal {c : Clause} (hc : c ≠ []) : c.tseitinFreshCount = List.length c - 3

On a nonempty clause, the fresh count is exactly length - 3.

theorem Complexity.SAT.Clause.tseitinFreshCount_wide_internal (next : ℕ) (a b c d : Lit) (rest : List Lit) : tseitinFreshCount (a :: b :: c :: d :: rest) = tseitinFreshCount (Lit.negVar next :: c :: d :: rest) + 1

One wide-clause split consumes one variable and leaves the remaining count to the recursive suffix.

theorem Complexity.SAT.Clause.tseitinFreshCount_le_length_add_one_internal (c : Clause) : c.tseitinFreshCount ≤ List.length c + 1

A clause never consumes more than one plus its number of literals.

theorem Complexity.SAT.Clause.to3CNF_is3CNF_internal (next : ℕ) (c : Clause) : (to3CNF next c).Is3CNF

Every clause emitted by the single-clause splitter has exactly three literals.

theorem Complexity.SAT.Clause.length_to3CNF_internal (next : ℕ) (c : Clause) : List.length (to3CNF next c) = c.tseitinFreshCount + 1

The splitter emits exactly one more clause than the number of fresh variables that it consumes.

theorem Complexity.SAT.Clause.length_to3CNF_le_internal (next : ℕ) (c : Clause) : List.length (to3CNF next c) ≤ List.length c + 2

Coarse clause-count bound for one split clause.

theorem Complexity.SAT.Clause.var_lt_of_mem_to3CNF_internal (next : ℕ) (c : Clause) : (∀ ℓ ∈ c, ℓ.var < next) → ∀ {out : Clause}, out ∈ to3CNF next c → ∀ {ℓ : Lit}, ℓ ∈ out → ℓ.var < next + c.tseitinFreshCount

Assuming all source variables precede next, every literal emitted for one clause precedes the returned fresh counter.

theorem Complexity.SAT.CNF.to3Aux_is3CNF_internal (next : ℕ) (φ : CNF) : (to3Aux next φ).1.Is3CNF

Splitting every clause preserves exact-width-three shape.

theorem Complexity.SAT.CNF.to3_is3CNF_internal (φ : CNF) : φ.to3.Is3CNF

The top-level transformation produces exact 3-CNF.

theorem Complexity.SAT.CNF.to3Aux_counter_internal (next : ℕ) (φ : CNF) : (to3Aux next φ).2 = next + φ.tseitinFreshCount

to3Aux returns exactly the first counter after all fresh variables.

theorem Complexity.SAT.CNF.tseitinFreshCount_le_literalCount_add_length_internal (φ : CNF) : φ.tseitinFreshCount ≤ φ.literalCount + List.length φ

Total fresh-variable use is bounded by source literals plus source clauses.

theorem Complexity.SAT.CNF.length_to3Aux_internal (next : ℕ) (φ : CNF) : List.length (to3Aux next φ).1 = φ.tseitinFreshCount + List.length φ

The output clause count is exactly fresh variables plus source clauses.

theorem Complexity.SAT.CNF.length_to3Aux_le_internal (next : ℕ) (φ : CNF) : List.length (to3Aux next φ).1 ≤ φ.literalCount + 2 * List.length φ

Coarse output clause-count bound in source literals and clauses.

theorem Complexity.SAT.CNF.literalCount_eq_three_mul_length_of_is3CNF_internal {φ : CNF} (hφ : φ.Is3CNF) : φ.literalCount = 3 * List.length φ

Exact 3-CNF has three literal occurrences per clause.

theorem Complexity.SAT.CNF.literalCount_to3Aux_internal (next : ℕ) (φ : CNF) : (to3Aux next φ).1.literalCount = 3 * (φ.tseitinFreshCount + List.length φ)

Exact literal count of the transformed formula.

theorem Complexity.SAT.CNF.literalCount_to3Aux_le_internal (next : ℕ) (φ : CNF) : (to3Aux next φ).1.literalCount ≤ 3 * (φ.literalCount + 2 * List.length φ)

Coarse transformed literal-count bound used by the later encoded-size proof.

theorem Complexity.SAT.CNF.var_lt_of_mem_to3Aux_internal (next : ℕ) (φ : CNF) (hsource : ∀ c ∈ φ, ∀ ℓ ∈ c, ℓ.var < next) {out : Clause} (hout : out ∈ (to3Aux next φ).1) {ℓ : Lit} (hℓ : ℓ ∈ out) : ℓ.var < next + φ.tseitinFreshCount

Assuming source variables precede next, every transformed literal precedes the returned fresh counter.

theorem Complexity.SAT.CNF.var_lt_of_mem_to3_internal (φ : CNF) {out : Clause} (hout : out ∈ φ.to3) {ℓ : Lit} (hℓ : ℓ ∈ out) : ℓ.var < φ.maxVar + 1 + φ.tseitinFreshCount

Every literal produced by to3 lies below its final fresh counter.