diff --git a/Complexity.lean b/Complexity.lean
index 2cf1ee1f9..72a705a94 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2133,6 +2133,7 @@ public import Complexity.Logics.Propositional.CNF.Gadgets
 public import Complexity.Logics.Propositional.CNF.ImplicationChain
 public import Complexity.Logics.Propositional.CNF.ImplicationCycle
 public import Complexity.Logics.Propositional.CNF.ModelCount
+public import Complexity.Logics.Propositional.CNF.ModelCount.Relabel
 public import Complexity.Logics.Propositional.CNF.Occurrence
 public import Complexity.Logics.Propositional.CNF.Parity
 public import Complexity.Logics.Propositional.CNF.Planar.Crossover
diff --git a/Complexity/Computability/Complexity/CookLevin/Parsimonious.lean b/Complexity/Computability/Complexity/CookLevin/Parsimonious.lean
index caed324bb..200d4bceb 100644
--- a/Complexity/Computability/Complexity/CookLevin/Parsimonious.lean
+++ b/Complexity/Computability/Complexity/CookLevin/Parsimonious.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Complexity.Classes.SharpP
 public import Complexity.Computability.Complexity.CookLevin.Reduction
 public import Complexity.Logics.Propositional.CNF.ModelCount
+import Complexity.Logics.Propositional.CNF.ModelCount.Relabel
 
 /-!
 # The Cook–Levin reduction is parsimonious
diff --git a/Complexity/Computability/Complexity/Problems/CountingSAT.lean b/Complexity/Computability/Complexity/Problems/CountingSAT.lean
index 05089725b..de5fedc87 100644
--- a/Complexity/Computability/Complexity/Problems/CountingSAT.lean
+++ b/Complexity/Computability/Complexity/Problems/CountingSAT.lean
@@ -17,6 +17,7 @@ import Complexity.Computability.Complexity.CookLevin.Counting
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 import Complexity.Logics.Propositional.CNF.PolyTime
+import Complexity.Logics.Propositional.CNF.ModelCount.Relabel
 
 /-!
 # Complete problems for the counting classes
diff --git a/Complexity/Computability/Complexity/Problems/PlanarThreeSATThree.lean b/Complexity/Computability/Complexity/Problems/PlanarThreeSATThree.lean
index a9c4c4862..059ce2432 100644
--- a/Complexity/Computability/Complexity/Problems/PlanarThreeSATThree.lean
+++ b/Complexity/Computability/Complexity/Problems/PlanarThreeSATThree.lean
@@ -149,7 +149,7 @@ theorem sharpThreeSATThree_toPlanarThreeSATThree (φ : CNF ℕ) :
     SharpThreeSATThree (toPlanarThreeSATThree φ) = SharpThreeSATThree φ := by
   have hout := (ThreeSATThree.syntaxCheck_iff (toPlanarThreeSATThree φ)).2
     ⟨width_toPlanarThreeSATThree φ, count_vars_toPlanarThreeSATThree φ⟩
-  simp only [SharpThreeSATThree, hout, ↓reduceIte]
+  simp only [SharpThreeSATThree, SharpSAT, hout, ↓reduceIte]
   by_cases hg : ThreeSATThree.syntaxCheck φ = true
   · have hs := (ThreeSATThree.syntaxCheck_iff φ).1 hg
     rw [modelCount_toPlanarThreeSATThree φ hs.1 hs.2]
diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCorrectness.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCorrectness.lean
index fbe3820c8..299142aba 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCorrectness.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCorrectness.lean
@@ -46,7 +46,7 @@ theorem crossing_axes_exist {φ : CNF ℕ}
           StraightThrough (occurrencePath φ t) p (0, 1) := by
   have hc := ((PlanarCompile.mem_crossingSites φ p).1 hp).2.2
   rw [← PlanarCompile.occurrencePaths_eq_paths] at hc
-  obtain ⟨i, j, hi, hj, hij, hpi, hpj⟩ := List.exists_pair_indices_of_two_le_filter_contains _ p hc
+  obtain ⟨i, j, hi, hj, hij, hpi, hpj⟩ := (List.two_le_filter_contains_iff _ p).1 hc
   have hi' : i < (Cslib.Logic.PL.occurrences φ).length := by
     simpa only [List.length_map] using hi
   have hj' : j < (Cslib.Logic.PL.occurrences φ).length := by
diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PathAssignments.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PathAssignments.lean
index fb99e4398..69ea4d557 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/Planar/PathAssignments.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PathAssignments.lean
@@ -100,8 +100,7 @@ theorem occurrencePath_crossing_straight {φ : CNF ℕ}
   have hdeg : ∀ v, G.incidenceVertices.count v ≤ 3 := SAT.incidenceGraph_degree_le hw hv
   have hi := occurrence_index_lt ho
   obtain ⟨j, hj, hji, hpj⟩ := List.exists_other_index_of_two_le_filter_contains (paths φ) p
-    ((Cslib.Logic.PL.occurrences φ).idxOf o)
-    (by simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hi) hsite.2.2
+    ((Cslib.Logic.PL.occurrences φ).idxOf o) hsite.2.2
   have hj' : j < G.2.length := by
     simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hj
   have hpi' : p ∈ G.unitPath ((Cslib.Logic.PL.occurrences φ).idxOf o) := by
@@ -181,10 +180,11 @@ theorem shared_ordinary_cell_center {φ : CNF ℕ}
   apply hp
   apply (mem_crossingSites φ p).2
   refine ⟨hcandidate, hc, ?_⟩
-  exact List.two_le_filter_contains_of_indices (paths φ) p
-    (by simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using occurrence_index_lt ho)
-    (by simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using occurrence_index_lt ht)
-    hij (path_mem_paths_get ho hpo) (path_mem_paths_get ht hpt)
+  exact (List.two_le_filter_contains_iff (paths φ) p).2
+    ⟨_, _,
+      by simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using occurrence_index_lt ho,
+      by simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using occurrence_index_lt ht,
+      hij, path_mem_paths_get ho hpo, path_mem_paths_get ht hpt⟩
 
 /-- No retained wire cell is the clause-center endpoint removed by `dropLast`. -/
 theorem clause_center_not_mem_dropLast {φ : CNF ℕ} {o : Occurrence ℕ}
diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Paths/Occupancy.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Paths/Occupancy.lean
index 70a78c5a8..9e29e55b0 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Paths/Occupancy.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/Paths/Occupancy.lean
@@ -43,7 +43,7 @@ theorem paths_filter_length_le_one {φ : CNF ℕ}
   by_contra h
   have ht : 2 ≤ ((paths φ).filter fun r => r.contains p).length := by omega
   obtain ⟨i, j, hi, hj, hij, hpi, hpj⟩ :=
-    List.exists_pair_indices_of_two_le_filter_contains (paths φ) p ht
+    (List.two_le_filter_contains_iff (paths φ) p).1 ht
   have hi' : i < (SAT.incidenceGraph φ).2.length := by
     simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hi
   have hj' : j < (SAT.incidenceGraph φ).2.length := by
diff --git a/Complexity/Computability/Complexity/Problems/ThreeSATThree.lean b/Complexity/Computability/Complexity/Problems/ThreeSATThree.lean
index b2cbc9f37..be7ce0bb8 100644
--- a/Complexity/Computability/Complexity/Problems/ThreeSATThree.lean
+++ b/Complexity/Computability/Complexity/Problems/ThreeSATThree.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Computability.Complexity.Problems.ThreeSAT
 public import Complexity.Logics.Propositional.CNF.ThreeOccurrence
+import Complexity.Logics.Propositional.CNF.ModelCount.Relabel
 import Complexity.Logics.Propositional.CNF.ThreeOccurrence.PolyTime
 import Complexity.Computability.Complexity.Problems.SAT.PolyTime
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
diff --git a/Complexity/Computability/Complexity/Problems/ThreeSATThree/Counting.lean b/Complexity/Computability/Complexity/Problems/ThreeSATThree/Counting.lean
index b6e9f2dbe..841ea03cd 100644
--- a/Complexity/Computability/Complexity/Problems/ThreeSATThree/Counting.lean
+++ b/Complexity/Computability/Complexity/Problems/ThreeSATThree/Counting.lean
@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Complexity.Classes.SharpP.Completeness
+public import Complexity.Computability.Complexity.Problems.SharpSAT
 public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Size
 public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Syntax
 
@@ -17,7 +18,7 @@ public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Syntax
 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
+They reuse `SharpSAT` and the existing syntax guards rather than introducing new assignment
 or satisfiability semantics.
 
 ## Main definitions
