Total size bounds for the finite occurrence splitter

The existing toThreeSATThree reduction accepts arbitrary binary-labelled CNF inputs. Its width-valid branch has one implication per literal occurrence; its rejecting branch is [[]]. Distinct variables are bounded by literal occurrences, independently of the original label sizes.

Main definitions

The existing total splitter, ordinary CNF variable count, and literal occurrences are reused.

Main results

• Cslib.Complexity.width_toThreeSATThree: every total output has width at most three.
• Cslib.Complexity.count_vars_toThreeSATThree_le: every output variable occurs at most thrice.
• Cslib.Complexity.size_toThreeSATThree_le: the total incidence size is at most seven times the original clause and literal-occurrence size, including the unit offset.

References

These are quantitative consequences of the finite splitter adapted from lean-trominoes revision 6d5b36c15cec6cb18d30137b7f1c7fb92ea24332. The imported construction records the source credit. The linear bound using occurrence counts is original.

theorem Cslib.Complexity.width_toThreeSATThree (φ : Logic.PL.CNF ℕ) (c : Logic.PL.Clause ℕ) : c ∈ toThreeSATThree φ → List.length c ≤ 3

Even rejected inputs produce width at most three; no width assumption is required.

theorem Cslib.Complexity.count_vars_toThreeSATThree_le (φ : Logic.PL.CNF ℕ) (v : ℕ) : List.count v (toThreeSATThree φ).vars ≤ 3

Every total output has at most three literal occurrences per variable, including repeats.

theorem Cslib.Complexity.size_toThreeSATThree_le_of_width (φ : Logic.PL.CNF ℕ) (hw : ∀ c ∈ φ, List.length c ≤ 3) : (toThreeSATThree φ).numVars + List.length (toThreeSATThree φ) + (toThreeSATThree φ).vars.length + 1 ≤ List.length φ + 7 * φ.vars.length + 1

Exact clause/literal counts and the generic variable-count bound give this sharper bound on the width-valid branch. Original labels may be arbitrarily large binary naturals.

theorem Cslib.Complexity.size_toThreeSATThree_le (φ : Logic.PL.CNF ℕ) : (toThreeSATThree φ).numVars + List.length (toThreeSATThree φ) + (toThreeSATThree φ).vars.length + 1 ≤ 7 * (List.length φ + φ.vars.length + 1)

The total splitter's incidence size is linearly bounded on all binary-labelled CNF inputs. The rejecting output [[]] has size two, so invalid-width inputs satisfy the same bound.