Encoding-size support for Tseitin splitting

These internal lemmas relate syntactic clause/literal counts to the existing unary-variable SAT bit encoding and bound exact-3 formulas whose variable indices share a common upper bound.

theorem Complexity.SAT.Clause.length_le_encode_length_internal (c : Clause) : List.length c ≤ c.encode.length

A clause has no more literal occurrences than bits in its encoding.

theorem Complexity.SAT.CNF.length_le_encode_length_internal (φ : CNF) : List.length φ ≤ φ.encode.length

A CNF has no more clauses than bits in its encoding.

theorem Complexity.SAT.CNF.literalCount_le_encode_length_internal (φ : CNF) : φ.literalCount ≤ φ.encode.length

The total number of literal occurrences is bounded by encoded length.

theorem Complexity.SAT.Clause.encode_length_le_of_length_eq_three_internal {c : Clause} {B : ℕ} (hlen : List.length c = 3) (hvar : ∀ ℓ ∈ c, ℓ.var ≤ B) : c.encode.length ≤ 6 * B + 12

A three-literal clause whose variables are at most B uses at most 6 * B + 12 bits in the unary-variable encoding.

theorem Complexity.SAT.CNF.encode_length_le_of_is3CNF_internal {φ : CNF} {B : ℕ} (h3 : φ.Is3CNF) (hvar : ∀ c ∈ φ, ∀ ℓ ∈ c, ℓ.var ≤ B) : φ.encode.length ≤ List.length φ * (6 * B + 14)

An exact-3 CNF with M clauses and variables at most B has encoded length at most M * (6 * B + 14), including clause separators.