@@ -28,12 +29,15 @@ or satisfiability semantics.
 ## Main results
 
 * `Cslib.Complexity.sharpThreeSATThree_toThreeSATThree`: exact counts for the total compiler.
+* `Cslib.Complexity.SharpThreeSAT.mem_ThreeSAT_iff`,
+  `Cslib.Complexity.SharpThreeSATThree.mem_ThreeSATThree_iff`: positivity recovers the languages.
 * `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`.
+The occurrence construction and its source credit are documented in `ThreeSATThree`. Its count
+preservation is an original elementary consequence of `CNF.copies_agree`.
 -/
 
 @[expose] public section
@@ -45,24 +49,43 @@ 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
+  if φ.all (fun c => decide (c.length ≤ 3)) then SharpSAT φ 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
+  if ThreeSATThree.syntaxCheck φ then SharpSAT φ else 0
+
+/-- Membership in `ThreeSAT` is equivalent to a positive guarded model count. -/
+theorem SharpThreeSAT.mem_ThreeSAT_iff {φ : CNF ℕ} :
+    φ ∈ ThreeSAT ↔ 0 < SharpThreeSAT φ := by
+  simp only [ThreeSAT, Set.mem_ofPred_eq, SharpThreeSAT]
+  split <;> simp_all [List.all_eq_true, CNF.modelCount_pos_iff, SharpSAT]
+
+/-- Membership in `ThreeSATThree` is equivalent to a positive guarded model count. -/
+theorem SharpThreeSATThree.mem_ThreeSATThree_iff {φ : CNF ℕ} :
+    φ ∈ ThreeSATThree ↔ 0 < SharpThreeSATThree φ := by
+  by_cases hg : ThreeSATThree.syntaxCheck φ = true
+  · obtain ⟨hw, hv⟩ := (ThreeSATThree.syntaxCheck_iff φ).mp hg
+    simp only [ThreeSATThree, Set.mem_ofPred_eq, SharpThreeSATThree, hg, ↓reduceIte,
+      SharpSAT, CNF.modelCount_pos_iff]
+    exact ⟨fun h => h.2.2, fun hs => ⟨hw, hv, hs⟩⟩
+  · simp only [ThreeSATThree, Set.mem_ofPred_eq, SharpThreeSATThree, hg, Bool.false_eq_true,
+      ite_false, Nat.lt_irrefl, iff_false]
+    rintro ⟨hw, hv, _⟩
+    exact hg ((ThreeSATThree.syntaxCheck_iff φ).mpr ⟨hw, hv⟩)
 
 /-- 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]
+  simp only [SharpThreeSATThree, hout, ↓reduceIte, SharpSAT]
   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, hw, ↓reduceIte, SharpSAT]
   · simp only [SharpThreeSAT, toThreeSATThree, hw, Bool.false_eq_true, ite_false]
     decide
 
