feat(CNF): preserve model counts under occurrence splitting

Complexity.lean

@@ -828,6 +828,7 @@ public import Complexity.Computability.Complexity.Problems.TQBF.Closed
 public import Complexity.Computability.Complexity.Problems.TSP
 public import Complexity.Computability.Complexity.Problems.ThreeSAT
 public import Complexity.Computability.Complexity.Problems.ThreeSATThree
+public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Counting
 public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Size
 public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Syntax
 public import Complexity.Computability.Complexity.Problems.TwoSAT
@@ -1886,10 +1887,13 @@ public import Complexity.Foundations.Data.List.BalancedFold
 public import Complexity.Foundations.Data.List.Basic
 public import Complexity.Foundations.Data.List.Counting
 public import Complexity.Foundations.Data.List.Equiv
+public import Complexity.Foundations.Data.List.Filter
 public import Complexity.Foundations.Data.List.Fold
+public import Complexity.Foundations.Data.List.Last
 public import Complexity.Foundations.Data.List.Lex
 public import Complexity.Foundations.Data.List.Lookup
 public import Complexity.Foundations.Data.List.OfFn
+public import Complexity.Foundations.Data.List.Range
 public import Complexity.Foundations.Data.List.SelectDistinct
 public import Complexity.Foundations.Data.Matrix.Binary
 public import Complexity.Foundations.Data.Matrix.Permanent
@@ -2080,6 +2084,7 @@ public import Complexity.Logics.FirstOrder.Tuple
 public import Complexity.Logics.Propositional.CNF
 public import Complexity.Logics.Propositional.CNF.Coding
 public import Complexity.Logics.Propositional.CNF.Compact
+public import Complexity.Logics.Propositional.CNF.Compact.ModelCount
 public import Complexity.Logics.Propositional.CNF.Compact.Relabel
 public import Complexity.Logics.Propositional.CNF.ExactlyOne
 public import Complexity.Logics.Propositional.CNF.Gadgets

Complexity/Computability/Complexity/Problems/ThreeSATThree.lean

@@ -42,6 +42,7 @@ This endpoint imposes no planarity condition.
 ## Main results
 
 * `Cslib.Complexity.mem_ThreeSATThree_toThreeSATThree_iff`: correctness of the reduction.
+* `Cslib.Complexity.modelCount_toThreeSATThree`: preservation of counts for width-three inputs.
 * `Cslib.Complexity.computableInPolyTime_toThreeSATThree`: native polynomial time under `encCNF`.
 * `Cslib.Complexity.ThreeSATThree_npComplete`: 3SAT-3 is NP-complete.
 
