From 63cd6fdf35f65c13bb587b6dcfe0c94f18f3ecc9 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Thu, 29 Oct 2026 22:32:27 +0000
Subject: [PATCH] refactor: deduplicate helpers across Planar, Expander,
 BitString, and Reductions (#949)

---
 .../Computability/Circuit/Arithmetic/VP.lean  |  5 +-
 .../Classes/ArthurMerlin/SetLowerBound.lean   | 11 +--
 .../Complexity/Classes/Toda/Counting.lean     |  7 --
 .../Problems/SAT/ExactOne/DrawingFits.lean    |  8 ---
 .../Problems/SAT/ExactOne/DrawingRoutes.lean  | 10 ---
 .../SAT/ExactOne/GeometryProfilesCollar.lean  | 12 ++++
 .../Problems/SAT/Planar/CrossoverLayout.lean  | 40 ++---------
 .../Problems/SAT/Planar/PairedBounds.lean     | 51 ++------------
 .../Problems/SAT/Planar/PairedCompile.lean    | 48 +++++++++++++
 .../Problems/SAT/Planar/PairedCounting.lean   |  3 +-
 .../SAT/Planar/PairedCrossoverLayout.lean     | 31 ++-------
 .../Problems/SAT/Planar/PairedGeometry.lean   | 68 ++-----------------
 .../Problems/SAT/Planar/PairedSemantics.lean  | 22 +-----
 .../Problems/SAT/Planar/PathData.lean         | 16 +++++
 .../Problems/SAT/Planar/PathGeometry.lean     | 16 -----
 .../Complexity/Problems/SAT/Planar/Paths.lean |  6 ++
 .../Complexity/Problems/TwoSAT/Layout.lean    |  6 ++
 .../Complexity/Problems/TwoSAT/Reduction.lean |  5 --
 .../Complexity/Problems/TwoSAT/Routines.lean  |  4 --
 .../Reduction/LogSpaceTruthTable.lean         |  5 +-
 .../Reduction/TruthTableVariants.lean         | 23 +------
 .../Turing/MultiTape/Internal/NormalForm.lean |  2 +-
 .../MultiTape/Internal/OPrimitives.lean       | 15 ++--
 .../BitString/InitialTestsSearch.lean         | 22 +++---
 .../Combinatorics/Expander/Basic.lean         | 30 +++++---
 .../Combinatorics/Expander/Hitting.lean       | 17 +----
 .../Combinatorics/Expander/Mixing.lean        | 19 ++----
 .../Combinatorics/Expander/Spectrum.lean      | 34 ++--------
 .../Foundations/Data/BitString/WordCount.lean | 18 +++--
 .../Foundations/Data/Finset/Expect.lean       | 17 ++++-
 Complexity/Foundations/Data/List/Filter.lean  | 25 ++++++-
 .../Foundations/Geometry/Orthogonal.lean      | 38 +++++++++++
 .../Geometry/Orthogonal/PairedPorts.lean      |  9 ---
 .../Sparsification/CountingSearch.lean        | 52 ++------------
 .../Sparsification/CountingTree.lean          |  8 ++-
 ComplexityTests/Consolidation.lean            | 17 +++++
 36 files changed, 286 insertions(+), 434 deletions(-)

diff --git a/Complexity/Computability/Circuit/Arithmetic/VP.lean b/Complexity/Computability/Circuit/Arithmetic/VP.lean
index cfc29a797c..42bbbce79a 100644
--- a/Complexity/Computability/Circuit/Arithmetic/VP.lean
+++ b/Complexity/Computability/Circuit/Arithmetic/VP.lean
@@ -250,9 +250,6 @@ theorem IsProjection.trans {P : MvPolynomial υ K} {Q : MvPolynomial σ K} {R :
   obtain ⟨ρ', rfl⟩ := hQR
   exact ⟨_, (projection_projection ρ ρ' R).symm⟩
 
-private theorem totalDegree_X_le (i : σ) : (X i : MvPolynomial σ K).totalDegree ≤ 1 :=
-  (totalDegree_monomial_le _ _).trans (by simp)
-
 /-- Substituting polynomials of degree at most one does not raise the degree. -/
 private theorem totalDegree_aeval_le {g : τ → MvPolynomial σ K}
     (hg : ∀ i, (g i).totalDegree ≤ 1) (P : MvPolynomial τ K) :
@@ -272,7 +269,7 @@ theorem totalDegree_projection_le (ρ : τ → σ ⊕ K) (P : MvPolynomial τ K)
     (projection ρ P).totalDegree ≤ P.totalDegree :=
   totalDegree_aeval_le (fun i => by
     rcases ρ i with k | a
-    · exact totalDegree_X_le k
+    · exact (totalDegree_monomial_le _ _).trans (by simp)
     · simp) P
 
 end Projection
diff --git a/Complexity/Computability/Complexity/Classes/ArthurMerlin/SetLowerBound.lean b/Complexity/Computability/Complexity/Classes/ArthurMerlin/SetLowerBound.lean
index 1d6e7b2060..136cf9c283 100644
--- a/Complexity/Computability/Complexity/Classes/ArthurMerlin/SetLowerBound.lean
+++ b/Complexity/Computability/Complexity/Classes/ArthurMerlin/SetLowerBound.lean
@@ -93,15 +93,6 @@ def certifiedSet (enc : α ↪ List Bool) (N c : Polynomial ℕ) (R : α × List
 
 namespace SetLowerBound
 
-/-! ### Bit-string helpers -/
-
-/-- A string has no bit `true` exactly when it is zero. -/
-private theorem not_any_ofFn_eq_true_iff {k : ℕ} (v : BitString k) :
-    (!(List.ofFn v).any fun b => b) = true ↔ v = 0 := by
-  simp only [Bool.not_eq_eq_eq_not, Bool.not_true, List.any_eq_false, List.mem_ofFn,
-    forall_exists_index, forall_apply_eq_imp_iff, Bool.not_eq_true]
-  exact ⟨fun h => funext h, fun h i => by rw [h]; rfl⟩
-
 /-! ### Amplification and normalisation -/
 
 /-- Five elements of `S`, followed by `T` bits whose first `ℓ` bits are `false`. -/
@@ -207,7 +198,7 @@ private theorem verifier_ofFn_append {N c m T : Polynomial ℕ} {ℓ : α → 
     rw [BitString.LinearHash.wordHash_eq_ofFn, List.ofFn_add, BitString.ofList_ofFn_append]
     rfl
   rw [hdrop, hdrop', htake, List.take_left' List.length_ofFn, hhash, hoffset,
-    ← BitString.ofFn_add, not_any_ofFn_eq_true_iff, and_assoc]
+    ← BitString.ofFn_add, BitString.not_any_ofFn_eq_true_iff, and_assoc]
   refine and_congr ⟨fun h i => ?_, fun h i hi => ?_⟩ Iff.rfl
   · have := h i i.2
     rwa [BitString.listRow_eq_ofFn (count := 5) _ i, BitString.listRow_eq_ofFn (count := 5) _ i,
diff --git a/Complexity/Computability/Complexity/Classes/Toda/Counting.lean b/Complexity/Computability/Complexity/Classes/Toda/Counting.lean
index 73f763df24..b751f9b5a0 100644
--- a/Complexity/Computability/Complexity/Classes/Toda/Counting.lean
+++ b/Complexity/Computability/Complexity/Classes/Toda/Counting.lean
@@ -159,13 +159,6 @@ theorem computableInPolyTime_subsetTest {γ : Type} {input : γ ↪ List Bool}
   unfold subsetTest
   fun_prop
 
-/-- A bit string `z` has no `true` bits in `List.ofFn z` if and only if `z = 0`. -/
-private theorem not_any_ofFn_eq_true_iff {Z : ℕ} (z : Fin Z → Bool) :
-    (!(List.ofFn z).any fun b => b) = true ↔ z = 0 := by
-  simp only [Bool.not_eq_eq_eq_not, Bool.not_true, List.any_eq_false, List.mem_ofFn,
-    forall_exists_index, forall_apply_eq_imp_iff, Bool.not_eq_true]
-  exact ⟨fun h => funext h, fun h i => congrFun h i⟩
-
 /-- The block-level predicate corresponding to `subsetTest`: the first `k` blocks are accepted and
 strictly increasing in lexicographic order, and the remaining blocks are zero. -/
 private def SubsetBlockPred (acc : List Bool → Bool) {K Z k : ℕ} (hk : k ≤ K)
diff --git a/Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingFits.lean b/Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingFits.lean
index f889db0f61..bedcb3fdd9 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingFits.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingFits.lean
@@ -117,14 +117,6 @@ private theorem local_clause_bounds (p : ClauseProfile) (s : PortAssignment) (i
   obtain ⟨a, ha, rfl⟩ := List.mem_map.mp hq
   exact collarPoint_bounds _ (prefix_clause_bounds p a ha)
 
-private theorem collarRoute_points_bounds (reflected : Bool) {r : Route}
-    (hr : ∀ q ∈ r, Rect 180000 180000 q) :
-    ∀ q ∈ collarRoute reflected r, Rect 540000 540000 q := by
-  intro q hq
-  rw [collarRoute_eq_map] at hq
-  obtain ⟨a, ha, rfl⟩ := List.mem_map.mp hq
-  exact collarPoint_bounds _ (hr a ha)
-
 private theorem local_route_bounds (p : ClauseProfile) (s : PortAssignment)
     {e : LocalIncidence}
     (he : e ∈ (collaredPrefixGeometry (profilePrefixGeometry p) s).incidenceRoutes) :
diff --git a/Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingRoutes.lean b/Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingRoutes.lean
index d0c2ba543a..36cc95abc1 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingRoutes.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingRoutes.lean
@@ -42,16 +42,6 @@ namespace Cslib.Complexity.SAT.ExactOne
 
 open Cslib.Logic.PL Orthogonal
 
-private theorem collarRoute_points_bounds (reflected : Bool) {r : Route}
-    (hr : ∀ q ∈ r, 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000) :
-    ∀ q ∈ collarRoute reflected r,
-      0 ≤ q.1 ∧ q.1 ≤ 540000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 540000 := by
-  intro q hq
-  rw [collarRoute_eq_map] at hq
-  obtain ⟨a, ha, rfl⟩ := List.mem_map.mp hq
-  have hb := hr a ha
-  cases reflected <;> dsimp [collarPoint, collarOffset, mirrorPoint] <;> omega
-
 private theorem collarPrefixRoute_points_bounds {s : PortAssignment} (hs : s.Distinct)
     (i : Fin 3) {r : Route}
     (hr : ∀ q ∈ r, 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000) :
diff --git a/Complexity/Computability/Complexity/Problems/SAT/ExactOne/GeometryProfilesCollar.lean b/Complexity/Computability/Complexity/Problems/SAT/ExactOne/GeometryProfilesCollar.lean
index 14dd62f893..31db280503 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/ExactOne/GeometryProfilesCollar.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/ExactOne/GeometryProfilesCollar.lean
@@ -345,4 +345,16 @@ theorem profileCollarRoute_outer_boundary_contact (p : ClauseProfile)
       (collarRoute_in_innerBox _ (profile_prefix_incidence_bounds p h he) hz)
     exact False.elim (List.not_mem_nil hq)
 
+/-- If every point of a route lies in the `180000`-by-`180000` inner square, then every point of
+its collared route lies in the `540000`-by-`540000` outer square. -/
+theorem collarRoute_points_bounds (reflected : Bool) {r : Route}
+    (hr : ∀ q ∈ r, 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000) :
+    ∀ q ∈ collarRoute reflected r,
+      0 ≤ q.1 ∧ q.1 ≤ 540000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 540000 := by
+  intro q hq
+  rw [collarRoute_eq_map] at hq
+  obtain ⟨a, ha, rfl⟩ := List.mem_map.mp hq
+  have hb := hr a ha
+  cases reflected <;> dsimp [collarPoint, collarOffset, mirrorPoint] <;> omega
+
 end Cslib.Complexity.SAT.ExactOne
diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/CrossoverLayout.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/CrossoverLayout.lean
index 3563e62fdb..c109e89345 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/Planar/CrossoverLayout.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/CrossoverLayout.lean
@@ -50,37 +50,14 @@ namespace Cslib.Logic.PL.CNF.Crossover
 
 open Orthogonal
 
-private theorem support_bounds_of_points {r : Route}
-    (h : ∀ q ∈ r, 20 ≤ q.1 ∧ q.1 ≤ 220 ∧ 20 ≤ q.2 ∧ q.2 ≤ 220)
-    {p : ℝ × ℝ} (hp : p ∈ support r) :
-    20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220 := by
-  have cast_bounds (q : Point) (hq : q ∈ r) :
-      (20 : ℝ) ≤ q.1 ∧ (q.1 : ℝ) ≤ 220 ∧ 20 ≤ (q.2 : ℝ) ∧ (q.2 : ℝ) ≤ 220 := by
-    exact_mod_cast h q hq
-  rcases hp with ⟨q, hq, rfl⟩ | ⟨e, he, hp⟩
-  · exact cast_bounds q hq
-  · have he' := List.of_mem_zip he
-    have ha := cast_bounds e.1 he'.1
-    have hb := cast_bounds e.2 (List.mem_of_mem_tail he'.2)
-    obtain ⟨hx, hy⟩ := mem_segment_bounds hp
-    rw [Set.mem_uIcc] at hx hy
-    have hx' : 20 ≤ p.1 ∧ p.1 ≤ 220 := by
-      rcases hx with hx | hx <;> constructor <;> linarith [ha.1, ha.2.1, hb.1, hb.2.1]
-    have hy' : 20 ≤ p.2 ∧ p.2 ≤ 220 := by
-      rcases hy with hy | hy <;> constructor <;>
-        linarith [ha.2.2.1, ha.2.2.2, hb.2.2.1, hb.2.2.2]
-    exact ⟨hx'.1, hx'.2, hy'.1, hy'.2⟩
-
 /-- Every real point of the core drawing is strictly inside the outer 240-by-240 box. -/
 theorem core_support_interior {e : ℕ × SplitVariable × Route} (he : e ∈ incidenceRoutes)
     {p : ℝ × ℝ} (hp : p ∈ support e.2.2) :
     0 < p.1 ∧ p.1 < 240 ∧ 0 < p.2 ∧ p.2 < 240 := by
-  have h := support_bounds_of_points (core_bounds e he) hp
-  constructor
-  · linarith [h.1]
-  constructor
-  · linarith [h.2.1]
-  constructor <;> linarith [h.2.2.1, h.2.2.2]
+  have h := support_bounds_of_points (x₀ := 20) (x₁ := 220) (y₀ := 20) (y₁ := 220)
+    (core_bounds e he) hp
+  norm_num at h
+  exact ⟨by linarith [h.1], by linarith [h.2.1], by linarith [h.2.2.1], by linarith [h.2.2.2]⟩
 
 /-- Distinct segments of a route intersect only at their consecutive shared bend. -/
 theorem incidence_simple {e : ℕ × SplitVariable × Route} (he : e ∈ incidenceRoutes)
@@ -197,15 +174,6 @@ theorem access_contact {i : Fin 4} {e : ℕ × SplitVariable × Route}
     exact ⟨h, hq' ▸ hpq⟩
   · exact False.elim (List.not_mem_nil hq)
 
-private theorem mem_support_pair {a b : Point} {p : ℝ × ℝ} :
-    p ∈ support [a, b] ↔ p ∈ segment a b := by
-  rw [support_cons_cons]
-  change (p ∈ segment a b ∨ p ∈ support [b]) ↔ _
-  have hright : realPoint b ∈ segment a b := _root_.right_mem_segment ℝ _ _
-  have hs : p ∈ support [b] ↔ p = realPoint b := by simp [support, List.consecutivePairs]
-  rw [hs]
-  exact ⟨fun h => h.elim id (fun h => h ▸ hright), Or.inl⟩
-
 /-- Every point of an access route lies in the outer box. Its only boundary point is the
 prescribed geometric access port; all other access points are strictly inside. -/
 theorem access_boundary_isolation {i : Fin 4} {p : ℝ × ℝ}
diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedBounds.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedBounds.lean
index 3bda2d4237..46b17422ab 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedBounds.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedBounds.lean
@@ -82,14 +82,8 @@ private theorem cellBound_path {φ : CNF ℕ} {r : Route} (hr : r ∈ paths φ)
 
 private theorem cellBound_occurrencePath {φ : CNF ℕ} {o : Occurrence ℕ}
     (ho : o ∈ Cslib.Logic.PL.occurrences φ) {p : Point} (hp : p ∈ occurrencePath φ o) :
-    CellBound φ p := by
-  have hi : (Cslib.Logic.PL.occurrences φ).idxOf o < (paths φ).length := by
-    rw [PlanarCompile.paths_length, ← Cslib.Logic.PL.length_occurrences]
-    exact List.idxOf_lt_length_of_mem ho
-  apply cellBound_path (r := occurrencePath φ o) _ hp
-  change (paths φ).getD ((Cslib.Logic.PL.occurrences φ).idxOf o) [] ∈ paths φ
-  rw [List.getD_eq_getElem _ _ hi]
-  exact List.getElem_mem hi
+    CellBound φ p :=
+  cellBound_path (PlanarCompile.occurrencePath_mem_paths ho) hp
 
 private theorem cellBound_crossing {φ : CNF ℕ} {p : Point} (hp : p ∈ crossingSites φ) :
     CellBound φ p := by
@@ -270,9 +264,7 @@ private theorem link_bounds {φ : CNF ℕ} (sites : List Point) (lane : Fin 2) {
 
 private theorem cellBound_ordinary {φ : CNF ℕ} {p : Point} (hp : p ∈ ordinaryCells φ) :
     CellBound φ p := by
-  have hmem : p ∈ (paths φ).flatMap List.dropLast ∧ p ∉ crossingSites φ := by
-    simpa [ordinaryCells, mem_selectDistinct_replicate] using hp
-  obtain ⟨r, hr, hp⟩ := List.mem_flatMap.mp hmem.1
+  obtain ⟨⟨r, hr, hp⟩, -⟩ := (mem_ordinaryCells φ p).1 hp
   exact cellBound_path hr ((List.dropLast_subset _) hp)
 
 private theorem placedClauses_bounds (φ : CNF ℕ) :
@@ -333,41 +325,6 @@ theorem positions_length_le (φ : CNF ℕ) :
   rw [length_vars_rawFormula, ← length_vars_formula] at hv
   omega
 
-private theorem cost_signal_position (sites : List Point) (p q : Point) (l : Fin 2) :
-    variablePosition (signal sites p q l) =
-      cellOrigin 120 p + PairedPorts.variablePosition (side p q) l := by
-  simp only [signal, port, variablePosition]
-  split_ifs <;> rfl
-
-/-- Actual accesses are translations of the fixed paired-port accesses. -/
-private theorem cost_access_eq_translate (sites : List Point) (p q : Point) (l : Fin 2) :
-    access sites p q l = translate (cellOrigin 120 p) (PairedPorts.accessRoute (side p q) l) := by
-  rw [access, cost_signal_position]
-  simp only [boundary, PairedPorts.accessRoute, translate, List.map_cons, List.map_nil]
-  simp only [add_comm]
-
-private def finalLocalRoute (s : Fin 4) : Route :=
-  [(120, 120), PairedPorts.spokeElbow s, PairedPorts.boundaryPort s (PairedPorts.spokeLane s),
-    cellOrigin 120 (PairedPorts.neighbor s) +
-      PairedPorts.variablePosition (PairedPorts.oppositeSide s) (PairedPorts.spokeLane s)]
-
-private theorem finalRoute_eq_translate (sites : List Point) {p q : Point}
-    (h : Orthogonal.length p q = 1) :
-    [center q, cellOrigin 120 q + PairedPorts.spokeElbow (side q p),
-      boundary q (side q p) (PairedPorts.spokeLane (side q p)),
-      variablePosition (signal sites p q (PairedPorts.spokeLane (side q p)))] =
-      translate (cellOrigin 120 q) (finalLocalRoute (side q p)) := by
-  rw [cost_signal_position]
-  have hrev : Orthogonal.length q p = 1 := by
-    simp only [Orthogonal.length] at h ⊢
-    omega
-  rcases q with ⟨x, y⟩
-  rcases PlanarCompile.unit_neighbor_cases hrev with rfl | rfl | rfl | rfl <;>
-    simp [translate, finalLocalRoute, side, PlanarCompile.side, center, PlanarCompile.center,
-      boundary, cellOrigin, PairedPorts.neighbor, PairedPorts.oppositeSide,
-      PairedPorts.variablePosition, PairedPorts.boundaryPort, PairedPorts.spokeLane,
-      PairedPorts.spokeElbow, PairedPorts.offset, Prod.ext_iff] <;> omega
-
 private theorem original_route_count (φ : CNF ℕ) (sites : List Point) :
     ((originalClauses φ sites).map fun c => c.2.2.length).sum = φ.vars.length := by
   rw [CNF.length_vars]
@@ -452,7 +409,7 @@ private theorem crossing_route_costs (p : Point) :
 
 private theorem access_wire_cost (sites : List Point) (p q : Point) (lane : Fin 2) :
     wireLength (access sites p q lane) = 20 := by
-  rw [cost_access_eq_translate, wireLength_translate]
+  rw [access_eq_translate, wireLength_translate]
   exact (PairedPorts.access_route_sizes _ _).2
 
 private theorem lastLiteral_wire_cost (sites : List Point) (r : Route) (b : Bool)
diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCompile.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCompile.lean
index 84ab9effa3..830fa1e085 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCompile.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCompile.lean
@@ -155,4 +155,52 @@ def positions (φ : CNF ℕ) : List Point :=
 /-- Incidence routes ordered by clauses and by literal positions. -/
 def routes (φ : CNF ℕ) : List Route := (placedClauses φ).flatMap fun c => c.2.2
 
+/-- A point receives an ordinary ring exactly when a retained path uses it outside a crossing. -/
+theorem mem_ordinaryCells (φ : CNF ℕ) (p : Point) :
+    p ∈ ordinaryCells φ ↔
+      (∃ r ∈ paths φ, p ∈ r.dropLast) ∧ p ∉ crossingSites φ := by
+  simp [ordinaryCells, mem_selectDistinct_replicate, List.mem_flatMap]
+
+/-- No ordinary ring is emitted twice. -/
+theorem ordinaryCells_nodup (φ : CNF ℕ) : (ordinaryCells φ).Nodup :=
+  nodup_selectDistinct _ _
+
+/-- The compiler's presented signal always has the shared inner access position. -/
+theorem signal_position (sites : List Point) (p q : Point) (l : Fin 2) :
+    variablePosition (signal sites p q l) =
+      cellOrigin 120 p + PairedPorts.variablePosition (side p q) l := by
+  simp only [signal, port, variablePosition]
+  split_ifs <;> rfl
+
+/-- Actual accesses are translations of the fixed paired-port accesses. -/
+theorem access_eq_translate (sites : List Point) (p q : Point) (l : Fin 2) :
+    access sites p q l = translate (cellOrigin 120 p) (PairedPorts.accessRoute (side p q) l) := by
+  rw [access, signal_position]
+  simp only [boundary, PairedPorts.accessRoute, translate, List.map_cons, List.map_nil]
+  simp only [add_comm]
+
+/-- Local template of the final incidence route inside a clause cell. -/
+def finalLocalRoute (s : Fin 4) : Route :=
+  [(120, 120), PairedPorts.spokeElbow s, PairedPorts.boundaryPort s (PairedPorts.spokeLane s),
+    cellOrigin 120 (PairedPorts.neighbor s) +
+      PairedPorts.variablePosition (PairedPorts.oppositeSide s) (PairedPorts.spokeLane s)]
+
+/-- Actual final literal routes are translations of `finalLocalRoute`. -/
+theorem finalRoute_eq_translate (sites : List Point) {p q : Point}
+    (h : Orthogonal.length p q = 1) :
+    [center q, cellOrigin 120 q + PairedPorts.spokeElbow (side q p),
+      boundary q (side q p) (PairedPorts.spokeLane (side q p)),
+      variablePosition (signal sites p q (PairedPorts.spokeLane (side q p)))] =
+      translate (cellOrigin 120 q) (finalLocalRoute (side q p)) := by
+  rw [signal_position]
+  have hrev : Orthogonal.length q p = 1 := by
+    simp only [Orthogonal.length] at h ⊢
+    omega
+  rcases q with ⟨x, y⟩
+  rcases PlanarCompile.unit_neighbor_cases hrev with rfl | rfl | rfl | rfl <;>
+    simp [translate, finalLocalRoute, side, PlanarCompile.side, center, PlanarCompile.center,
+      boundary, cellOrigin, PairedPorts.neighbor, PairedPorts.oppositeSide,
+      PairedPorts.variablePosition, PairedPorts.boundaryPort, PairedPorts.spokeLane,
+      PairedPorts.spokeElbow, PairedPorts.offset, Prod.ext_iff] <;> omega
+
 end Cslib.Complexity.SAT.ParsimoniousPlanar
diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCounting.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCounting.lean
index 4165529768..08f80e2dea 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCounting.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCounting.lean
@@ -64,7 +64,8 @@ theorem source_cell_mem_ordinary {φ : CNF ℕ} {v : ℕ} (hv : v ∈ φ.vars) :
     rw [← List.getElem_dropLast hi]
     exact List.getElem_mem _
   exact (mem_ordinaryCells φ _).2
-    ⟨⟨_, occurrencePath_mem_paths ho, hret⟩, PlanarCompile.source_center_not_crossing ho⟩
+    ⟨⟨_, PlanarCompile.occurrencePath_mem_paths ho, hret⟩,
+      PlanarCompile.source_center_not_crossing ho⟩
 
 /-- Every used source representative is an occurring variable of the actual raw output. -/
 theorem sourceVariable_mem_rawFormula {φ : CNF ℕ} {v : ℕ} (hv : v ∈ φ.vars) :
diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayout.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayout.lean
index 2b111bc70d..e04d9a8f19 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayout.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayout.lean
@@ -48,37 +48,14 @@ namespace Cslib.Logic.PL.CNF.PairedCrossover
 
 open Orthogonal
 
-private theorem support_bounds_of_points {r : Route}
-    (h : ∀ q ∈ r, 20 ≤ q.1 ∧ q.1 ≤ 220 ∧ 20 ≤ q.2 ∧ q.2 ≤ 220)
-    {p : ℝ × ℝ} (hp : p ∈ support r) :
-    20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220 := by
-  have cast_bounds (q : Point) (hq : q ∈ r) :
-      (20 : ℝ) ≤ q.1 ∧ (q.1 : ℝ) ≤ 220 ∧ 20 ≤ (q.2 : ℝ) ∧ (q.2 : ℝ) ≤ 220 := by
-    exact_mod_cast h q hq
-  rcases hp with ⟨q, hq, rfl⟩ | ⟨e, he, hp⟩
-  · exact cast_bounds q hq
-  · have he' := List.of_mem_zip he
-    have ha := cast_bounds e.1 he'.1
-    have hb := cast_bounds e.2 (List.mem_of_mem_tail he'.2)
-    obtain ⟨hx, hy⟩ := mem_segment_bounds hp
-    rw [Set.mem_uIcc] at hx hy
-    have hx' : 20 ≤ p.1 ∧ p.1 ≤ 220 := by
-      rcases hx with hx | hx <;> constructor <;> linarith [ha.1, ha.2.1, hb.1, hb.2.1]
-    have hy' : 20 ≤ p.2 ∧ p.2 ≤ 220 := by
-      rcases hy with hy | hy <;> constructor <;>
-        linarith [ha.2.2.1, ha.2.2.2, hb.2.2.1, hb.2.2.2]
-    exact ⟨hx'.1, hx'.2, hy'.1, hy'.2⟩
-
 /-- Every real point of the core drawing is strictly inside the outer 240-by-240 box. -/
 theorem core_support_interior {e : ℕ × Variable × Route} (he : e ∈ incidenceRoutes)
     {p : ℝ × ℝ} (hp : p ∈ support e.2.2) :
     0 < p.1 ∧ p.1 < 240 ∧ 0 < p.2 ∧ p.2 < 240 := by
-  have h := support_bounds_of_points (core_bounds e he) hp
-  constructor
-  · linarith [h.1]
-  constructor
-  · linarith [h.2.1]
-  constructor <;> linarith [h.2.2.1, h.2.2.2]
+  have h := support_bounds_of_points (x₀ := 20) (x₁ := 220) (y₀ := 20) (y₁ := 220)
+    (core_bounds e he) hp
+  norm_num at h
+  exact ⟨by linarith [h.1], by linarith [h.2.1], by linarith [h.2.2.1], by linarith [h.2.2.2]⟩
 
 /-- Distinct segments of a route intersect only at their consecutive shared bend. -/
 theorem incidence_simple {e : ℕ × Variable × Route} (he : e ∈ incidenceRoutes)
diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedGeometry.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedGeometry.lean
index 131a7fe7da..4b9e68d67e 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedGeometry.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedGeometry.lean
@@ -63,20 +63,6 @@ theorem shared_boundary {p q : Point} (h : Orthogonal.length p q = 1) (l : Fin 2
     ext <;> norm_num [boundary, side, PlanarCompile.side, cellOrigin, PairedPorts.boundaryPort,
       PairedPorts.offset] <;> omega
 
-/-- The compiler's presented signal always has the shared inner access position. -/
-theorem signal_position (sites : List Point) (p q : Point) (l : Fin 2) :
-    variablePosition (signal sites p q l) =
-      cellOrigin 120 p + PairedPorts.variablePosition (side p q) l := by
-  simp only [signal, port, variablePosition]
-  split_ifs <;> rfl
-
-/-- Actual accesses are translations of the fixed paired-port accesses. -/
-theorem access_eq_translate (sites : List Point) (p q : Point) (l : Fin 2) :
-    access sites p q l = translate (cellOrigin 120 p) (PairedPorts.accessRoute (side p q) l) := by
-  rw [access, signal_position]
-  simp only [boundary, PairedPorts.accessRoute, translate, List.map_cons, List.map_nil]
-  simp only [add_comm]
-
 /-- Every actual access is proper and orthogonal. -/
 theorem access_orthogonal (sites : List Point) (p q : Point) (l : Fin 2) :
     IsOrthogonal (access sites p q l) := by
@@ -222,30 +208,16 @@ theorem pathBoundaries_nodup {φ : CNF ℕ}
       exact hmid (boundary_step_midpoint_eq (path_step_unit he) (path_step_unit hf) hy).2
   simpa only [steps, List.flatMap_assoc] using hn'
 
-/-- The actual ordinary-cell list has no repetitions. -/
-private theorem ordinaryCells_nodup (φ : CNF ℕ) : (ordinaryCells φ).Nodup :=
-  nodup_selectDistinct _ _
-
-/-- Ordinary tiles are emitted exactly at retained occupied cells outside crossing sites. -/
-private theorem mem_ordinaryCells (φ : CNF ℕ) (p : Point) :
-    p ∈ ordinaryCells φ ↔ p ∈ (paths φ).flatMap List.dropLast ∧ p ∉ crossingSites φ := by
-  simp [ordinaryCells, mem_selectDistinct_replicate]
-
 /-- Every original clause cell is disjoint from all ordinary tiles. -/
 theorem clause_cell_not_ordinary {φ : CNF ℕ} {i : ℕ} (hi : i < φ.length) :
     Layout.center (φ.distinctVars.length + i) ∉ ordinaryCells φ := by
   intro hp
-  obtain ⟨r, hr, hp⟩ := List.mem_flatMap.mp ((mem_ordinaryCells φ _).1 hp).1
+  obtain ⟨⟨r, hr, hp⟩, -⟩ := (mem_ordinaryCells φ _).1 hp
   change r ∈ PlanarCompile.paths φ at hr
   rw [← PlanarCompile.occurrencePaths_eq_paths φ] at hr
   obtain ⟨o, ho, rfl⟩ := List.mem_map.mp hr
   exact PlanarCompile.clause_cell_not_mem_path_dropLast ho hi hp
 
-private def finalLocalRoute (s : Fin 4) : Route :=
-  [(120, 120), PairedPorts.spokeElbow s, PairedPorts.boundaryPort s (PairedPorts.spokeLane s),
-    cellOrigin 120 (PairedPorts.neighbor s) +
-      PairedPorts.variablePosition (PairedPorts.oppositeSide s) (PairedPorts.spokeLane s)]
-
 private theorem finalLocalRoute_orthogonal : ∀ s, IsOrthogonal (finalLocalRoute s) := by
   decide +kernel
 
@@ -270,23 +242,6 @@ private theorem finalLocalRoute_simple (s : Fin 4) : IsSimple (finalLocalRoute s
     exact ⟨Or.inl hpq, Or.inr (hpq.trans (congrArg realPoint h'.symm))⟩
   · exact False.elim (List.not_mem_nil hq)
 
-private theorem finalRoute_eq_translate (sites : List Point) {p q : Point}
-    (h : Orthogonal.length p q = 1) :
-    [center q, cellOrigin 120 q + PairedPorts.spokeElbow (side q p),
-      boundary q (side q p) (PairedPorts.spokeLane (side q p)),
-      variablePosition (signal sites p q (PairedPorts.spokeLane (side q p)))] =
-      translate (cellOrigin 120 q) (finalLocalRoute (side q p)) := by
-  rw [signal_position]
-  have hrev : Orthogonal.length q p = 1 := by
-    simp only [Orthogonal.length] at h ⊢
-    omega
-  rcases q with ⟨x, y⟩
-  rcases PlanarCompile.unit_neighbor_cases hrev with rfl | rfl | rfl | rfl <;>
-    norm_num [translate, finalLocalRoute, side, PlanarCompile.side, center, PlanarCompile.center,
-      boundary, cellOrigin, PairedPorts.neighbor, PairedPorts.oppositeSide,
-      PairedPorts.variablePosition, PairedPorts.boundaryPort, PairedPorts.spokeLane,
-      PairedPorts.spokeElbow, PairedPorts.offset, Prod.ext_iff] <;> omega
-
 /-- Every actual final literal route is proper, orthogonal and continuously simple. -/
 theorem lastLiteral_route_regular (sites : List Point) (r : Route) (b : Bool)
     (h : Orthogonal.length (r.getD (r.length - 2) (0, 0)) (r.getLastD (0, 0)) = 1) :
@@ -677,15 +632,6 @@ theorem placedClause_endpoints (φ : CNF ℕ) {pc : PlacedClause} (hpc : pc ∈
     rcases hpc with rfl | rfl <;>
       exact link_endpoints _ (PlanarCompile.occurrencePath_unit ho he') _ hlr
 
-private theorem support_pair (a b : Point) : support [a, b] = segment a b := by
-  ext p
-  rw [support_cons_cons]
-  change (p ∈ segment a b ∨ p ∈ support [b]) ↔ _
-  have hright : realPoint b ∈ segment a b := _root_.right_mem_segment ℝ _ _
-  have hs : p ∈ support [b] ↔ p = realPoint b := by simp [support, List.consecutivePairs]
-  rw [hs]
-  exact ⟨fun h => h.elim id (fun h => h ▸ hright), Or.inl⟩
-
 private theorem support_four (a b c d : Point) :
     support [a, b, c, d] = support [a, b, c] ∪ support [c, d] := by
   have hl : support [a, b, c, d] = segment a b ∪ (segment b c ∪ segment c d) := by
@@ -873,12 +819,6 @@ theorem routes_endpoints (φ : CNF ℕ) {i : ℕ}
   have h := (raw_routes_endpoints φ).get hi hir
   simpa only [List.get_eq_getElem, List.getD_eq_getElem _ _ hir] using h
 
-private theorem occurrencePath_mem_paths {φ : CNF ℕ} {o : Occurrence ℕ}
-    (ho : o ∈ Cslib.Logic.PL.occurrences φ) : occurrencePath φ o ∈ paths φ := by
-  change occurrencePath φ o ∈ PlanarCompile.paths φ
-  rw [← PlanarCompile.occurrencePaths_eq_paths φ]
-  exact List.mem_map_of_mem ho
-
 private theorem penultimate_mem_dropLast {r : Route} (h : 2 ≤ r.length) :
     r.getD (r.length - 2) (0, 0) ∈ r.dropLast := by
   have hk : r.length - 2 < r.dropLast.length := by simp only [List.length_dropLast]; omega
@@ -902,14 +842,14 @@ theorem raw_variable_cell_membership (φ : CNF ℕ) {v : Variable}
     have heq' := congrArg Prod.fst heq
     dsimp only [lastLiteral] at heq'
     subst v
-    exact Or.inr ⟨_, occurrencePath_mem_paths ho,
+    exact Or.inr ⟨_, PlanarCompile.occurrencePath_mem_paths ho,
       penultimate_mem_dropLast (PlanarCompile.occurrencePath_length_ge_two ho)⟩
   · obtain ⟨ci, _, rfl⟩ := List.mem_map.mp hpc
     obtain ⟨l, _, heq⟩ := List.mem_map.mp hv
     have heq' := congrArg Prod.fst heq
     change (p, Sum.inl l.1) = v at heq'
     subst v
-    exact Or.inr (List.mem_flatMap.mp ((mem_ordinaryCells φ p).1 hp).1)
+    exact Or.inr ((mem_ordinaryCells φ p).1 hp).1
   · obtain ⟨ci, _, rfl⟩ := List.mem_map.mp hpc
     obtain ⟨l, _, heq⟩ := List.mem_map.mp hv
     have heq' := congrArg Prod.fst heq
@@ -923,7 +863,7 @@ theorem raw_variable_cell_membership (φ : CNF ℕ) {v : Variable}
       rcases link_literal_cases _ _ _ _ hv with heq | heq <;> dsimp only at heq <;> subst v
     all_goals
       apply Or.inr
-      refine ⟨_, occurrencePath_mem_paths ho, ?_⟩
+      refine ⟨_, PlanarCompile.occurrencePath_mem_paths ho, ?_⟩
       first | exact hpair.1 | exact List.mem_of_mem_tail hpair.2
 
 /-- No actual variable is placed in an original clause cell. -/
diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedSemantics.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedSemantics.lean
index 5b766bf8bf..1b6655ccc4 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedSemantics.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedSemantics.lean
@@ -46,16 +46,6 @@ def wire (sites : List Point) (r : Route) : List (PairedWire.Cell Variable) :=
   r.dropLast.zipIdx.map fun (p, i) lane =>
     (signal sites p (r.getD (i - 1) p) lane, signal sites p (r.getD (i + 1) p) lane)
 
-/-- A point receives an ordinary ring exactly when a retained path uses it outside a crossing. -/
-theorem mem_ordinaryCells (φ : CNF ℕ) (p : Point) :
-    p ∈ ordinaryCells φ ↔
-      (∃ r ∈ paths φ, p ∈ r.dropLast) ∧ p ∉ crossingSites φ := by
-  simp [ordinaryCells, mem_selectDistinct_replicate, List.mem_flatMap]
-
-/-- No ordinary ring is emitted twice. -/
-theorem ordinaryCells_nodup (φ : CNF ℕ) : (ordinaryCells φ).Nodup :=
-  nodup_selectDistinct _ _
-
 /-- The two local clause tables retain their exact formulas under variable tagging. -/
 theorem map_fst_ordinaryClauses (p : Point) :
     (ordinaryClauses p).map Prod.fst =
@@ -123,13 +113,6 @@ theorem getElem_wire (sites : List Point) (r : Route) (i : ℕ) (hi : i < r.leng
         signal sites r[i] (r.getD (i + 1) r[i]) lane) := by
   simp only [wire, List.getElem_map, List.getElem_zipIdx, Nat.zero_add, List.getElem_dropLast]
 
-/-- An actual occurrence selects a member of the canonical path list. -/
-theorem occurrencePath_mem_paths {φ : CNF ℕ} {o : Occurrence ℕ}
-    (ho : o ∈ Cslib.Logic.PL.occurrences φ) : occurrencePath φ o ∈ paths φ := by
-  change PlanarCompile.occurrencePath φ o ∈ PlanarCompile.paths φ
-  rw [← PlanarCompile.occurrencePaths_eq_paths]
-  exact List.mem_map_of_mem ho
-
 /-- The side lookup recovers each cardinal neighbor's side. -/
 theorem side_neighbor (p : Point) (s : Fin 4) :
     side p (p + PairedPorts.neighbor s) = s := by
@@ -182,7 +165,7 @@ theorem wire_cells_agree {φ : CNF ℕ}
         rw [crossing_port_value h hp, crossing_port_value h hp, crossing_port_value h hp]
         simp
   · have hord : p ∈ ordinaryCells φ :=
-      (mem_ordinaryCells φ p).2 ⟨⟨_, occurrencePath_mem_paths ho, hpod⟩, hp⟩
+      (mem_ordinaryCells φ p).2 ⟨⟨_, PlanarCompile.occurrencePath_mem_paths ho, hpod⟩, hp⟩
     intro lane
     change σ (signal _ _ _ lane) = σ (signal _ _ _ 0) ∧
       σ (signal _ _ _ lane) = σ (signal _ _ _ 0)
@@ -256,7 +239,8 @@ theorem wire_first_value {φ : CNF ℕ} {σ : Variable → Bool}
     rw [← List.getElem_dropLast hdrop]
     exact List.getElem_mem _
   have hord := (mem_ordinaryCells φ _).2
-    ⟨⟨_, occurrencePath_mem_paths ho, hret⟩, PlanarCompile.source_center_not_crossing ho⟩
+    ⟨⟨_, PlanarCompile.occurrencePath_mem_paths ho, hret⟩,
+      PlanarCompile.source_center_not_crossing ho⟩
   rw [hhead, getElem_wire _ _ 0 (by omega)]
   simp only [Nat.zero_sub]
   rw [List.getD_eq_getElem _ _ (by omega), hp']
diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PathData.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PathData.lean
index f08b7f2798..02e7b77e9a 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/Planar/PathData.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PathData.lean
@@ -80,4 +80,20 @@ def side (p q : Point) : Fin 4 :=
 /-- The center of a square of side 240 indexed by an integer grid point. -/
 def center (p : Point) : Point := cellOrigin 120 p + (120, 120)
 
+/-- Unit-adjacent integer cells differ by exactly one of the four cardinal displacements. -/
+theorem unit_neighbor_cases {p q : Point} (h : Orthogonal.length p q = 1) :
+    q = p + (-1, 0) ∨ q = p + (1, 0) ∨ q = p + (0, -1) ∨ q = p + (0, 1) := by
+  rcases p with ⟨px, py⟩
+  rcases q with ⟨qx, qy⟩
+  simp only [Orthogonal.length] at h
+  simp only [Prod.mk_add_mk, Prod.mk.injEq]
+  omega
+
+/-- Neighboring unit cells use exactly the same geometric midpoint for their shared port. -/
+theorem shared_cellPort {p q : Point} (h : Orthogonal.length p q = 1) :
+    cellPort 120 p (side p q) = cellPort 120 q (side q p) := by
+  rcases p with ⟨px, py⟩
+  rcases unit_neighbor_cases h with rfl | rfl | rfl | rfl <;>
+    simp [side, cellPort, cellOrigin, Prod.ext_iff] <;> omega
+
 end Cslib.Complexity.SAT.PlanarCompile
diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PathGeometry.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PathGeometry.lean
index 21e494e60f..39a9d5de7b 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/Planar/PathGeometry.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PathGeometry.lean
@@ -41,22 +41,6 @@ namespace Cslib.Complexity.SAT.PlanarCompile
 
 open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal
 
-/-- Unit-adjacent integer cells differ by exactly one of the four cardinal displacements. -/
-theorem unit_neighbor_cases {p q : Point} (h : Orthogonal.length p q = 1) :
-    q = p + (-1, 0) ∨ q = p + (1, 0) ∨ q = p + (0, -1) ∨ q = p + (0, 1) := by
-  rcases p with ⟨px, py⟩
-  rcases q with ⟨qx, qy⟩
-  simp only [Orthogonal.length] at h
-  simp only [Prod.mk_add_mk, Prod.mk.injEq]
-  omega
-
-/-- Neighboring unit cells use exactly the same geometric midpoint for their shared port. -/
-theorem shared_cellPort {p q : Point} (h : Orthogonal.length p q = 1) :
-    cellPort 120 p (side p q) = cellPort 120 q (side q p) := by
-  rcases p with ⟨px, py⟩
-  rcases unit_neighbor_cases h with rfl | rfl | rfl | rfl <;>
-    norm_num [side, cellPort, cellOrigin, Prod.ext_iff] <;> omega
-
 private theorem consecutivePair_index {r : Route} {a b : Point}
     (h : (a, b) ∈ r.consecutivePairs) :
     ∃ (k : ℕ) (hk : k + 1 < r.length), r[k] = a ∧ r[k + 1] = b := by
diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Paths.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Paths.lean
index 6e63918ecd..bb22a149e9 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Paths.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/Paths.lean
@@ -173,4 +173,10 @@ theorem occurrencePaths_eq_paths (φ : CNF ℕ) :
     rw [(Cslib.Logic.PL.occurrences_nodup φ).idxOf_getElem i (by simpa using hi),
       List.getD_eq_getElem _ _ hj]
 
+/-- An actual occurrence selects a member of the canonical path list. -/
+theorem occurrencePath_mem_paths {φ : CNF ℕ} {o : Occurrence ℕ}
+    (ho : o ∈ Cslib.Logic.PL.occurrences φ) : occurrencePath φ o ∈ paths φ := by
+  rw [← occurrencePaths_eq_paths]
+  exact List.mem_map_of_mem ho
+
 end Cslib.Complexity.SAT.PlanarCompile
diff --git a/Complexity/Computability/Complexity/Problems/TwoSAT/Layout.lean b/Complexity/Computability/Complexity/Problems/TwoSAT/Layout.lean
index d91e8dc220..4313964575 100644
--- a/Complexity/Computability/Complexity/Problems/TwoSAT/Layout.lean
+++ b/Complexity/Computability/Complexity/Problems/TwoSAT/Layout.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Computability.Complexity.Problems.SAT
 import Complexity.Computability.Machines.Turing.MultiTape.Universal.InPlace
+import Mathlib.Data.List.GetD
 
 /-!
 # The layout of encoded formulas
@@ -286,6 +287,11 @@ end ClausesAt
 theorem clausesAt_encCNF (φ : CNF ℕ) : ClausesAt (encCNF φ) 0 φ := fun q => by
   rw [Nat.zero_add, encCNF_eq_flatMap]
 
+/-- Overwriting a register with its own value changes nothing. -/
+theorem set_getD_self {regs : List ℕ} {i : ℕ} (hi : i < regs.length) :
+    regs.set i (regs.getD i 0) = regs := by
+  rw [List.getD_eq_getElem _ _ hi, List.set_getElem_self]
+
 end TwoSAT
 
 end Cslib.Complexity
diff --git a/Complexity/Computability/Complexity/Problems/TwoSAT/Reduction.lean b/Complexity/Computability/Complexity/Problems/TwoSAT/Reduction.lean
index c968cdb19c..f35e8e66a8 100644
--- a/Complexity/Computability/Complexity/Problems/TwoSAT/Reduction.lean
+++ b/Complexity/Computability/Complexity/Problems/TwoSAT/Reduction.lean
@@ -187,11 +187,6 @@ private theorem bits_of_pos {q : ℕ} (hq : 0 < q) : q.bits = decide (q % 2 = 1)
     rw [Nat.bit1_bits, h]
     rfl
 
-/-- Overwriting a register with its own value changes nothing. -/
-private theorem set_getD_self {regs : List ℕ} {i : ℕ} (hi : i < regs.length) :
-    regs.set i (regs.getD i 0) = regs := by
-  rw [List.getD_eq_getElem _ _ hi, List.set_getElem_self]
-
 variable {P : CounterProgram} {w : List Bool} {B : ℕ}
 
 /-- The digit-writing loop of `literalCode`, writing the binary digits of `q` from register `5`. -/
diff --git a/Complexity/Computability/Complexity/Problems/TwoSAT/Routines.lean b/Complexity/Computability/Complexity/Problems/TwoSAT/Routines.lean
index 71eac8062d..6952525244 100644
--- a/Complexity/Computability/Complexity/Problems/TwoSAT/Routines.lean
+++ b/Complexity/Computability/Complexity/Problems/TwoSAT/Routines.lean
@@ -52,10 +52,6 @@ open _root_.Turing _root_.Turing.CounterProgram _root_.Turing.CounterProgram.Ins
 
 variable {P : CounterProgram} {w : List Bool} {B : ℕ}
 
-private theorem set_getD_self {regs : List ℕ} {i : ℕ} (hi : i < regs.length) :
-    regs.set i (regs.getD i 0) = regs := by
-  rw [List.getD_eq_getElem _ _ hi, List.set_getElem_self]
-
 /-- The register `r` of a bounded list is bounded. -/
 private theorem getD_le {regs : List ℕ} (hB : ∀ r ∈ regs, r ≤ B) (i : ℕ) :
     regs.getD i 0 ≤ B := by
diff --git a/Complexity/Computability/Complexity/Reduction/LogSpaceTruthTable.lean b/Complexity/Computability/Complexity/Reduction/LogSpaceTruthTable.lean
index 13d29ea5a7..e5e87e5e5f 100644
--- a/Complexity/Computability/Complexity/Reduction/LogSpaceTruthTable.lean
+++ b/Complexity/Computability/Complexity/Reduction/LogSpaceTruthTable.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Complexity.Classes.LogSpace
 public import Complexity.Computability.Complexity.Reduction.TruthTable
 public import Complexity.Computability.Complexity.Reduction.TruthTableVariants
+import Complexity.Foundations.Data.List.Filter
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram.Unary
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram.Words
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.Words
@@ -222,7 +223,7 @@ theorem LogSpaceDTTReducible.logSpacePTTReducible (h : LogSpaceDTTReducible encA
     LogSpacePTTReducible encA encB A B := by
   obtain ⟨r, q, hr, hq, hA⟩ := h
   refine ⟨r, q, fun p => p.2.any id, hr, hq, by fun_prop,
-    fun _ _ _ huv => any_id_le_of_forall₂ huv, fun a => ?_⟩
+    fun _ _ _ huv => List.any_id_le_of_forall₂ huv, fun a => ?_⟩
   rw [hA a]
   simp [truthTableAnswers, List.any_eq_true, List.mem_ofFn, Fin.exists_iff]
 
@@ -232,7 +233,7 @@ theorem LogSpaceCTTReducible.logSpacePTTReducible (h : LogSpaceCTTReducible encA
     LogSpacePTTReducible encA encB A B := by
   obtain ⟨r, q, hr, hq, hA⟩ := h
   refine ⟨r, q, fun p => p.2.all id, hr, hq, by fun_prop,
-    fun _ _ _ huv => all_id_le_of_forall₂ huv, fun a => ?_⟩
+    fun _ _ _ huv => List.all_id_le_of_forall₂ huv, fun a => ?_⟩
   rw [hA a]
   simp [truthTableAnswers, List.all_eq_true, List.mem_ofFn, Fin.forall_iff]
 
diff --git a/Complexity/Computability/Complexity/Reduction/TruthTableVariants.lean b/Complexity/Computability/Complexity/Reduction/TruthTableVariants.lean
index 38acc254c9..bd12a82a65 100644
--- a/Complexity/Computability/Complexity/Reduction/TruthTableVariants.lean
+++ b/Complexity/Computability/Complexity/Reduction/TruthTableVariants.lean
@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Complexity.Reduction.TruthTable
+import Complexity.Foundations.Data.List.Filter
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
@@ -396,30 +397,12 @@ theorem PolyTimePTTReducible.polyTimeTruthTableReducible (h : PolyTimePTTReducib
   let ⟨r, q, d, hr, hq, hd, _, hL⟩ := h
   ⟨r, q, d, hr, hq, hd, hL⟩
 
-/-- `List.any id` is monotone with respect to `List.Forall₂ (· ≤ ·)`. -/
-theorem any_id_le_of_forall₂ {u v : List Bool} (h : List.Forall₂ (· ≤ ·) u v) :
-    u.any id ≤ v.any id := by
-  induction h with
-  | nil => exact le_rfl
-  | cons hab _ ih =>
-    simp only [List.any_cons, id]
-    exact max_le_max hab ih
-
-/-- `List.all id` is monotone with respect to `List.Forall₂ (· ≤ ·)`. -/
-theorem all_id_le_of_forall₂ {u v : List Bool} (h : List.Forall₂ (· ≤ ·) u v) :
-    u.all id ≤ v.all id := by
-  induction h with
-  | nil => exact le_rfl
-  | cons hab _ ih =>
-    simp only [List.all_cons, id]
-    exact min_le_min hab ih
-
 /-- A disjunctive reduction is positive, with the disjunction of the answers as combiner. -/
 theorem PolyTimeDTTReducible.polyTimePTTReducible (h : PolyTimeDTTReducible encA encB L B) :
     PolyTimePTTReducible encA encB L B := by
   obtain ⟨r, q, hr, hq, hL⟩ := h
   refine ⟨r, q, fun x => x.2.any id, hr, hq, by fun_prop,
-    fun _ _ _ huv => any_id_le_of_forall₂ huv, fun a => ?_⟩
+    fun _ _ _ huv => List.any_id_le_of_forall₂ huv, fun a => ?_⟩
   rw [hL a]
   simp [truthTableAnswers, List.any_eq_true, List.mem_ofFn, Fin.exists_iff]
 
@@ -428,7 +411,7 @@ theorem PolyTimeCTTReducible.polyTimePTTReducible (h : PolyTimeCTTReducible encA
     PolyTimePTTReducible encA encB L B := by
   obtain ⟨r, q, hr, hq, hL⟩ := h
   refine ⟨r, q, fun x => x.2.all id, hr, hq, by fun_prop,
-    fun _ _ _ huv => all_id_le_of_forall₂ huv, fun a => ?_⟩
+    fun _ _ _ huv => List.all_id_le_of_forall₂ huv, fun a => ?_⟩
   rw [hL a]
   simp [truthTableAnswers, List.all_eq_true, List.mem_ofFn, Fin.forall_iff]
 
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/NormalForm.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/NormalForm.lean
index e37f9ecf4a..c6c51de0de 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Internal/NormalForm.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/NormalForm.lean
@@ -44,7 +44,7 @@ variable {α β γ : Type*} {encIn : α ↪ List Bool} {encMid : β ↪ List Boo
   {encOut : γ ↪ List Bool}
 
 /-- Absorb an additive constant into the factor of `n + 1`. -/
-private theorem le_mul_succ {u A B C n : ℕ} (h : u ≤ A * (n + 1) + B) (hC : A + B ≤ C) :
+theorem le_mul_succ {u A B C n : ℕ} (h : u ≤ A * (n + 1) + B) (hC : A + B ≤ C) :
     u ≤ C * (n + 1) := by
   have hB : B ≤ B * (n + 1) := Nat.le_mul_of_pos_right B (Nat.succ_pos n)
   have : A * (n + 1) + B ≤ (A + B) * (n + 1) := by rw [Nat.add_mul]; omega
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/OPrimitives.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/OPrimitives.lean
index aa94afe57b..19518ae0d1 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Internal/OPrimitives.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/OPrimitives.lean
@@ -35,13 +35,6 @@ namespace Turing.MultiTapeTM.ComputableInO
 variable {α β γ : Type*} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool}
   {encOut : γ ↪ List Bool}
 
-/-- Absorb an additive constant into the factor of `n + 1`. -/
-private theorem le_mul_succ {u A B C n : ℕ} (h : u ≤ A * (n + 1) + B) (hC : A + B ≤ C) :
-    u ≤ C * (n + 1) := by
-  have hB : B ≤ B * (n + 1) := Nat.le_mul_of_pos_right B (Nat.succ_pos n)
-  have : A * (n + 1) + B ≤ (A + B) * (n + 1) := by rw [Nat.add_mul]; omega
-  exact h.trans (this.trans (Nat.mul_le_mul_right _ hC))
-
 /-- **Composition** within time `O(T₁ a + T₂ (g a))` and space `O(S₁ a + S₂ (g a))`, through the
 machine-level composition of tidy machines. -/
 theorem comp {f : β → γ} {g : α → β} {T₁ S₁ : α → ℕ} {T₂ S₂ : β → ℕ}
@@ -59,7 +52,8 @@ theorem comp {f : β → γ} {g : α → β} {T₁ S₁ : α → ℕ} {T₂ S₂
     have e : (6 * c₁ + c₂) * (T₁ a + T₂ (g a) + 1) =
         6 * (c₁ * (T₁ a + T₂ (g a) + 1)) + c₂ * (T₁ a + T₂ (g a) + 1) := by ring
     beta_reduce
-    exact le_mul_succ (A := 6 * c₁ + c₂) (B := 6 * max k₁ k₂ + 20) (by omega) le_rfl
+    exact Internal.NormalForm.le_mul_succ (A := 6 * c₁ + c₂) (B := 6 * max k₁ k₂ + 20) (by omega)
+      le_rfl
   · -- the intermediate word is within the space bound of `g`
     have hm := l₁ a
     have := Nat.mul_le_mul_left c₁ (by omega : S₁ a + 1 ≤ S₁ a + S₂ (g a) + 1)
@@ -67,7 +61,8 @@ theorem comp {f : β → γ} {g : α → β} {T₁ S₁ : α → ℕ} {T₂ S₂
     have e : (6 * c₁ + c₂) * (S₁ a + S₂ (g a) + 1) =
         6 * (c₁ * (S₁ a + S₂ (g a) + 1)) + c₂ * (S₁ a + S₂ (g a) + 1) := by ring
     beta_reduce
-    exact le_mul_succ (A := 6 * c₁ + c₂) (B := 6 * max k₁ k₂ + 20) (by omega) le_rfl
+    exact Internal.NormalForm.le_mul_succ (A := 6 * c₁ + c₂) (B := 6 * max k₁ k₂ + 20) (by omega)
+      le_rfl
   · have := Nat.mul_le_mul_left c₂ (by omega : S₂ (g a) + 1 ≤ S₁ a + S₂ (g a) + 1)
     exact (l₂ (g a)).trans (this.trans (Nat.mul_le_mul_right _ (by omega)))
 
@@ -94,7 +89,7 @@ theorem ite {encC : Bool ↪ List Bool} {c : α → Bool} {f g : α → β}
     have := Nat.mul_le_mul_left c₀ (by omega : X + 1 ≤ X + Y + 1)
     have := Nat.mul_le_mul_left c' (by omega : Y + 1 ≤ X + Y + 1)
     have e : (c₀ + c') * (X + Y + 1) = c₀ * (X + Y + 1) + c' * (X + Y + 1) := by ring
-    exact le_mul_succ (A := c₀ + c') (B := d') (by omega) (by omega)
+    exact Internal.NormalForm.le_mul_succ (A := c₀ + c') (B := d') (by omega) (by omega)
   refine ⟨c₀ + c₁ + c₂ + k, ⟨K, Q, inferInstance, tm,
     fun x => ((h x).mono ?_ ?_).computesInTimeAndSpace⟩, fun x => ?_⟩
   · beta_reduce
diff --git a/Complexity/Computability/PolyTime/BitString/InitialTestsSearch.lean b/Complexity/Computability/PolyTime/BitString/InitialTestsSearch.lean
index 38d2a75f34..17b84c9093 100644
--- a/Complexity/Computability/PolyTime/BitString/InitialTestsSearch.lean
+++ b/Complexity/Computability/PolyTime/BitString/InitialTestsSearch.lean
@@ -17,6 +17,7 @@ import Complexity.Foundations.Data.BitString.Binary
 import Complexity.Foundations.Data.BitString.InitialTests
 import Complexity.Foundations.Data.BitString.Parity.DotProduct
 import Complexity.Foundations.Data.List.OfFn
+import Complexity.Foundations.Data.Nat.CeilDiv
 import Complexity.Probability.SmallBias.Random
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
@@ -64,10 +65,6 @@ open Finset Cslib.BitString Cslib.GenericRAM Cslib.Probability.PMF Turing.MultiT
 
 /-! ### Lemma 6.1 integer parameter schedule -/
 private abbrev mu (m : ℕ) : ℕ := Nat.log 2 m + 1
-private theorem le_ceilDiv_mul {a b : ℕ} (ha : 1 ≤ a) (hb : 0 < b) : a ≤ (a + b - 1) / b * b := by
-  have := Nat.div_add_mod (a + b - 1) b; have := Nat.mod_lt (a + b - 1) hb
-  have : a + b - 1 + 1 = a + b := by omega
-  nlinarith
 
 /-- Cayley degree `d_G = min(m, D₀)` (`D₀ = initialRowWeightBound B m`) of [OpenAI2026ETH],
 Lemma 6.1. -/
@@ -90,9 +87,11 @@ theorem dG_pos {m B : ℕ} (hm : 1 ≤ m) (hB : 1 ≤ B) : 0 < dG m B := by
   unfold dG initialRowWeightBound
   have : 0 < 320000 * B ^ 2 * (Nat.log 2 m + 1) ^ 3 := by positivity
   omega
-theorem le_qG_mul_dG {m B : ℕ} (hm : 1 ≤ m) (hB : 1 ≤ B) : m ≤ qG m B * dG m B :=
-  (le_ceilDiv_mul hm (dG_pos hm hB)).trans
-    (Nat.mul_le_mul_right _ (Nat.le_pow_clog (by decide : 1 < 2) _))
+theorem le_qG_mul_dG {m B : ℕ} (hm : 1 ≤ m) (hB : 1 ≤ B) : m ≤ qG m B * dG m B := by
+  have hd := dG_pos hm hB
+  exact (Nat.le_ceilDiv_mul hd).trans (by
+    rw [Nat.ceilDiv_eq_add_pred_div]
+    exact Nat.mul_le_mul_right _ (Nat.le_pow_clog (by decide : 1 < 2) _))
 theorem qG_mul_dG_lt_two_mul {m B : ℕ} (hm : 1 ≤ m) (hB : 1 ≤ B) : qG m B * dG m B < 2 * m := by
   have hd := dG_pos hm hB; set k := (m + dG m B - 1) / dG m B
   rcases le_or_gt k 1 with hk | hk
@@ -156,8 +155,9 @@ private theorem hDist_succ_eq {m B : ℕ} (hm : 1 ≤ m) (hB : 1 ≤ B) :
   have := (Nat.le_div_iff_mul_le hM).2 hle; unfold hDist; dsimp only [mu] at *; omega
 theorem dG_le_hDist_succ_mul {m B : ℕ} (hm : 1 ≤ m) (hB : 1 ≤ B) :
     dG m B ≤ (hDist m B + 1) * (100 * B * (Nat.log 2 m + 1)) := by
-  change dG m B ≤ (hDist m B + 1) * (100 * B * mu m); rw [hDist_succ_eq hm hB]
-  exact le_ceilDiv_mul (dG_pos hm hB) (by positivity)
+  change dG m B ≤ (hDist m B + 1) * (100 * B * mu m)
+  rw [hDist_succ_eq hm hB, ← Nat.ceilDiv_eq_add_pred_div]
+  exact Nat.le_ceilDiv_mul (by positivity)
 
 private abbrev encMB : ℕ × ℕ ↪ List Bool := encPair encUnary encUnary
 section
@@ -1070,7 +1070,9 @@ private theorem exists_localMatrix_params {m B : ℕ} (hm : 1 ≤ m) (hB : 1 ≤
   have hd_lt : dG m B < 2 ^ mu m :=
     (Nat.min_le_left _ _).trans_lt (Nat.lt_pow_succ_log_self (by decide : 1 < 2) m)
   have hmu_h : mu m * hDist m B < cG m B := by
-    have hc_ge : dG m B ≤ cG m B * (8 * B) := le_ceilDiv_mul (dG_pos hm hB) (by omega)
+    have hc_ge : dG m B ≤ cG m B * (8 * B) := by
+      rw [cG, ← Nat.ceilDiv_eq_add_pred_div]
+      exact Nat.le_ceilDiv_mul (by omega)
     have hle := Nat.mul_div_le (dG m B + 100 * B * mu m - 1) (100 * B * mu m)
     rw [← hDist_succ_eq hm hB] at hle; have := dG_pos hm hB
     have : dG m B + 100 * B * mu m - 1 + 1 = dG m B + 100 * B * mu m := by omega
diff --git a/Complexity/Foundations/Combinatorics/Expander/Basic.lean b/Complexity/Foundations/Combinatorics/Expander/Basic.lean
index e7bfdca147..1942b71a80 100644
--- a/Complexity/Foundations/Combinatorics/Expander/Basic.lean
+++ b/Complexity/Foundations/Combinatorics/Expander/Basic.lean
@@ -49,6 +49,8 @@ below is proved from these characterizations. `λ(G) ≤ 1` always, and `G` is a
 * `Cslib.RotationMap.interedges`: the edges from one set of vertices to another, as darts.
 * `Cslib.RotationMap.edgeCount`: the number of edges from one vertex to another.
 * `Cslib.RotationMap.walk`: the walk operator.
+* `Cslib.RotationMap.orthogonalSubmodule`: the subspace of `EuclideanSpace ℝ V` orthogonal to the
+  constant functions.
 * `Cslib.RotationMap.spectralExpansion`: the spectral expansion `λ(G)`.
 
 ## Main results
@@ -310,6 +312,11 @@ section SpectralExpansion
 
 variable [Fintype V] [Fintype D]
 
+/-- The subspace of `EuclideanSpace ℝ V` orthogonal to the constant functions. -/
+noncomputable def orthogonalSubmodule (V : Type*) [Fintype V] :
+    Submodule ℝ (EuclideanSpace ℝ V) :=
+  (ℝ ∙ WithLp.toLp 2 (fun _ ↦ 1 : V → ℝ))ᗮ
+
 /-- The **spectral expansion** `λ(G)`: the operator norm, for the Euclidean norm, of the walk
 operator on the functions orthogonal to the constants (`spectralExpansion_eq_norm_orthogonalWalk`)
 [Arora and Barak, Section 21.1][AroraBarak09].
@@ -322,7 +329,7 @@ absolute value of its eigenvalues on the functions of expectation zero
 noncomputable def spectralExpansion : ℝ :=
   ‖(LinearMap.toContinuousLinearMap
       (G.walk.withLpMap 2 : EuclideanSpace ℝ V →ₗ[ℝ] EuclideanSpace ℝ V)).comp
-    (ℝ ∙ WithLp.toLp 2 (fun _ ↦ 1 : V → ℝ))ᗮ.subtypeL‖
+    (orthogonalSubmodule V).subtypeL‖
 
 /-- The spectral expansion is nonnegative. -/
 theorem spectralExpansion_nonneg : 0 ≤ G.spectralExpansion := by
@@ -332,16 +339,17 @@ theorem spectralExpansion_nonneg : 0 ≤ G.spectralExpansion := by
 variable {G}
 
 /-- The second moment is the squared Euclidean norm, scaled by the number of vertices. -/
-private theorem card_mul_expect_sq (f : V → ℝ) :
+theorem card_mul_expect_sq (f : V → ℝ) :
     Fintype.card V * 𝔼 v, f v ^ 2 = ‖(WithLp.toLp 2 f : EuclideanSpace ℝ V)‖ ^ 2 := by
   rw [EuclideanSpace.real_norm_sq_eq, ← nsmul_eq_mul, ← card_univ, card_smul_expect]
 
-/-- The functions orthogonal to the constants are those of expectation zero. -/
-private theorem mem_orthogonal_iff (f : V → ℝ) :
-    (WithLp.toLp 2 f : EuclideanSpace ℝ V) ∈ (ℝ ∙ WithLp.toLp 2 (fun _ ↦ 1 : V → ℝ))ᗮ ↔
-      𝔼 v, f v = 0 := by
-  rw [Submodule.mem_orthogonal_singleton_iff_inner_right, EuclideanSpace.inner_toLp_toLp,
-    Fintype.expect_eq_sum_div_card, div_eq_zero_iff, or_iff_left_of_imp]
+/-- A vector in `EuclideanSpace ℝ V` is orthogonal to the constants iff its coordinates have
+expectation zero. -/
+theorem mem_orthogonalSubmodule_iff (f : V → ℝ) :
+    WithLp.toLp 2 f ∈ orthogonalSubmodule V ↔ 𝔼 v, f v = 0 := by
+  rw [orthogonalSubmodule, Submodule.mem_orthogonal_singleton_iff_inner_right,
+    EuclideanSpace.inner_toLp_toLp, Fintype.expect_eq_sum_div_card, div_eq_zero_iff,
+    or_iff_left_of_imp]
   · simp [dotProduct]
   · intro h
     have : IsEmpty V := Fintype.card_eq_zero_iff.1 (Nat.cast_eq_zero.1 h)
@@ -353,8 +361,8 @@ theorem expect_walk_sq_le_spectralExpansion_sq_mul {f : V → ℝ} (hf : 𝔼 v,
     𝔼 v, G.walk f v ^ 2 ≤ G.spectralExpansion ^ 2 * 𝔼 v, f v ^ 2 := by
   have h := ContinuousLinearMap.le_opNorm ((LinearMap.toContinuousLinearMap
       (G.walk.withLpMap 2 : EuclideanSpace ℝ V →ₗ[ℝ] EuclideanSpace ℝ V)).comp
-    (ℝ ∙ WithLp.toLp 2 (fun _ ↦ 1 : V → ℝ))ᗮ.subtypeL)
-    ⟨WithLp.toLp 2 f, (mem_orthogonal_iff f).2 hf⟩
+    (orthogonalSubmodule V).subtypeL)
+    ⟨WithLp.toLp 2 f, (mem_orthogonalSubmodule_iff f).2 hf⟩
   change ‖(WithLp.toLp 2 (G.walk f) : EuclideanSpace ℝ V)‖ ≤
     G.spectralExpansion * ‖(WithLp.toLp 2 f : EuclideanSpace ℝ V)‖ at h
   have h2 := pow_le_pow_left₀ (norm_nonneg _) h 2
@@ -371,7 +379,7 @@ theorem spectralExpansion_le {c : ℝ} (hc : 0 ≤ c)
     G.spectralExpansion ≤ c := by
   refine ContinuousLinearMap.opNorm_le_bound _ hc fun x ↦ ?_
   obtain ⟨⟨f⟩, hx⟩ := x
-  have hf := h f ((mem_orthogonal_iff f).1 hx)
+  have hf := h f ((mem_orthogonalSubmodule_iff f).1 hx)
   change ‖(WithLp.toLp 2 (G.walk f) : EuclideanSpace ℝ V)‖ ≤
     c * ‖(WithLp.toLp 2 f : EuclideanSpace ℝ V)‖
   refine (pow_le_pow_iff_left₀ (norm_nonneg _) (by positivity) two_ne_zero).1 ?_
diff --git a/Complexity/Foundations/Combinatorics/Expander/Hitting.lean b/Complexity/Foundations/Combinatorics/Expander/Hitting.lean
index 2c6f97c3c3..fa6863b330 100644
--- a/Complexity/Foundations/Combinatorics/Expander/Hitting.lean
+++ b/Complexity/Foundations/Combinatorics/Expander/Hitting.lean
@@ -130,18 +130,6 @@ section Hitting
 
 variable [Fintype V] [Fintype D]
 
-/-- By the second moment method (`Fintype.sq_expect_le_dens_mul_expect_sq`), the squared average
-of a function vanishing outside `C` is at most the density of `C` times its second moment. -/
-private theorem sq_expect_le_dens_mul_expect_sq {C : Finset V} {x : V → ℝ}
-    (hx : ∀ v ∉ C, x v = 0) :
-    (𝔼 v, x v) ^ 2 ≤ dens C * 𝔼 v, x v ^ 2 := by
-  classical
-  refine (Fintype.sq_expect_le_dens_mul_expect_sq x).trans ?_
-  have hsub : ({v : V | x v ≠ 0} : Finset V) ⊆ C := fun v hv =>
-    by_contra fun hvC => (mem_filter.mp hv).2 (hx v hvC)
-  exact mul_le_mul_of_nonneg_right (by exact_mod_cast dens_le_dens hsub)
-    (expect_nonneg fun _ _ => sq_nonneg _)
-
 /-- Subtracting `(1 - λ(G))` times the mean from `G.walk x` leaves second moment at most
 `λ(G) ^ 2` times the second moment of `x`. -/
 theorem expect_walk_sub_one_sub_spectralExpansion_sq_le [Nonempty V] [Nonempty D]
@@ -203,7 +191,7 @@ theorem expect_ite_mem_walk_sq_le [Nonempty D] {B C : Finset V} {μ : ℝ} (hB :
       _ ≤ μ * (μ * 𝔼 v, x v ^ 2) := by
           have := expect_nonneg (s := (univ : Finset V)) fun v _ => sq_nonneg (x v)
           gcongr
-          exact (sq_expect_le_dens_mul_expect_sq hx).trans (by gcongr)
+          exact (Fintype.sq_expect_le_dens_mul_expect_sq_of_eq_zero hx).trans (by gcongr)
       _ = μ ^ 2 * 𝔼 v, x v ^ 2 := by ring
   · refine le_trans (expect_le_expect fun v _ => ?_)
       (G.expect_walk_sub_one_sub_spectralExpansion_sq_le x)
@@ -268,7 +256,8 @@ theorem dens_filter_forall_walkAt_mem_le [Nonempty D] {B : ℕ → Finset V} {μ
     simp only [h, prod_ite_zero, prod_const_one, mem_range, Nat.lt_succ_iff]
   rw [hprob]
   have hbound : (𝔼 v, G.weightedWalk t h v) ^ 2 ≤ (μ * c ^ t) ^ 2 :=
-    (sq_expect_le_dens_mul_expect_sq fun _ => G.weightedWalk_ite_eq_zero_of_notMem t B).trans <|
+    (Fintype.sq_expect_le_dens_mul_expect_sq_of_eq_zero fun _ =>
+      G.weightedWalk_ite_eq_zero_of_notMem t B).trans <|
       (mul_le_mul (hB 0) (G.expect_weightedWalk_ite_sq_le t B hB)
         (expect_nonneg fun _ _ => sq_nonneg _) hμ).trans_eq (by ring)
   calc 𝔼 v, G.weightedWalk t h v ≤ μ * c ^ t := (abs_le_of_sq_le_sq' hbound (by positivity)).2
diff --git a/Complexity/Foundations/Combinatorics/Expander/Mixing.lean b/Complexity/Foundations/Combinatorics/Expander/Mixing.lean
index f68a740af8..6d46c3c8a5 100644
--- a/Complexity/Foundations/Combinatorics/Expander/Mixing.lean
+++ b/Complexity/Foundations/Combinatorics/Expander/Mixing.lean
@@ -131,16 +131,6 @@ section Sets
 
 variable [DecidableEq V]
 
-/-- The expectation of an indicator function is the density of the set. -/
-private theorem expect_boole_mem (S : Finset V) :
-    𝔼 v, (if v ∈ S then (1 : ℝ) else 0) = #S / Fintype.card V := by
-  rw [Fintype.expect_boole_mem, nnratCast_dens]
-
-/-- An indicator function is its own square. -/
-private theorem expect_boole_mem_sq (S : Finset V) :
-    𝔼 v, (if v ∈ S then (1 : ℝ) else 0) ^ 2 = #S / Fintype.card V := by
-  rw [Fintype.expect_boole_mem_sq, nnratCast_dens]
-
 /-- The correlation of the indicator function of `S` with the walk operator applied to that of `T`
 is the proportion of the darts from `S` to `T`. -/
 private theorem expect_boole_mem_mul_walk (S T : Finset V) :
@@ -175,8 +165,9 @@ theorem abs_card_interedges_sub_le (S T : Finset V) :
   have hd : (0 : ℝ) < Fintype.card D := Nat.cast_pos.2 Fintype.card_pos
   have h := G.sq_expect_mul_walk_pow_sub_le 1 (fun v ↦ if v ∈ S then 1 else 0)
     (fun v ↦ if v ∈ T then 1 else 0)
-  rw [pow_one, mul_one, expect_boole_mem_mul_walk, expect_boole_mem, expect_boole_mem,
-    expect_boole_mem_sq, expect_boole_mem_sq] at h
+  rw [pow_one, mul_one, expect_boole_mem_mul_walk, Fintype.expect_boole_mem,
+    Fintype.expect_boole_mem, Fintype.expect_boole_mem_sq, Fintype.expect_boole_mem_sq,
+    nnratCast_dens, nnratCast_dens] at h
   have := G.spectralExpansion_nonneg
   refine abs_le_of_sq_le_sq ?_ (by positivity)
   rw [div_pow, mul_pow, mul_pow, Real.sq_sqrt (by positivity), card_compl_eq, card_compl_eq]
@@ -233,8 +224,8 @@ theorem le_card_interedges_compl_of_expect_mul_walk_le {μ : ℝ}
     (fun v ↦ if v ∈ S then 1 else 0)
   rw [pow_one] at hc
   rw [← add_sub_cancel_left ((𝔼 v, if v ∈ S then (1 : ℝ) else 0) * 𝔼 v, if v ∈ S then 1 else 0)
-    (𝔼 v, _ * G.walk _ v), ← hc, expect_sub_expect_sq, expect_boole_mem_mul_walk, expect_boole_mem,
-    expect_boole_mem_sq] at h
+    (𝔼 v, _ * G.walk _ v), ← hc, expect_sub_expect_sq, expect_boole_mem_mul_walk,
+    Fintype.expect_boole_mem, Fintype.expect_boole_mem_sq, nnratCast_dens] at h
   have he : (#(G.interedges S S) : ℝ) + #(G.interedges S Sᶜ) = #S * Fintype.card D := by
     exact_mod_cast G.card_interedges_add_card_interedges_compl S S
   rw [card_compl_eq, div_le_iff₀ hn]
diff --git a/Complexity/Foundations/Combinatorics/Expander/Spectrum.lean b/Complexity/Foundations/Combinatorics/Expander/Spectrum.lean
index a5f8bbf250..951c573a73 100644
--- a/Complexity/Foundations/Combinatorics/Expander/Spectrum.lean
+++ b/Complexity/Foundations/Combinatorics/Expander/Spectrum.lean
@@ -105,33 +105,11 @@ private theorem card_mul_expect_mul (x y : EuclideanSpace ℝ V) :
   rw [Fintype.card_mul_expect, EuclideanSpace.inner_eq_star_dotProduct, star_trivial, dotProduct]
   exact sum_congr rfl fun _ _ ↦ mul_comm _ _
 
-/-- The squared Euclidean norm on `EuclideanSpace ℝ V` is the second moment scaled by `|V|`. -/
-private theorem card_mul_expect_sq (x : EuclideanSpace ℝ V) :
-    (Fintype.card V : ℝ) * 𝔼 v, x.ofLp v ^ 2 = ‖x‖ ^ 2 := by
-  rw [EuclideanSpace.real_norm_sq_eq, Fintype.card_mul_expect]
-
 /-- The walk operator on `EuclideanSpace ℝ V` is symmetric. -/
 theorem isSymmetric_walkEuclidean : G.walkEuclidean.IsSymmetric := fun x y ↦ by
   rw [← card_mul_expect_mul, ← card_mul_expect_mul, ofLp_walkEuclidean, ofLp_walkEuclidean,
     G.expect_mul_walk_comm]
 
-/-- The subspace of `EuclideanSpace ℝ V` orthogonal to the constant functions. -/
-noncomputable def orthogonalSubmodule (V : Type*) [Fintype V] :
-    Submodule ℝ (EuclideanSpace ℝ V) :=
-  (ℝ ∙ WithLp.toLp 2 (fun _ ↦ 1 : V → ℝ))ᗮ
-
-/-- A vector in `EuclideanSpace ℝ V` is orthogonal to the constants iff its coordinates have
-expectation zero. -/
-theorem mem_orthogonalSubmodule_iff (f : V → ℝ) :
-    WithLp.toLp 2 f ∈ orthogonalSubmodule V ↔ 𝔼 v, f v = 0 := by
-  rw [orthogonalSubmodule, Submodule.mem_orthogonal_singleton_iff_inner_right,
-    EuclideanSpace.inner_toLp_toLp, Fintype.expect_eq_sum_div_card, div_eq_zero_iff,
-    or_iff_left_of_imp]
-  · simp [dotProduct]
-  · intro h
-    have : IsEmpty V := Fintype.card_eq_zero_iff.1 (Nat.cast_eq_zero.1 h)
-    simp
-
 /-- The walk operator preserves `orthogonalSubmodule V`. -/
 theorem walkEuclidean_mem_orthogonalSubmodule {x : EuclideanSpace ℝ V}
     (hx : x ∈ orthogonalSubmodule V) :
@@ -276,9 +254,9 @@ theorem spectralExpansion_eq_ciSup_abs_eigenvalues :
       exact pow_le_pow_left₀ (abs_nonneg _) hi 2
     exact mul_le_mul_of_nonneg_right hi2 (sq_nonneg _)
   have hnorm_u : ‖u‖ ^ 2 = (Fintype.card V : ℝ) * 𝔼 v, f v ^ 2 :=
-    (card_mul_expect_sq (WithLp.toLp 2 f)).symm
+    (card_mul_expect_sq f).symm
   have hnorm_wu : ‖G.orthogonalWalk u‖ ^ 2 = (Fintype.card V : ℝ) * 𝔼 v, G.walk f v ^ 2 :=
-    (card_mul_expect_sq (WithLp.toLp 2 (G.walk f))).symm
+    (card_mul_expect_sq (G.walk f)).symm
   rw [hnorm_wu, hnorm_u, mul_left_comm] at hle
   rcases (Fintype.card V).eq_zero_or_pos with hV | hV
   · have : IsEmpty V := Fintype.card_eq_zero_iff.1 hV
@@ -318,7 +296,7 @@ theorem secondEigenvalue_eq_orthogonalWalk_eigenvalues_zero (h0 : 0 < n) :
   have hinner : ⟪u, G.orthogonalWalk u⟫ = (Fintype.card V : ℝ) * 𝔼 v, f v * G.walk f v :=
     (card_mul_expect_mul (WithLp.toLp 2 f) (WithLp.toLp 2 (G.walk f))).symm
   have hnorm : ‖u‖ ^ 2 = (Fintype.card V : ℝ) * 𝔼 v, f v ^ 2 :=
-    (card_mul_expect_sq (WithLp.toLp 2 f)).symm
+    (card_mul_expect_sq f).symm
   rw [hinner, hnorm, mul_left_comm] at hle
   exact le_of_mul_le_mul_left hle (Nat.cast_pos.2 Fintype.card_pos)
 
@@ -409,8 +387,8 @@ private theorem le_secondEigenvalue_of_mul_norm_sq_le_inner [Nonempty V]
     expect_pos' (fun _ _ ↦ sq_nonneg _) ⟨v₀, mem_univ v₀, sq_pos_iff.2 hv₀⟩
   have hinner : ⟪u, G.walkEuclidean u⟫ = (Fintype.card V : ℝ) * 𝔼 v, f v * G.walk f v :=
     (card_mul_expect_mul u (G.walkEuclidean u)).symm
-  have hnorm : ‖u‖ ^ 2 = (Fintype.card V : ℝ) * 𝔼 v, f v ^ 2 :=
-    (card_mul_expect_sq u).symm
+  have hnorm : ‖u‖ ^ 2 = (Fintype.card V : ℝ) * 𝔼 v, f v ^ 2 := by
+    simpa [f] using (card_mul_expect_sq f).symm
   rw [hinner, hnorm, mul_left_comm] at hu_quad
   have hle₁ := le_of_mul_le_mul_left hu_quad (Nat.cast_pos.2 Fintype.card_pos)
   have hle₂ := G.expect_mul_walk_le_secondEigenvalue_mul hu_exp
@@ -487,7 +465,7 @@ private theorem secondEigenvalue_le_walkEuclidean_eigenvalues_one [Nonempty D] (
   have hinner : ⟪x, G.walkEuclidean x⟫ = (Fintype.card V : ℝ) * 𝔼 v, f v * G.walk f v :=
     (card_mul_expect_mul x (G.walkEuclidean x)).symm
   have hnorm : ‖x‖ ^ 2 = (Fintype.card V : ℝ) * 𝔼 v, f v ^ 2 :=
-    (card_mul_expect_sq x).symm
+    (card_mul_expect_sq f).symm
   rw [hinner, hnorm, mul_left_comm] at hle
   exact le_of_mul_le_mul_left hle (Nat.cast_pos.2 Fintype.card_pos)
 
diff --git a/Complexity/Foundations/Data/BitString/WordCount.lean b/Complexity/Foundations/Data/BitString/WordCount.lean
index 52ebc0f8b2..a35f2efd63 100644
--- a/Complexity/Foundations/Data/BitString/WordCount.lean
+++ b/Complexity/Foundations/Data/BitString/WordCount.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Foundations.Data.BitString.List
 public import Complexity.Foundations.Data.BitString.List.Binary
 public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+public import Mathlib.Algebra.Ring.BooleanRing
 public import Mathlib.Data.Fintype.Pi
 public import Mathlib.Data.ZMod.Basic
 public import Mathlib.Order.PiLex
@@ -59,7 +60,8 @@ represent sets of words.
 * `Cslib.BitString.two_pow_mul_card_filter_card_filter_block_le`: majority votes of `12 e` blocks
   err on at most a `2 ^ (-e)` fraction.
 * `Cslib.BitString.card_filter_listRows_all`: counting words by a condition on each row.
-* `Cslib.BitString.card_filter_not_any`, `Cslib.BitString.card_filter_all`: the constant words.
+* `Cslib.BitString.not_any_ofFn_eq_true_iff`, `Cslib.BitString.card_filter_not_any`,
+  `Cslib.BitString.card_filter_all`: the constant words.
 * `Cslib.BitString.ofFn_decide_lt`: the unary word of `k` bits `true` among `K`.
 * `Cslib.BitString.wordLt_ofFn_iff`: `wordLt` is the lexicographic order.
 * `Cslib.BitString.odd_prod_iff`, `Cslib.BitString.odd_one_add_prod_one_add`: parity of products
@@ -188,15 +190,19 @@ theorem card_filter_ofFn_succ (n : ℕ) (g : List Bool → Prop) [DecidablePred
   rw [hmap, card_filter, Fintype.sum_prod_type, Fintype.sum_bool]
   simp only [card_filter]
 
+/-- A bit string `w` has no `true` bits in `List.ofFn w` if and only if `w = 0`. -/
+theorem not_any_ofFn_eq_true_iff {n : ℕ} (w : Fin n → Bool) :
+    (!(List.ofFn w).any fun b => b) = true ↔ w = 0 := by
+  simp only [Bool.not_eq_eq_eq_not, Bool.not_true, List.any_eq_false, List.mem_ofFn,
+    forall_exists_index, forall_apply_eq_imp_iff, Bool.not_eq_true]
+  exact ⟨fun h => funext h, fun h i => congrFun h i⟩
+
 /-- Only the word of `false`s has no bit `true`. -/
 theorem card_filter_not_any (n : ℕ) :
     (univ.filter fun w : Fin n → Bool => (!(List.ofFn w).any fun b => b) = true).card = 1 := by
   rw [card_eq_one]
-  refine ⟨fun _ => false, ext fun w => ?_⟩
-  simp only [mem_filter, mem_univ, true_and, Bool.not_eq_eq_eq_not, Bool.not_true,
-    List.any_eq_false, List.mem_ofFn, forall_exists_index, forall_apply_eq_imp_iff,
-    mem_singleton, Bool.not_eq_true]
-  exact ⟨fun h => funext h, fun h i => by rw [h]⟩
+  refine ⟨0, ext fun w => ?_⟩
+  simp only [mem_filter, mem_univ, true_and, not_any_ofFn_eq_true_iff, mem_singleton]
 
 /-- Only the word of `true`s has all bits `true`. -/
 theorem card_filter_all (n : ℕ) :
diff --git a/Complexity/Foundations/Data/Finset/Expect.lean b/Complexity/Foundations/Data/Finset/Expect.lean
index 34afa16b3a..7872a17c3b 100644
--- a/Complexity/Foundations/Data/Finset/Expect.lean
+++ b/Complexity/Foundations/Data/Finset/Expect.lean
@@ -68,7 +68,9 @@ random tuple leaves its average unchanged (`Fintype.expect_expect_update`).
 * `Fintype.expect_boole`, `Fintype.expect_boole_sq`, `Fintype.expect_boole_mem`,
   `Fintype.expect_boole_mem_sq`: the average of an indicator (or its square) is a density.
 * `Fintype.mul_dens_filter_le_expect`: Markov's inequality for a uniform average.
-* `Fintype.sq_expect_le_dens_mul_expect_sq`: the second moment method for a uniform average.
+* `Fintype.sq_expect_le_dens_mul_expect_sq`,
+  `Fintype.sq_expect_le_dens_mul_expect_sq_of_eq_zero`: the second moment method for a uniform
+  average.
 * `Fintype.expect_add_sq_le`, `Fintype.expect_sq_le_of_expect_mul_le`: second-moment bounds from
   triangle and Cauchy–Schwarz inequalities.
 -/
@@ -296,6 +298,19 @@ theorem sq_expect_le_dens_mul_expect_sq [Semifield 𝕜] [LinearOrder 𝕜] [IsS
     expect_congr rfl fun i _ ↦ by split_ifs <;> simp_all
   rwa [h₁, expect_boole_sq] at h
 
+/-- By the second moment method (`Fintype.sq_expect_le_dens_mul_expect_sq`), the squared average
+of a function vanishing outside `C` is at most the density of `C` times its second moment. -/
+theorem sq_expect_le_dens_mul_expect_sq_of_eq_zero [Semifield 𝕜] [LinearOrder 𝕜]
+    [IsStrictOrderedRing 𝕜] [ExistsAddOfLE 𝕜] {C : Finset ι} {f : ι → 𝕜}
+    (hf : ∀ i ∉ C, f i = 0) :
+    (𝔼 i, f i) ^ 2 ≤ (dens C : 𝕜) * 𝔼 i, f i ^ 2 := by
+  classical
+  refine (sq_expect_le_dens_mul_expect_sq f).trans ?_
+  have hsub : ({i : ι | f i ≠ 0} : Finset ι) ⊆ C := fun i hi =>
+    by_contra fun hiC => (mem_filter.mp hi).2 (hf i hiC)
+  exact mul_le_mul_of_nonneg_right (by exact_mod_cast dens_le_dens hsub)
+    (expect_nonneg fun _ _ => sq_nonneg _)
+
 section LinearOrderedField
 
 variable [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
diff --git a/Complexity/Foundations/Data/List/Filter.lean b/Complexity/Foundations/Data/List/Filter.lean
index afb7dac702..20cc3ed21a 100644
--- a/Complexity/Foundations/Data/List/Filter.lean
+++ b/Complexity/Foundations/Data/List/Filter.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2026 Erik Demaine, Samuel Schlesinger. All rights reserved.
+Copyright (c) 2026 Erik Demaine, Christian Reitwiessner, Samuel Schlesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Erik Demaine, Samuel Schlesinger
+Authors: Erik Demaine, Christian Reitwiessner, Samuel Schlesinger
 -/
 
 module
@@ -10,6 +10,7 @@ module
 public import Complexity.Init
 public import Mathlib.Algebra.BigOperators.Group.List.Basic
 public import Mathlib.Data.Finset.Basic
+public import Mathlib.Data.List.Forall2
 import Mathlib.Data.List.GetD
 
 /-!
@@ -26,6 +27,8 @@ They are generalized from the canonical incidence-path occupancy proofs.
   `C.toFinset \ H.toFinset`.
 * `List.countP_le_sum_map`: if `1 ≤ f x` whenever `p x = true` on `l`, then
   `l.countP p ≤ (l.map f).sum`.
+* `List.any_id_le_of_forall₂`, `List.all_id_le_of_forall₂`: `List.any id` and `List.all id` are
+  monotone with respect to `List.Forall₂ (· ≤ ·)`.
 -/
 
 @[expose] public section
@@ -135,4 +138,22 @@ theorem countP_le_sum_map {α : Type*} {p : α → Bool} {f : α → ℕ} {l : L
     · simp only [hp, Bool.false_eq_true, ite_false]
       omega
 
+/-- `List.any id` is monotone with respect to `List.Forall₂ (· ≤ ·)`. -/
+theorem any_id_le_of_forall₂ {u v : List Bool} (h : List.Forall₂ (· ≤ ·) u v) :
+    u.any id ≤ v.any id := by
+  induction h with
+  | nil => exact le_rfl
+  | cons hab _ ih =>
+    simp only [List.any_cons, id]
+    exact max_le_max hab ih
+
+/-- `List.all id` is monotone with respect to `List.Forall₂ (· ≤ ·)`. -/
+theorem all_id_le_of_forall₂ {u v : List Bool} (h : List.Forall₂ (· ≤ ·) u v) :
+    u.all id ≤ v.all id := by
+  induction h with
+  | nil => exact le_rfl
+  | cons hab _ ih =>
+    simp only [List.all_cons, id]
+    exact min_le_min hab ih
+
 end List
diff --git a/Complexity/Foundations/Geometry/Orthogonal.lean b/Complexity/Foundations/Geometry/Orthogonal.lean
index 6170e20d5a..8affa647a7 100644
--- a/Complexity/Foundations/Geometry/Orthogonal.lean
+++ b/Complexity/Foundations/Geometry/Orthogonal.lean
@@ -31,6 +31,8 @@ points. A singleton route has singleton support; an empty route has empty suppor
 
 * `Cslib.Orthogonal.mem_horizontal`, `Cslib.Orthogonal.mem_vertical`: real segment membership
   characterized by coordinate intervals.
+* `Cslib.Orthogonal.mem_support_pair`, `Cslib.Orthogonal.support_bounds_of_points`: continuous
+  support of a single segment and coordinate bounding-box preservation.
 
 ## References
 
@@ -72,6 +74,20 @@ theorem support_cons_cons (a b : Point) (r : Route) :
   have ha : realPoint a ∈ segment a b := left_mem_segment ℝ _ _
   aesop
 
+/-- The continuous support of a two-point route `[a, b]` is the segment `segment a b`. -/
+theorem mem_support_pair {a b : Point} {p : ℝ × ℝ} :
+    p ∈ support [a, b] ↔ p ∈ segment a b := by
+  rw [support_cons_cons]
+  change (p ∈ segment a b ∨ p ∈ support [b]) ↔ _
+  have hright : realPoint b ∈ segment a b := _root_.right_mem_segment ℝ _ _
+  have hs : p ∈ support [b] ↔ p = realPoint b := by simp [support, List.consecutivePairs]
+  rw [hs]
+  exact ⟨fun h => h.elim id (fun h => h ▸ hright), Or.inl⟩
+
+/-- The continuous support of a two-point route `[a, b]` equals `segment a b`. -/
+theorem support_pair (a b : Point) : support [a, b] = segment a b :=
+  Set.ext fun _ => mem_support_pair
+
 /-- A proper axis-aligned segment; zero-length segments are excluded. -/
 def AxisAligned (a b : Point) : Prop :=
   (a.1 = b.1 ∨ a.2 = b.2) ∧ a ≠ b
@@ -145,6 +161,28 @@ theorem mem_segment_bounds {a b : Point} {p : ℝ × ℝ} (hp : p ∈ segment a
   obtain ⟨s, t, hs, ht, hst, rfl⟩ := hp
   constructor <;> rw [← segment_eq_uIcc] <;> exact ⟨s, t, hs, ht, hst, rfl⟩
 
+/-- If every listed point of a route lies in `[x₀, x₁] × [y₀, y₁]`, then every point of its
+continuous support lies in `[x₀, x₁] × [y₀, y₁]`. -/
+theorem support_bounds_of_points {r : Route} {x₀ x₁ y₀ y₁ : ℤ}
+    (h : ∀ q ∈ r, x₀ ≤ q.1 ∧ q.1 ≤ x₁ ∧ y₀ ≤ q.2 ∧ q.2 ≤ y₁)
+    {p : ℝ × ℝ} (hp : p ∈ support r) :
+    (x₀ : ℝ) ≤ p.1 ∧ p.1 ≤ x₁ ∧ (y₀ : ℝ) ≤ p.2 ∧ p.2 ≤ y₁ := by
+  have cast_bounds (q : Point) (hq : q ∈ r) :
+      (x₀ : ℝ) ≤ q.1 ∧ (q.1 : ℝ) ≤ x₁ ∧ (y₀ : ℝ) ≤ q.2 ∧ (q.2 : ℝ) ≤ y₁ := by
+    exact_mod_cast h q hq
+  rcases hp with ⟨q, hq, rfl⟩ | ⟨e, he, hp⟩
+  · exact cast_bounds q hq
+  · have he' := List.of_mem_zip he
+    have ha := cast_bounds e.1 he'.1
+    have hb := cast_bounds e.2 (List.mem_of_mem_tail he'.2)
+    obtain ⟨hx, hy⟩ := mem_segment_bounds hp
+    rw [Set.mem_uIcc] at hx hy
+    refine ⟨?_, ?_, ?_, ?_⟩
+    · exact hx.elim (fun hx => ha.1.trans hx.1) (fun hx => hb.1.trans hx.1)
+    · exact hx.elim (fun hx => hx.2.trans hb.2.1) (fun hx => hx.2.trans ha.2.1)
+    · exact hy.elim (fun hy => ha.2.2.1.trans hy.1) (fun hy => hb.2.2.1.trans hy.1)
+    · exact hy.elim (fun hy => hy.2.trans hb.2.2.2) (fun hy => hy.2.trans ha.2.2.2)
+
 /-- Horizontal real segment membership is a one-dimensional interval test. -/
 theorem mem_horizontal {a b y : ℝ} {p : ℝ × ℝ} :
     p ∈ _root_.segment ℝ (a, y) (b, y) ↔ p.2 = y ∧ p.1 ∈ Set.uIcc a b := by
diff --git a/Complexity/Foundations/Geometry/Orthogonal/PairedPorts.lean b/Complexity/Foundations/Geometry/Orthogonal/PairedPorts.lean
index 50a34d3722..ce89a4fde1 100644
--- a/Complexity/Foundations/Geometry/Orthogonal/PairedPorts.lean
+++ b/Complexity/Foundations/Geometry/Orthogonal/PairedPorts.lean
@@ -122,15 +122,6 @@ theorem access_disjoint {p q : Port} (h : p ≠ q) :
     Disjoint (support (accessRoute p.1 p.2)) (support (accessRoute q.1 q.2)) :=
   disjoint_support_of_routeContactCheck (access_disjoint_check p q h)
 
-private theorem mem_support_pair {a b : Point} {p : ℝ × ℝ} :
-    p ∈ support [a, b] ↔ p ∈ segment a b := by
-  rw [support_cons_cons]
-  change (p ∈ segment a b ∨ p ∈ support [b]) ↔ _
-  have hright : realPoint b ∈ segment a b := _root_.right_mem_segment ℝ _ _
-  have hs : p ∈ support [b] ↔ p = realPoint b := by simp [support, List.consecutivePairs]
-  rw [hs]
-  exact ⟨fun h => h.elim id (fun h => h ▸ hright), Or.inl⟩
-
 /-- An access stays in the cell and touches its boundary only at the designated port. -/
 theorem access_boundary_isolation {s : Fin 4} {l : Fin 2} {p : ℝ × ℝ}
     (hp : p ∈ support (accessRoute s l)) :
diff --git a/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingSearch.lean b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingSearch.lean
index 8bec696bdf..4654acee13 100644
--- a/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingSearch.lean
+++ b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingSearch.lean
@@ -84,31 +84,6 @@ variable {V : Type*} [DecidableEq V] {θ : ℕ → ℕ}
 
 /-! ### Clause-set properties of `countingChild` -/
 
-/-- The flower `flower ψ c H` is disjoint from both counting children `countingChild ψ c H b`:
-on `false` every flower clause strictly contains `H`, and on `true` every flower clause `C`
-strictly contains its petal `C \ H`. -/
-theorem disjoint_flower_countingChild {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)}
-    (h : Heavy θ ψ c H) (b : Bool) :
-    Disjoint (flower ψ c H) (countingChild ψ c H b) := by
-  rw [Finset.disjoint_left]
-  intro C hC hCchild
-  obtain ⟨-, hcard, hH⟩ := mem_flower.mp hC
-  cases b with
-  | false =>
-    have hmin := (mem_reduce.mp hCchild).2
-    refine hmin H (mem_union_right _ (by simp [intro])) (ssubset_of_subset_of_ne hH ?_)
-    intro heq
-    have := h.2.1
-    rw [heq, hcard] at this
-    exact lt_irrefl _ this
-  | true =>
-    have hmin := (mem_reduce.mp hCchild).2
-    refine hmin (C \ H)
-      (mem_union_left _ (mem_union_right _ (mem_petals.mpr ⟨C, hC, rfl⟩)))
-      (sdiff_ssubset hH ?_)
-    rw [← card_pos]
-    exact h.1
-
 /-- Every clause of `countingChild ψ c H true` belongs to `(ψ \ flower ψ c H) ∪ petals ψ c H ∪
 negatedHeartUnits H`. -/
 private theorem countingChild_true_subset {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)}
@@ -118,7 +93,7 @@ private theorem countingChild_true_subset {ψ : ClauseSet V} {c : ℕ} {H : Fins
   rcases mem_union.mp (reduce_subset _ hC) with hC' | hCu
   · rcases mem_union.mp hC' with hCψ | hCp
     · refine mem_union_left _ (mem_union_left _ (mem_sdiff.mpr ⟨hCψ, fun hF => ?_⟩))
-      exact disjoint_left.mp (disjoint_flower_countingChild h true) hF hC
+      exact disjoint_left.mp (disjoint_flower_countingChild ψ h.1 h.2.1 true) hF hC
     · exact mem_union_left _ (mem_union_right _ hCp)
   · exact mem_union_right _ hCu
 
@@ -129,24 +104,9 @@ private theorem countingChild_false_subset {ψ : ClauseSet V} {c : ℕ} {H : Fin
   intro C hC
   rcases mem_union.mp (reduce_subset _ hC) with hCψ | hCH
   · refine mem_union_left _ (mem_sdiff.mpr ⟨hCψ, fun hF => ?_⟩)
-    exact disjoint_left.mp (disjoint_flower_countingChild h false) hF hC
+    exact disjoint_left.mp (disjoint_flower_countingChild ψ h.1 h.2.1 false) hF hC
   · exact mem_union_right _ hCH
 
-/-- Counting children keep the clause width `≤ k` when `1 ≤ k`. -/
-theorem card_le_of_mem_countingChild (hθ : ∀ j, 1 ≤ θ j) {ψ : ClauseSet V} {c k : ℕ}
-    (hk1 : 1 ≤ k) {H : Finset (Literal V)} (h : Heavy θ ψ c H) (hk : ∀ C ∈ ψ, C.card ≤ k)
-    {b : Bool} {C : Finset (Literal V)} (hC : C ∈ countingChild ψ c H b) : C.card ≤ k := by
-  cases b with
-  | false => exact card_le_of_mem_child hθ h hk hC
-  | true =>
-    rcases mem_union.mp (countingChild_true_subset h hC) with hC' | hCu
-    · rcases mem_union.mp hC' with hCψ | hCp
-      · exact hk C (mem_sdiff.mp hCψ).1
-      · obtain ⟨D, hD, rfl⟩ := mem_petals.mp hCp
-        exact (card_le_card sdiff_subset).trans (hk D (flower_subset ψ c H hD))
-    · rw [card_of_mem_negatedHeartUnits hCu]
-      exact hk1
-
 /-- Each counting child increases the number of clauses by at most `k`: the flower `F` is removed
 from `ψ` while at most `|F| + |H| ≤ |F| + k` clauses are added. -/
 theorem card_countingChild_le (hθ : ∀ j, 1 ≤ θ j) {ψ : ClauseSet V} {c k : ℕ}
@@ -277,7 +237,7 @@ theorem exists_isLeafWord (hθ : ∀ j, 1 ≤ j → 2 ≤ θ j) (s : σ) :
       exact ⟨false :: w, hs, hw⟩
 
 /-- Node words preserve clause width `≤ k` when `1 ≤ k`. -/
-theorem IsNodeWord.card_le_of_mem_walk (hθ : ∀ j, 1 ≤ θ j) {k : ℕ} (hk1 : 1 ≤ k) {s : σ}
+theorem IsNodeWord.card_le_of_mem_walk (hθ : ∀ j, 1 ≤ θ j) {k : ℕ} (_hk1 : 1 ≤ k) {s : σ}
     (hk : ∀ C ∈ R.toClauseSet s, C.card ≤ k) {w : List Bool} (hw : R.IsNodeWord s w) :
     ∀ C ∈ R.toClauseSet (R.walk s w), C.card ≤ k := by
   induction w generalizing s with
@@ -286,11 +246,11 @@ theorem IsNodeWord.card_le_of_mem_walk (hθ : ∀ j, 1 ≤ θ j) {k : ℕ} (hk1
     obtain ⟨c, H, hch, hnext⟩ := R.exists_choice_next s hw.1
     refine ih (fun C hC => ?_) hw.2
     rw [hnext b] at hC
-    exact card_le_of_mem_countingChild hθ hk1 hch.1 hk hC
+    exact card_le_of_mem_countingChild hch.1.1 hch.1.2.1 (hch.1.flower_nonempty hθ) hk hC
 
 /-- Along a node word `w` from a state of width `≤ k` (`1 ≤ k`), the number of clauses increases by
 at most `k * w.length`. -/
-theorem IsNodeWord.card_walk_le (hθ : ∀ j, 1 ≤ θ j) {k : ℕ} (hk1 : 1 ≤ k) {s : σ}
+theorem IsNodeWord.card_walk_le (hθ : ∀ j, 1 ≤ θ j) {k : ℕ} (_hk1 : 1 ≤ k) {s : σ}
     (hk : ∀ C ∈ R.toClauseSet s, C.card ≤ k) {w : List Bool} (hw : R.IsNodeWord s w) :
     (R.toClauseSet (R.walk s w)).card ≤ (R.toClauseSet s).card + k * w.length := by
   induction w generalizing s with
@@ -300,7 +260,7 @@ theorem IsNodeWord.card_walk_le (hθ : ∀ j, 1 ≤ θ j) {k : ℕ} (hk1 : 1 ≤
     have hk_next : ∀ C ∈ R.toClauseSet (R.next s b), C.card ≤ k := by
       intro C hC
       rw [hnext b] at hC
-      exact card_le_of_mem_countingChild hθ hk1 hch.1 hk hC
+      exact card_le_of_mem_countingChild hch.1.1 hch.1.2.1 (hch.1.flower_nonempty hθ) hk hC
     have hcard_next : (R.toClauseSet (R.next s b)).card ≤ (R.toClauseSet s).card + k := by
       rw [hnext b]
       exact card_countingChild_le hθ hch.1 hk b
diff --git a/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingTree.lean b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingTree.lean
index 5c9cbcc123..f6d3b464eb 100644
--- a/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingTree.lean
+++ b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingTree.lean
@@ -121,7 +121,10 @@ private theorem reduced_countingChild (ψ : ClauseSet V) (c : ℕ) (H : Finset (
     (b : Bool) : Reduced (countingChild ψ c H b) := by
   cases b <;> exact reduced_reduce _
 
-private theorem disjoint_flower_countingChild (ψ : ClauseSet V) {c : ℕ} {H : Finset (Literal V)}
+/-- The flower `flower ψ c H` is disjoint from both counting children `countingChild ψ c H b`:
+on `false` every flower clause strictly contains `H`, and on `true` every flower clause `C`
+strictly contains its petal `C \ H`. -/
+theorem disjoint_flower_countingChild (ψ : ClauseSet V) {c : ℕ} {H : Finset (Literal V)}
     (h1 : 1 ≤ H.card) (hlt : H.card < c) (b : Bool) :
     Disjoint (flower ψ c H) (countingChild ψ c H b) := by
   rw [Finset.disjoint_left]
@@ -140,7 +143,8 @@ private theorem disjoint_flower_countingChild (ψ : ClauseSet V) {c : ℕ} {H :
     refine hmin (C \ H) ?_ (sdiff_ssubset hHC (card_pos.mp h1))
     exact mem_union_left _ (mem_union_right _ (mem_petals.mpr ⟨C, hC, rfl⟩))
 
-private theorem card_le_of_mem_countingChild {ψ : ClauseSet V} {c k : ℕ} {H : Finset (Literal V)}
+/-- Counting children keep the clause width `≤ k` when the flower `flower ψ c H` is nonempty. -/
+theorem card_le_of_mem_countingChild {ψ : ClauseSet V} {c k : ℕ} {H : Finset (Literal V)}
     (h1 : 1 ≤ H.card) (hlt : H.card < c) (hF : (flower ψ c H).Nonempty)
     (hk : ∀ C ∈ ψ, C.card ≤ k) {b : Bool} {C : Finset (Literal V)}
     (hC : C ∈ countingChild ψ c H b) : C.card ≤ k := by
diff --git a/ComplexityTests/Consolidation.lean b/ComplexityTests/Consolidation.lean
index 442b959932..3c4ed7c2bf 100644
--- a/ComplexityTests/Consolidation.lean
+++ b/ComplexityTests/Consolidation.lean
@@ -11,6 +11,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Universal.PolyTime
 import Complexity.Foundations.Control.Monad.IsMonadHom.StateT
 import Complexity.Foundations.Data.BitString.Affine
 import Complexity.Foundations.Data.BitString.Parity
+import Complexity.Foundations.Data.BitString.WordCount
 import Complexity.Foundations.Data.Fin.Order
 import Complexity.Foundations.Data.Finset.Average
 import Complexity.Foundations.Data.List.Filter
@@ -20,6 +21,7 @@ import Complexity.Foundations.Data.Nat.Choose.Real
 import Complexity.Foundations.Data.Nat.Div
 import Complexity.Foundations.Data.Nat.Log
 import Complexity.Foundations.Data.Nat.PolynomialBound.Log
+import Complexity.Foundations.Geometry.Orthogonal
 import Complexity.Foundations.LinearAlgebra.CubeSum
 import Complexity.Foundations.LinearAlgebra.Matrix.SchurComplement
 import Complexity.Foundations.LinearAlgebra.Rank
@@ -253,4 +255,19 @@ example :
     simp only [decide_eq_true_eq] at hp
     exact hp
 
+/-- Monotonicity of `List.any` and `List.all` under `List.Forall₂ (· ≤ ·)`. -/
+example : [false, true].any id ≤ [true, true].any id ∧
+    [false, true].all id ≤ [true, true].all id :=
+  ⟨List.any_id_le_of_forall₂ (by decide), List.all_id_le_of_forall₂ (by decide)⟩
+
+/-- A bit string has no `true` bits in `List.ofFn` iff it is zero. -/
+example (w : Fin 3 → Bool) :
+    (!(List.ofFn w).any fun b => b) = true ↔ w = 0 :=
+  Cslib.BitString.not_any_ofFn_eq_true_iff w
+
+/-- The continuous support of a two-point route `[a, b]` equals `segment a b`. -/
+example (a b : Orthogonal.Point) :
+    Orthogonal.support [a, b] = Orthogonal.segment a b :=
+  Orthogonal.support_pair a b
+
 end ComplexityTests.Consolidation