diff --git a/Complexity/Foundations/Data/List/Filter.lean b/Complexity/Foundations/Data/List/Filter.lean
index 1af02195a..55c8bc424 100644
--- a/Complexity/Foundations/Data/List/Filter.lean
+++ b/Complexity/Foundations/Data/List/Filter.lean
@@ -18,8 +18,7 @@ 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.two_le_filter_contains_iff`.
 * `List.exists_other_index_of_two_le_filter_contains`.
 -/
 
@@ -27,110 +26,83 @@ They are generalized from the canonical incidence-path occupancy proofs.
 
 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]
+/-- At least two memberships correspond to distinct indices, even for repeated equal lists. -/
+theorem two_le_filter_contains_iff {α : Type*} [DecidableEq α]
+    (rs : List (List α)) (p : α) :
+    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
+  constructor
+  · intro hlen
+    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
-        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
+        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⟩
+  · rintro ⟨i, j, hi, hj, hij, hpi, hpj⟩
+    induction rs generalizing i j with
+    | nil => simp at hi
+    | cons r rs ih =>
+      cases i 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]
+        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
-        · exact ht
+        | succ j =>
+          have ht := ih i j (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. -/
+/-- Two filtered memberships give an index different from any given natural number. -/
 theorem exists_other_index_of_two_le_filter_contains {α : Type*} [DecidableEq α]
-    (rs : List (List α)) (p : α) (i : ℕ) (hi : i < rs.length)
+    (rs : List (List α)) (p : α) (i : ℕ)
     (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⟩
-
+  obtain ⟨j, k, hj, hk, hjk, hpj, hpk⟩ := (two_le_filter_contains_iff rs p).1 hcount
+  by_cases hji : j = i
+  · exact ⟨k, hk, by omega, hpk⟩
+  · exact ⟨j, hj, hji, hpj⟩
 
 end List
diff --git a/Complexity/Foundations/Data/List/Last.lean b/Complexity/Foundations/Data/List/Last.lean
index b0781335c..f19693bcf 100644
--- a/Complexity/Foundations/Data/List/Last.lean
+++ b/Complexity/Foundations/Data/List/Last.lean
@@ -8,12 +8,13 @@ module
 -- upstream: candidate
 
 public import Complexity.Init
-import Mathlib.Data.List.GetD
+import Init.Data.List.Lemmas
 
 /-!
 # Defaulted last-element lookup
 
-The default is unused for a nonempty list. The proof is moved from the path semantics.
+The default is unused for a nonempty list. This indexed form follows from the core last-element
+lookup API.
 
 ## Main results
 
@@ -27,14 +28,7 @@ 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]
-
+  rw [List.getLastD_eq_getLast?, List.getLast?_eq_some_getLast hne]
+  exact List.getLast_eq_getElem hne
 
 end List
diff --git a/Complexity/Logics/Propositional/CNF/Compact/ModelCount.lean b/Complexity/Logics/Propositional/CNF/Compact/ModelCount.lean
index 83e40eca3..04a2752b0 100644
--- a/Complexity/Logics/Propositional/CNF/Compact/ModelCount.lean
+++ b/Complexity/Logics/Propositional/CNF/Compact/ModelCount.lean
@@ -8,8 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Logics.Propositional.CNF.Compact
-public import Complexity.Logics.Propositional.CNF.ModelCount
-import Mathlib.Data.List.GetD
+public import Complexity.Logics.Propositional.CNF.ModelCount.Relabel
 
 /-!
 # Model counts under compact variable numbering
@@ -35,24 +34,6 @@ variable {V : Type*} [DecidableEq V]
 /-- First-occurrence numbering preserves the number of satisfying assignments, including for
 empty formulas, empty clauses, and repeated literal occurrences. -/
 theorem modelCount_compact (φ : CNF V) : φ.compact.modelCount = φ.modelCount := by
-  refine modelCount_eq_card_filter (fun σ (v : φ.vars.toFinset) => σ (φ.vars.idxOf (v : V)))
-    (fun τ => φ.eval (φ.extendAssignment τ) = true) (fun σ τ _ _ => ?_) fun τ => ?_
-  · rw [compact, vars_relabel, List.forall_mem_map, funext_iff, Subtype.forall]
-    simp only [List.mem_toFinset]
-  · constructor
-    · intro hτ
-      let σ : ℕ → Bool := fun i => φ.vars[i]?.elim false (φ.extendAssignment τ)
-      have he : ∀ v ∈ φ.vars, σ (φ.vars.idxOf v) = φ.extendAssignment τ v := by
-        intro v hv
-        simp [σ, List.getElem?_idxOf hv]
-      refine ⟨σ, ?_, funext fun v => ?_⟩
-      · rw [compact, eval_relabel]
-        exact (eval_congr he).trans hτ
-      · exact (he v (List.mem_toFinset.1 v.2)).trans
-          (extendAssignment_of_mem _ (List.mem_toFinset.1 v.2))
-    · rintro ⟨σ, hσ, rfl⟩
-      rw [compact, eval_relabel] at hσ
-      rw [← hσ]
-      exact eval_extendAssignment_restrict φ (σ ∘ φ.vars.idxOf)
+  exact modelCount_relabel_of_injOn φ (fun _ ha _ _ h => (List.idxOf_inj ha).1 h)
 
 end Cslib.Logic.PL.CNF
diff --git a/Complexity/Logics/Propositional/CNF/ModelCount.lean b/Complexity/Logics/Propositional/CNF/ModelCount.lean
index 19a74e6ee..1594bcc40 100644
--- a/Complexity/Logics/Propositional/CNF/ModelCount.lean
+++ b/Complexity/Logics/Propositional/CNF/ModelCount.lean
@@ -17,9 +17,9 @@ public import Mathlib.Data.Nat.Bitwise
 
 `CNF.modelCount φ` is the number of satisfying assignments of a formula `φ` in conjunctive normal
 form: the assignments of the variables occurring in `φ` (`CNF.vars`) that satisfy it. Variables
-not occurring in `φ` are not counted, so the count does not depend on the type of variables, and
-injective relabelling preserves it (`CNF.modelCount_relabel`). As a function of the formula this
-is the counting problem `#SAT` [Valiant][Valiant1979].
+not occurring in `φ` are not counted, so the count does not depend on the type of variables.
+Relabelling results are in `CNF.ModelCount.Relabel`. As a function of the formula this is the
+counting problem `#SAT` [Valiant][Valiant1979].
 
 The distinct variables of `φ` in order of their first occurrence are listed by `CNF.distinctVars`,
 of length `CNF.numVars` (`CNF.length_distinctVars`), and the literal occurrences with their clause