@@ -149,6 +150,14 @@ theorem length_vars_toThreeSATThree (φ : CNF ℕ) (hφ : ∀ c ∈ φ, c.length
   have hg : φ.all (fun c => decide (c.length ≤ 3)) = true := by simpa using hφ
   simp [toThreeSATThree, hg, CNF.vars_relabel, CNF.length_vars_toThreeOccurrence]
 
+/-- For a width-three input, occurrence splitting and injective numbering preserve the number of
+satisfying assignments on occurring variables. -/
+theorem modelCount_toThreeSATThree (φ : CNF ℕ) (hφ : ∀ c ∈ φ, c.length ≤ 3) :
+    (toThreeSATThree φ).modelCount = φ.modelCount := by
+  have hg : φ.all (fun c => decide (c.length ≤ 3)) = true := by simpa using hφ
+  simp only [toThreeSATThree, hg, ↓reduceIte]
+  rw [CNF.modelCount_relabel ThreeSATThree.numberCopy_injective, CNF.modelCount_toThreeOccurrence]
+
 /-- The total splitter is polynomial-time under binary `encCNF`. -/
 @[fun_prop]
 theorem computableInPolyTime_toThreeSATThree :

Complexity/Computability/Complexity/Problems/ThreeSATThree/Counting.lean

@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Complexity.Classes.SharpP.Completeness
+public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Size
+public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Syntax
+
+/-!
+# Parsimonious occurrence reduction for 3SAT
+
+The existing occurrence splitter preserves the number of satisfying assignments. Each source
+variable has one value on every copy in its implication cycle, and numbering copies is injective.
+The counting problems below count only occurring variables and return zero outside their syntax.
+They reuse `CNF.modelCount` and the existing syntax guards rather than introducing new assignment
+or satisfiability semantics.
+
+## Main definitions
+
+* `Cslib.Complexity.SharpThreeSAT`: model count for width-at-most-three CNF, zero otherwise.
+* `Cslib.Complexity.SharpThreeSATThree`: model count with the additional three-occurrence bound.
+
+## Main results
+
+* `Cslib.Complexity.sharpThreeSATThree_toThreeSATThree`: exact counts for the total compiler.
+* `Cslib.Complexity.parsimoniousReducible_SharpThreeSAT_SharpThreeSATThree`: the existing
+  polynomial-time compiler is a parsimonious reduction.
+
+## References
+
+The occurrence construction and its source credit are documented in `ThreeSATThree`.
+-/
+
+@[expose] public section
+
+namespace Cslib.Complexity
+
+open Cslib.Logic.PL
+
+/-- Count satisfying assignments of width-at-most-three CNF; reject other syntax with count zero.
+Only variables occurring in the formula are counted. -/
+def SharpThreeSAT (φ : CNF ℕ) : ℕ :=
+  if φ.all (fun c => decide (c.length ≤ 3)) then φ.modelCount else 0
+
+/-- Count satisfying assignments of width-three, occurrence-three CNF; reject other syntax with
+count zero. Repetitions are literal positions, as in `ThreeSATThree.syntaxCheck`. -/
+def SharpThreeSATThree (φ : CNF ℕ) : ℕ :=
+  if ThreeSATThree.syntaxCheck φ then φ.modelCount else 0
+
+/-- The total occurrence compiler preserves the count, including rejected inputs. -/
+theorem sharpThreeSATThree_toThreeSATThree (φ : CNF ℕ) :
+    SharpThreeSATThree (toThreeSATThree φ) = SharpThreeSAT φ := by
+  have hout := (ThreeSATThree.syntaxCheck_iff (toThreeSATThree φ)).2
+    ⟨width_toThreeSATThree φ, count_vars_toThreeSATThree_le φ⟩
+  simp only [SharpThreeSATThree, hout, ↓reduceIte]
+  by_cases hw : φ.all (fun c => decide (c.length ≤ 3)) = true
+  · have hwidth : ∀ c ∈ φ, c.length ≤ 3 := by
+      simpa only [List.all_eq_true, decide_eq_true_eq] using hw
+    rw [modelCount_toThreeSATThree φ hwidth]
+    simp only [SharpThreeSAT, hw, ↓reduceIte]
+  · simp only [SharpThreeSAT, toThreeSATThree, hw, Bool.false_eq_true, ite_false]
+    decide
+
+/-- The already-certified polynomial-time 3SAT-to-3SAT-3 compiler is parsimonious. -/
+theorem parsimoniousReducible_SharpThreeSAT_SharpThreeSATThree :
+    ParsimoniousReducible encCNF encCNF SharpThreeSAT SharpThreeSATThree :=
+  ⟨toThreeSATThree, computableInPolyTime_toThreeSATThree,
+    fun φ => (sharpThreeSATThree_toThreeSATThree φ).symm⟩
+
+end Cslib.Complexity

Complexity/Foundations/Data/List/Filter.lean

@@ -0,0 +1,136 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Init
+import Mathlib.Data.List.GetD
+
+/-!
+# Indexed multiplicity under list membership filtering
+
+These statements count positions, so repeated equal lists still contribute separately.
+They are generalized from the canonical incidence-path occupancy proofs.
+
+## Main results
+
+* `List.exists_pair_indices_of_two_le_filter_contains`.
+* `List.two_le_filter_contains_of_indices`.
+* `List.exists_other_index_of_two_le_filter_contains`.
+-/
+
+@[expose] public section
+
+namespace List
+
+/-- Two filtered memberships occur at distinct indices, even for repeated lists. -/
+theorem exists_pair_indices_of_two_le_filter_contains {α : Type*} [DecidableEq α]
+    (rs : List (List α)) (p : α)
+    (hlen : 2 ≤ (rs.filter fun r => r.contains p).length) :
+    ∃ (i j : ℕ) (hi : i < rs.length) (hj : j < rs.length),
+      i ≠ j ∧ p ∈ rs[i] ∧ p ∈ rs[j] := by
+  induction rs with
+  | nil => simp at hlen
+  | cons r rs ih =>
+    by_cases hp : p ∈ r
+    · have hne : (rs.filter fun r => r.contains p) ≠ [] := by
+        intro h
+        have hf : ((r :: rs).filter fun r => r.contains p) = [r] := by
+          have hpred : r.contains p = true := by simpa using hp
+          simp only [List.filter_cons, hpred, ↓reduceIte, h]
+        rw [hf] at hlen
+        simp at hlen
+      cases hf : rs.filter (fun r => r.contains p) with
+      | nil => exact False.elim (hne hf)
+      | cons t ts =>
+        have ht : t ∈ rs.filter (fun r => r.contains p) := by rw [hf]; simp
+        obtain ⟨htmem, htp⟩ := List.mem_filter.mp ht
+        obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp htmem
+        exact ⟨0, j + 1, by simp, by simpa using hj, by omega, hp, by simpa using htp⟩
+    · have hf : ((r :: rs).filter fun r => r.contains p) = rs.filter (fun r => r.contains p) := by
+        simp [hp]
+      rw [hf] at hlen
+      obtain ⟨i, j, hi, hj, hij, hpi, hpj⟩ := ih hlen
+      exact ⟨i + 1, j + 1, by simpa using hi, by simpa using hj, by omega, hpi, hpj⟩
+
+/-- Two distinct indices witnessing membership give at least two filtered entries. -/
+theorem two_le_filter_contains_of_indices {α : Type*} [DecidableEq α]
+    (rs : List (List α)) (p : α) {i j : ℕ}
+    (hi : i < rs.length) (hj : j < rs.length) (hij : i ≠ j)
+    (hpi : p ∈ rs[i]) (hpj : p ∈ rs[j]) :
+    2 ≤ (rs.filter fun r => r.contains p).length := by
+  induction rs generalizing i j with
+  | nil => simp at hi
+  | cons r rs ih =>
+    cases i with
+    | zero =>
+      cases j with
+      | zero => exact False.elim (hij rfl)
+      | succ j =>
+        have hj' : j < rs.length := by simpa using hj
+        have hm : rs[j] ∈ rs.filter (fun r => r.contains p) :=
+          List.mem_filter.mpr ⟨List.getElem_mem (by simpa using hj),
+            List.contains_iff_mem.mpr hpj⟩
+        obtain ⟨k, hk, _⟩ := List.mem_iff_getElem.mp hm
+        have hphead : p ∈ r := hpi
+        simp only [List.filter_cons, List.contains_iff_mem.mpr hphead,
+          ite_true, List.length_cons]
+        omega
+    | succ i =>
+      cases j with
+      | zero =>
+        have hi' : i < rs.length := by simpa using hi
+        have hm : rs[i] ∈ rs.filter (fun r => r.contains p) :=
+          List.mem_filter.mpr ⟨List.getElem_mem (by simpa using hi),
+            List.contains_iff_mem.mpr hpi⟩
+        obtain ⟨k, hk, _⟩ := List.mem_iff_getElem.mp hm
+        have hphead : p ∈ r := hpj
+        simp only [List.filter_cons, List.contains_iff_mem.mpr hphead,
+          ite_true, List.length_cons]
+        omega
+      | succ j =>
+        have ht := ih (by simpa using hi) (by simpa using hj) (by omega) hpi hpj
+        rw [List.filter_cons]
+        split_ifs
+        · simp only [List.length_cons]
+          omega
+        · exact ht
+
+/-- At least two filtered memberships give an index different from any given index. -/
+theorem exists_other_index_of_two_le_filter_contains {α : Type*} [DecidableEq α]
+    (rs : List (List α)) (p : α) (i : ℕ) (hi : i < rs.length)
+    (hcount : 2 ≤ (rs.filter fun r => r.contains p).length) :
+    ∃ j, ∃ hj : j < rs.length, j ≠ i ∧ p ∈ rs[j] := by
+  induction rs generalizing i with
+  | nil => simp at hi
+  | cons r rs ih =>
+    cases i with
+    | zero =>
+      have hpos : 0 < (rs.filter fun r => r.contains p).length := by
+        rw [List.filter_cons] at hcount
+        split_ifs at hcount
+        · simp only [List.length_cons] at hcount
+          omega
+        · omega
+      obtain ⟨s, hs⟩ := List.exists_mem_of_length_pos hpos
+      have hm := List.mem_filter.mp hs
+      obtain ⟨j, hj, hsj⟩ := List.mem_iff_getElem.mp hm.1
+      refine ⟨j + 1, by simp only [List.length_cons]; omega, by omega, ?_⟩
+      simp only [List.getElem_cons_succ]
+      rw [hsj]
+      exact List.contains_iff_mem.mp hm.2
+    | succ i =>
+      by_cases hmem : r.contains p = true
+      · exact ⟨0, by simp, by omega, by simpa using List.contains_iff_mem.mp hmem⟩
+      · have ht : 2 ≤ (rs.filter fun r => r.contains p).length := by
+          have hp : p ∉ r := fun hp => hmem (List.contains_iff_mem.mpr hp)
+          simpa [List.filter_cons, hp] using hcount
+        obtain ⟨j, hj, hji, hp⟩ := ih i (by simp only [List.length_cons] at hi; omega) ht
+        exact ⟨j + 1, by simp only [List.length_cons]; omega, by omega, by simpa using hp⟩
+
+
+end List

Complexity/Foundations/Data/List/Last.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Init
+import Mathlib.Data.List.GetD
+
+/-!
+# Defaulted last-element lookup
+
+The default is unused for a nonempty list. The proof is moved from the path semantics.
+
+## Main results
+
+* `List.getLastD_eq_getElem`.
+-/
+
+@[expose] public section
+
+namespace List
+
+/-- A nonempty list's defaulted last lookup is its final indexed element. -/
+theorem getLastD_eq_getElem {α : Type*} (xs : List α) (d : α) (hne : xs ≠ []) :
+    xs.getLastD d = xs[xs.length - 1]'(by cases xs <;> simp_all) := by
+  induction xs generalizing d with
+  | nil => exact False.elim (hne rfl)
+  | cons a xs ih =>
+    cases xs with
+    | nil => rfl
+    | cons b xs =>
+      rw [List.getLastD_cons, ih a (List.cons_ne_nil _ _)]
+      simp only [List.length_cons, Nat.add_sub_cancel, List.getElem_cons_succ]
+
+
+end List

Complexity/Foundations/Data/List/Range.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Init
+import Mathlib.Data.List.GetD
+import Mathlib.Data.List.Nodup
+
+/-!
+# First indices in natural-number ranges
+
+This index identity is shared by source endpoint and path geometry certificates.
+
+## Main results
+
+* `List.idxOf_range_of_lt`.
+-/
+
+@[expose] public section
+
+namespace List
+
+/-- An in-range natural number occurs at its own position in `range`. -/
+theorem idxOf_range_of_lt {i n : ℕ} (hi : i < n) : (List.range n).idxOf i = i := by
+  have h := (List.nodup_range : (List.range n).Nodup).idxOf_getElem i
+    (by simpa only [List.length_range] using hi)
+  rw [List.getElem_range] at h
+  exact h
+
+
+end List