@@ -58,7 +58,6 @@ with a given one on the variables of the formula (`CNF.modelCount_eq_one_iff`).
   `Cslib.Logic.PL.CNF.satisfiable_iff_exists_bitsAssignment`: satisfiability is a search over
   `2 ^ |vs|` numbered assignments.
 * `Cslib.Logic.PL.CNF.modelCount_eq_card_filter`: counting satisfying assignments through a map.
-* `Cslib.Logic.PL.CNF.modelCount_relabel`: injective relabelling preserves the count.
 * `Cslib.Logic.PL.CNF.modelCount_pos_iff`, `Cslib.Logic.PL.CNF.modelCount_eq_one_iff`.
 
 ## References
@@ -73,7 +72,7 @@ namespace Cslib.Logic.PL
 
 open Cslib.Complexity
 
-variable {V W : Type*}
+variable {V : Type*}
 
 /-- An occurrence of a literal in a formula: its clause, its position in the clause, and the
 literal. -/
@@ -229,23 +228,6 @@ theorem CNF.modelCount_eq_card_filter {ι : Type*} [Fintype ι] {φ : CNF V}
     exact ⟨_, Finset.mem_filter.2 ⟨Finset.mem_univ _, he⟩,
       (hf _ _ he hσ).2 fun _ hv => CNF.extendAssignment_of_mem _ hv⟩
 
-/-- **Relabelling along an injective map preserves the number of satisfying assignments.** -/
-theorem CNF.modelCount_relabel [DecidableEq W] {f : V → W} (hf : Function.Injective f)
-    (φ : CNF V) : (φ.relabel f).modelCount = φ.modelCount := by
-  refine CNF.modelCount_eq_card_filter (fun σ (v : φ.vars.toFinset) => σ (f v))
-    (fun τ => φ.eval (φ.extendAssignment τ) = true) (fun σ τ _ _ => ?_) fun τ => ?_
-  · rw [CNF.vars_relabel, List.forall_mem_map, funext_iff, Subtype.forall]
-    simp only [List.mem_toFinset]
-  · constructor
-    · intro hτ
-      refine ⟨Function.extend f (φ.extendAssignment τ) fun _ => false, ?_, funext fun v => ?_⟩
-      · rwa [CNF.eval_relabel, Function.extend_comp hf]
-      · rw [hf.extend_apply, CNF.extendAssignment_of_mem _ (List.mem_toFinset.1 v.2)]
-    · rintro ⟨σ, hσ, rfl⟩
-      rw [CNF.eval_relabel] at hσ
-      rw [← hσ]
-      exact CNF.eval_congr fun v hv => CNF.extendAssignment_of_mem _ hv
-
 /-- A formula has a satisfying assignment exactly when its count is positive. -/
 theorem CNF.modelCount_pos_iff {φ : CNF V} : 0 < φ.modelCount ↔ φ.Satisfiable := by
   rw [CNF.modelCount, Finset.card_pos, Finset.filter_nonempty_iff]
diff --git a/Complexity/Logics/Propositional/CNF/ModelCount/Relabel.lean b/Complexity/Logics/Propositional/CNF/ModelCount/Relabel.lean
new file mode 100644
index 000000000..3be1851a2
--- /dev/null
+++ b/Complexity/Logics/Propositional/CNF/ModelCount/Relabel.lean
@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger, Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger, Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Logics.Propositional.CNF.ModelCount
+
+/-!
+# Model counts under CNF relabelling
+
+Relabelling preserves the count when it is injective on the occurring variables. Collisions
+outside that support are harmless, including when the source variable type is infinite or empty.
+
+## Main results
+
+* `Cslib.Logic.PL.CNF.modelCount_relabel_of_injOn`: support-injective relabelling preserves counts.
+* `Cslib.Logic.PL.CNF.modelCount_relabel`: globally injective relabelling preserves counts.
+
+## References
+
+These are original elementary transport proofs for the existing occurring-variable model count.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.PL.CNF
+
+variable {V W : Type*} [DecidableEq V]
+
+/-- Relabelling injectively on the occurring variables preserves the number of satisfying
+assignments. No injectivity is required outside those variables. -/
+theorem modelCount_relabel_of_injOn [DecidableEq W] {f : V → W} (φ : CNF V)
+    (hf : Set.InjOn f {v | v ∈ φ.vars}) : (φ.relabel f).modelCount = φ.modelCount := by
+  have hf' : Function.Injective (fun v : φ.vars.toFinset => f v) :=
+    fun a b h => Subtype.ext (hf (List.mem_toFinset.1 a.2) (List.mem_toFinset.1 b.2) h)
+  refine modelCount_eq_card_filter (fun σ (v : φ.vars.toFinset) => σ (f v))
+    (fun τ => φ.eval (φ.extendAssignment τ) = true) (fun σ τ _ _ => ?_) fun τ => ?_
+  · rw [vars_relabel, List.forall_mem_map, funext_iff, Subtype.forall]
+    simp only [List.mem_toFinset]
+  · constructor
+    · intro hτ
+      let σ := Function.extend (fun v : φ.vars.toFinset => f v) τ (fun _ => false)
+      have he (v : V) (hv : v ∈ φ.vars) : σ (f v) = φ.extendAssignment τ v := by
+        rw [extendAssignment_of_mem _ hv]
+        exact hf'.extend_apply τ (fun _ => false) ⟨v, List.mem_toFinset.2 hv⟩
+      refine ⟨σ, ?_, funext fun v => ?_⟩
+      · rw [eval_relabel]
+        exact (eval_congr he).trans hτ
+      · exact hf'.extend_apply τ (fun _ => false) v
+    · rintro ⟨σ, hσ, rfl⟩
+      rw [eval_relabel] at hσ
+      rw [← hσ]
+      exact eval_congr fun v hv => extendAssignment_of_mem _ hv
+
+/-- **Relabelling along an injective map preserves the number of satisfying assignments.** -/
+theorem modelCount_relabel [DecidableEq W] {f : V → W} (hf : Function.Injective f)
+    (φ : CNF V) : (φ.relabel f).modelCount = φ.modelCount :=
+  modelCount_relabel_of_injOn φ (fun _ _ _ _ h => hf h)
+
+end Cslib.Logic.PL.CNF
diff --git a/Complexity/Logics/Propositional/CNF/ThreeOccurrence.lean b/Complexity/Logics/Propositional/CNF/ThreeOccurrence.lean
index 9c714a4f0..94fb6c053 100644
--- a/Complexity/Logics/Propositional/CNF/ThreeOccurrence.lean
+++ b/Complexity/Logics/Propositional/CNF/ThreeOccurrence.lean
@@ -28,6 +28,8 @@ Adapted from `lean-trominoes` at `6d5b36c15cec6cb18d30137b7f1c7fb92ea24332`,
 `LeanTrominoes/SAT/ThreeSAT/PeriodicThreeSATThree{,Correctness,ExactSize}.lean`.
 This construction uses ordinary CNF formulas and Boolean assignments.
 
+The model-count preservation proof is original here, an elementary consequence of `copies_agree`.
+
 ## Main definitions
 
 * `Cslib.Logic.PL.CNF.occurrenceClauses`: separate the literal occurrences.
diff --git a/ComplexityTests/ListFilter.lean b/ComplexityTests/ListFilter.lean
new file mode 100644
index 000000000..f551cc867
--- /dev/null
+++ b/ComplexityTests/ListFilter.lean
@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+import Complexity.Foundations.Data.List.Filter
+
+-- Equal list values still occupy two distinct positions.
+example : ∃ (i j : ℕ) (hi : i < ([[7], [7]] : List (List ℕ)).length)
+    (hj : j < ([[7], [7]] : List (List ℕ)).length),
+    i ≠ j ∧ 7 ∈ ([[7], [7]] : List (List ℕ))[i] ∧
+      7 ∈ ([[7], [7]] : List (List ℕ))[j] :=
+  (List.two_le_filter_contains_iff [[7], [7]] 7).1 (by decide)
+
+example : ¬ 2 ≤ (([[7], []] : List (List ℕ)).filter fun r => r.contains 7).length := by
+  decide
+
+-- The excluded index need not itself be in bounds.
+example : ∃ j, ∃ hj : j < ([[7], [7]] : List (List ℕ)).length,
+    j ≠ 100 ∧ 7 ∈ ([[7], [7]] : List (List ℕ))[j] :=
+  List.exists_other_index_of_two_le_filter_contains [[7], [7]] 7 100 (by decide)
+
+example : ¬ 2 ≤ (([] : List (List ℕ)).filter fun r => r.contains 7).length := by
+  decide
diff --git a/ComplexityTests/ThreeSATThreeCounting.lean b/ComplexityTests/ThreeSATThreeCounting.lean
index 270dafc50..b8dce4903 100644
--- a/ComplexityTests/ThreeSATThreeCounting.lean
+++ b/ComplexityTests/ThreeSATThreeCounting.lean
@@ -6,6 +6,8 @@ Authors: Erik Demaine
 
 import Complexity.Computability.Complexity.Problems.ThreeSATThree
 import Complexity.Computability.Complexity.Problems.ThreeSATThree.Counting
+import Complexity.Logics.Propositional.CNF.Compact.ModelCount
+import Complexity.Logics.Propositional.CNF.ModelCount.Relabel
 
 /-! # Exact counts under occurrence splitting and numbering -/
 
@@ -62,3 +64,52 @@ example : SharpThreeSATThree
     (toThreeSATThree [[(0, true), (0, true), (0, true)], [(0, true)]]) = 1 := by
   rw [sharpThreeSATThree_toThreeSATThree]
   decide
+
+/-- Two used labels stay distinct even though parity merges many unused labels. -/
+example : CNF.modelCount (CNF.relabel (fun v : ℕ => v % 2) [[(7, true), (42, true)]]) = 3 := by
+  rw [CNF.modelCount_relabel_of_injOn _ (by
+    intro a ha b hb h
+    change a ∈ [7, 42] at ha
+    change b ∈ [7, 42] at hb
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at ha hb
+    rcases ha with rfl | rfl <;> rcases hb with rfl | rfl <;> first | rfl | norm_num at h)]
+  decide
+
+/-- Identifying two occurring variables can change a disjunction's model count. -/
+example :
+    CNF.modelCount ([[(0, true), (1, true)]] : CNF ℕ) = 3 ∧
+    CNF.modelCount (CNF.relabel (fun _ => 0) ([[(0, true), (1, true)]] : CNF ℕ)) = 1 := by
+  decide
+
+/-- The transport theorem also applies to an empty source variable type. -/
+example : CNF.modelCount (CNF.relabel (fun v => nomatch v : Empty → ℕ) []) = 1 := by
+  rw [CNF.modelCount_relabel_of_injOn _ (fun v => nomatch v)]
+  decide
+
+/-- An empty support permits even a constant map from an infinite variable type. -/
+example : CNF.modelCount (CNF.relabel (fun _ => 0) ([] : CNF ℕ)) = 1 := by
+  rw [CNF.modelCount_relabel_of_injOn _ (by simp [CNF.vars, Set.InjOn])]
+  decide
+
+/-- Repeated first occurrences leave a gap in compact names while preserving all models. -/
+example :
+    CNF.compact ([[(1000000, true), (1000000, true), (7, true)]] : CNF ℕ) =
+      [[(0, true), (0, true), (2, true)]] ∧
+    CNF.modelCount (CNF.compact ([[(1000000, true), (1000000, true), (7, true)]] : CNF ℕ)) = 3 := by
+  constructor
+  · decide
+  · rw [CNF.modelCount_compact]
+    decide
+
+/-- Positive guarded source counts recover the existing decision language. -/
+example : [[(7, true)]] ∈ ThreeSAT :=
+  SharpThreeSAT.mem_ThreeSAT_iff.mpr (by decide)
+
+/-- Positive guarded target counts recover the existing decision language. -/
+example : [[(7, true)]] ∈ ThreeSATThree :=
+  SharpThreeSATThree.mem_ThreeSATThree_iff.mpr (by decide)
+
+/-- Rejected target syntax cannot belong to the decision language, even when satisfiable. -/
+example : [[(0, true), (0, true), (0, true)], [(0, true)]] ∉ ThreeSATThree := by
+  rw [SharpThreeSATThree.mem_ThreeSATThree_iff]
+  decide