diff --git a/LeanPool/ACMax/AHL/AHLAmGm.lean b/LeanPool/ACMax/AHL/AHLAmGm.lean
index 1fc5a30825..3afa5b14c1 100644
--- a/LeanPool/ACMax/AHL/AHLAmGm.lean
+++ b/LeanPool/ACMax/AHL/AHLAmGm.lean
@@ -8,7 +8,6 @@ module
 public import LeanPool.ACMax.AHL.AHLMarginals
 public import Mathlib.Analysis.MeanInequalities
 public import Mathlib.Analysis.Convex.Deriv
-public import Mathlib.Analysis.Convex.Jensen
 public import Mathlib.Analysis.SpecialFunctions.Log.Deriv
 
 /-!
diff --git a/LeanPool/ACMax/AHL/NBWalk.lean b/LeanPool/ACMax/AHL/NBWalk.lean
index 33ec2e7b6a..a97b89b9f6 100644
--- a/LeanPool/ACMax/AHL/NBWalk.lean
+++ b/LeanPool/ACMax/AHL/NBWalk.lean
@@ -6,7 +6,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 module
 
 public import Mathlib.Combinatorics.SimpleGraph.Paths
-public import Mathlib.Combinatorics.SimpleGraph.Finite
 
 /-!
 # Non-backtracking walks — the foundation of the AHL irregular-Moore ladder
diff --git a/LeanPool/ACMax/AHL/NBWalkCount.lean b/LeanPool/ACMax/AHL/NBWalkCount.lean
index 286ea72bc2..829b259e41 100644
--- a/LeanPool/ACMax/AHL/NBWalkCount.lean
+++ b/LeanPool/ACMax/AHL/NBWalkCount.lean
@@ -6,7 +6,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 module
 
 public import Mathlib.Combinatorics.SimpleGraph.Walk.Counting
-public import Mathlib.Combinatorics.SimpleGraph.Finite
 public import Mathlib.Algebra.Order.BigOperators.Group.Finset
 public import LeanPool.ACMax.AHL.NBWalk
 
diff --git a/LeanPool/ACMax/AHL/NBWeighted.lean b/LeanPool/ACMax/AHL/NBWeighted.lean
index 0780c763e1..24d33d65a3 100644
--- a/LeanPool/ACMax/AHL/NBWeighted.lean
+++ b/LeanPool/ACMax/AHL/NBWeighted.lean
@@ -6,7 +6,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 module
 
 public import LeanPool.ACMax.AHL.NBWalkCount
-public import Mathlib.Combinatorics.SimpleGraph.Walk.Operations
 public import Mathlib.Algebra.Order.Chebyshev
 
 /-!
diff --git a/LeanPool/ACMax/Band/AssemblyAllRange.lean b/LeanPool/ACMax/Band/AssemblyAllRange.lean
index 444e28782b..e5b9fad866 100644
--- a/LeanPool/ACMax/Band/AssemblyAllRange.lean
+++ b/LeanPool/ACMax/Band/AssemblyAllRange.lean
@@ -9,7 +9,6 @@ public import LeanPool.ACMax.Band.CertAllRange
 public import LeanPool.ACMax.Band.KillSharp
 public import LeanPool.ACMax.Band.Rows
 public import LeanPool.ACMax.Counting.MEdgeSparse
-public import LeanPool.ACMax.Cuts.LowDegreeVertex
 public import LeanPool.ACMax.Spectral.AlgConnK2
 
 /-!
diff --git a/LeanPool/ACMax/Band/CertAllRange.lean b/LeanPool/ACMax/Band/CertAllRange.lean
index ded371c9ee..a078c92872 100644
--- a/LeanPool/ACMax/Band/CertAllRange.lean
+++ b/LeanPool/ACMax/Band/CertAllRange.lean
@@ -278,8 +278,8 @@ theorem band_cert_uniform_ge_48 (n X h : ℕ)
     have hsquare : 43 * t ≤ t * t := Nat.mul_le_mul_right t ht43
     have hlinear : 10 * v + 1 + 9 * t ≤ 43 * t := by omega
     have hpoly : 10 * v + 1 + 9 * t ≤ t * t := hlinear.trans hsquare
-    have hA : t * (v - 1) + 1 ≤ (t - 10) * (v + t) := by
-      nlinarith
+    have hA : t * (v - 1) + 1 ≤ (t - 10) * (v + t) :=
+      uniform_count_bound t v ht10 hv hpoly
     change t * (v - 1) * v ^ ell <
       (v + t) * ((v + 2 * t) ^ ell - v ^ ell)
     exact sum_cert_of_power ht10 hA hpower hv
diff --git a/LeanPool/ACMax/Band/CertUniform.lean b/LeanPool/ACMax/Band/CertUniform.lean
index 65a3f709bd..b2942d5b2d 100644
--- a/LeanPool/ACMax/Band/CertUniform.lean
+++ b/LeanPool/ACMax/Band/CertUniform.lean
@@ -6,7 +6,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 module
 
 public import Mathlib.Tactic.Linarith
-public import Mathlib.Tactic.NormNum
 public import Mathlib.Tactic.Ring
 public import Mathlib.Tactic.Positivity
 
@@ -88,7 +87,8 @@ theorem uniform_power_four (t v : ℕ)
     dsimp [u, A] at *
     linarith
   have hcoef : 0 ≤ 773272 - 81 * u ^ 2 - 5297 * u := by
-    nlinarith [sq_nonneg (u - 36), sq_nonneg u]
+    have hsq := pow_le_pow_left₀ hu0 hu36 2
+    nlinarith only [hsq, hu36]
   have hgap :
       0 ≤ (A + 10 * T) ^ 4 - (T - 9) * A ^ 4 := by
     have hid :
@@ -98,10 +98,14 @@ theorem uniform_power_four (t v : ℕ)
       dsimp [A, u, T]
       ring
     rw [hid]
+    clear_value u
+    clear * - hu0 hcoef
     positivity
   have hend : (T - 9) * A ^ 4 ≤ (A + 10 * T) ^ 4 := by linarith
   have hcross : (A + 10 * T) * (5 * V) ≤ (5 * V + 10 * T) * A := by
-    nlinarith
+    have hmonotone := mul_le_mul_of_nonneg_left hVA
+      (show 0 ≤ 10 * T by linarith only [hT43])
+    nlinarith only [hmonotone]
   have hcross4 := pow_le_pow_left₀ (by positivity) hcross 4
   have hcross4' :
       (A + 10 * T) ^ 4 * (5 * V) ^ 4 ≤
@@ -173,6 +177,8 @@ theorem uniform_cubic_arith (t v ell : ℕ)
   have hb79 : b ≤ 79 := by dsimp [b]; linarith
   have hLa : L = a + 5 := by dsimp [a]; ring
   have hTb : T = b + 43 := by dsimp [b]; ring
+  -- Keep positivity in the shifted coordinates instead of expanding their definitions.
+  clear_value a b
   have hbracket :
       0 ≤ 4 * L ^ 3 - 6 * L ^ 2 + 8 * L - 3 * T + 30 := by
     have hid :
@@ -207,6 +213,7 @@ theorem uniform_cubic_arith (t v ell : ℕ)
       rw [hLa, hTb]
       ring
     rw [hid]
+    clear * - ha0 hb0 hcoef
     positivity
   let Q : ℤ :=
     (T - 10) * (A + X) + 5 * T * (T - 2 * L - 10)
@@ -214,7 +221,9 @@ theorem uniform_cubic_arith (t v ell : ℕ)
     have hAX : 10 * T ≤ A + X := by linarith
     have hcore : 0 ≤ 3 * T - 2 * L - 30 := by linarith
     dsimp [Q]
-    nlinarith
+    have hproduct := mul_le_mul_of_nonneg_left hAX (show 0 ≤ T - 10 by omega)
+    have hnonneg := mul_nonneg (show 0 ≤ 5 * T by omega) hcore
+    nlinarith only [hproduct, hnonneg]
   have hPX : 0 ≤ P X := by
     by_cases heq : A = 5 * T
     · have hX : X = 5 * T := by linarith
@@ -229,7 +238,15 @@ theorem uniform_cubic_arith (t v ell : ℕ)
         ring
       have hmul : 0 ≤ (A - 5 * T) * P X := by
         rw [hchord]
-        positivity
+        exact add_nonneg
+          (add_nonneg (mul_nonneg (sub_nonneg.mpr hXA) hPlo)
+            (mul_nonneg (sub_nonneg.mpr hTX) hPhi))
+          (mul_nonneg
+            (mul_nonneg
+              (mul_nonneg
+                (mul_nonneg (by norm_num) hwidth.le)
+                (sub_nonneg.mpr hXA))
+              (sub_nonneg.mpr hTX)) hQ)
       exact nonneg_of_mul_nonneg_right hmul hwidth
   have hdesiredZ :
       3 * (T - 10) * V ^ 3 ≤
@@ -331,6 +348,13 @@ theorem uniform_region_bounds (n X h : ℕ)
   dsimp
   omega
 
+/-- Convert the quadratic census bound into the strict power-certificate coefficient. -/
+theorem uniform_count_bound (t v : ℕ) (ht10 : 10 ≤ t) (hv : 1 ≤ v)
+    (hpoly : 10 * v + 1 + 9 * t ≤ t * t) :
+    t * (v - 1) + 1 ≤ (t - 10) * (v + t) := by
+  zify [ht10, hv] at hpoly ⊢
+  nlinarith only [hpoly]
+
 theorem sum_cert_of_power {t v ell : ℕ}
     (ht10 : 10 ≤ t)
     (hA : t * (v - 1) + 1 ≤ (t - 10) * (v + t))
@@ -391,8 +415,8 @@ theorem band_cert_uniform_48_122 (n X h : ℕ)
   have hsquare : 43 * t ≤ t * t := Nat.mul_le_mul_right t ht43
   have hlinear : 10 * v + 1 + 9 * t ≤ 43 * t := by omega
   have hpoly : 10 * v + 1 + 9 * t ≤ t * t := hlinear.trans hsquare
-  have hA : t * (v - 1) + 1 ≤ (t - 10) * (v + t) := by
-    nlinarith
+  have hA : t * (v - 1) + 1 ≤ (t - 10) * (v + t) :=
+    uniform_count_bound t v ht10 hv hpoly
   have hpower := uniform_power_certificate t v ell
     ht43 htv hv122 hell4 hell10 hlin
   change t * (v - 1) * v ^ ell <
diff --git a/LeanPool/ACMax/Counting/Arithmetic.lean b/LeanPool/ACMax/Counting/Arithmetic.lean
new file mode 100644
index 0000000000..339c51f9f9
--- /dev/null
+++ b/LeanPool/ACMax/Counting/Arithmetic.lean
@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2026 Zeru Zhu, Jinzheng Li, Yuanjie Ren and OpenAI. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren, OpenAI
+-/
+module
+
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.Positivity
+public import Mathlib.Tactic.Ring
+
+/-!
+# Scalar certificates for the sharp Moore bound
+
+Keeping these integer arguments independent of graph definitions lets them elaborate
+while the graph infrastructure builds.
+-/
+
+@[expose] public section
+
+namespace ACMax.Arithmetic
+
+open Classical in
+/-- **The sharp strip cubic.**  The single-variable inequality the `n ≥ 123` region arithmetic
+bottoms out at, after `X` is pushed to its master maximum and `H` to the end of its range.
+Substituting `N = 123 + u` makes every coefficient non-negative
+(`1068496017 + 1122649307u + 11552736u² + 20700u³`), giving an explicit positive certificate. -/
+theorem strip_cubic_sharp {N : ℤ} (hN : 123 ≤ N) :
+    779812849 * N + 755972700 < 20700 * N ^ 3 + 3914436 * N ^ 2 := by
+  have hu : (0 : ℤ) ≤ N - 123 := by linarith
+  have hidentity :
+      20700 * N ^ 3 + 3914436 * N ^ 2 - (779812849 * N + 755972700) =
+        1068496017 + 1122649307 * (N - 123) +
+          11552736 * (N - 123) ^ 2 + 20700 * (N - 123) ^ 3 := by ring
+  apply sub_pos.mp
+  rw [hidentity]
+  positivity
+
+open Classical in
+/-- **The two-variable core.**  After both `X`-eliminations the target is a cubic in `(N, H)`:
+
+  `4608000·(N−H)² < 38400·(N−H)·(Q+120) + 23·P·Q²`,  `P = 6N+160−23H`, `Q = 16N+7H−150`.
+
+Every `H`-coefficient of the gap is negative at `N ≥ 123`, so the minimum is at `17H = 4N − 200`,
+and `4913·gap − cubic` is *identically* `289(M−17H)(−c₁) + 17(M²−(17H)²)(−c₂) + (M³−(17H)³)·25921`
+with `M = 4N − 200`, `−c₁ = 104512N² − 11944120N + 18478500 ≥ 0` (its larger root is `≈ 112.7`)
+and `−c₂ = 111734N + 3585580 ≥ 0`.  So `linarith` closes on those three products plus the cubic. -/
+theorem moore_strip_twovar_sharp {N H : ℤ} (hN : 123 ≤ N) (hH : 0 ≤ H)
+    (hs : 17 * H ≤ 4 * N - 200) :
+    4608000 * (N - H) ^ 2
+      < 38400 * ((N - H) * (16 * N + 7 * H - 30))
+        + 23 * ((6 * N + 160 - 23 * H) * (16 * N + 7 * H - 150) ^ 2) := by
+  have hd : (0 : ℤ) ≤ (4 * N - 200) - 17 * H := by linarith
+  have hHm : (0 : ℤ) ≤ 17 * H := by linarith
+  have hnc1 : (0 : ℤ) ≤ 104512 * N ^ 2 - 11944120 * N + 18478500 := by
+    have hidentity :
+        104512 * N ^ 2 - 11944120 * N + 18478500 =
+          104512 * (N - 123) ^ 2 + 13765832 * (N - 123) + 130513788 := by ring
+    rw [hidentity]
+    have hu : (0 : ℤ) ≤ N - 123 := sub_nonneg.mpr hN
+    positivity
+  have hnc2 : (0 : ℤ) ≤ 111734 * N + 3585580 := by linarith
+  have hsq : (0 : ℤ) ≤ (4 * N - 200) ^ 2 + 17 * H * (4 * N - 200) + (17 * H) ^ 2 := by
+    exact add_nonneg (add_nonneg (sq_nonneg _)
+      (mul_nonneg hHm (by linarith only [hd, hHm]))) (sq_nonneg _)
+  have e1 := mul_nonneg hd hnc1
+  have e2 := mul_nonneg (mul_nonneg hd (by linarith : (0 : ℤ) ≤ (4 * N - 200) + 17 * H)) hnc2
+  have e3 := mul_nonneg (mul_nonneg hd hsq) (by norm_num : (0 : ℤ) ≤ 25921)
+  have hcub := strip_cubic_sharp hN
+  linarith only [e1, e2, e3, hcub]
+
+open Classical in
+/-- **The `R`-free core of the sharp strip discharge.**  On the counting region
+(`0 ≤ H ≤ X`, `10X + 7H ≤ 4N − 200`) at `N ≥ 123`,
+
+  `4608·(N−H)² < 384·(N−H)·(2N−X−23) + 23·(N−4−X−3H)·(2N−X−35)²`.
+
+Both `X`-dependent factors are pushed to the master maximum simultaneously — `10·t ≥ 6N+160−23H`
+and `10·A ≥ 16N+7H−150`, equalities together at `X = X_max` — and `moore_strip_twovar_sharp`
+closes what is left. -/
+theorem moore_strip_core_sharp {N X H : ℤ} (hN : 123 ≤ N) (hH : 0 ≤ H) (hHX : H ≤ X)
+    (hmaster : 10 * X + 7 * H ≤ 4 * N - 200) :
+    4608 * (N - H) ^ 2
+      < 384 * ((N - H) * (2 * N - X - 23))
+        + 23 * ((N - 4 - X - 3 * H) * (2 * N - X - 35) ^ 2) := by
+  have h17 : 17 * H ≤ 4 * N - 200 := by linarith
+  have hvpos : (0 : ℤ) ≤ N - H := by linarith
+  have hPpos : (0 : ℤ) ≤ 6 * N + 160 - 23 * H := by linarith
+  have hQpos : (0 : ℤ) ≤ 16 * N + 7 * H - 150 := by linarith
+  have hP : 6 * N + 160 - 23 * H ≤ 10 * (N - 4 - X - 3 * H) := by linarith
+  have hQ : 16 * N + 7 * H - 150 ≤ 10 * (2 * N - X - 35) := by linarith
+  -- the ball factor, pushed to the master maximum
+  have hA : 38400 * ((N - H) * (16 * N + 7 * H - 30))
+      ≤ 1000 * (384 * ((N - H) * (2 * N - X - 23))) := by
+    convert mul_le_mul_of_nonneg_left (add_le_add_right hQ 120)
+      (mul_nonneg (by norm_num : (0 : ℤ) ≤ 38400) hvpos) using 1 <;> ring
+  -- the excess factor, pushed to the master maximum
+  have hQ2 : (16 * N + 7 * H - 150) ^ 2 ≤ (10 * (2 * N - X - 35)) ^ 2 := by
+    exact pow_le_pow_left₀ hQpos hQ 2
+  have hmul : (6 * N + 160 - 23 * H) * (16 * N + 7 * H - 150) ^ 2
+      ≤ (10 * (N - 4 - X - 3 * H)) * (10 * (2 * N - X - 35)) ^ 2 :=
+    mul_le_mul hP hQ2 (sq_nonneg _) (by linarith)
+  have hB : 23 * ((6 * N + 160 - 23 * H) * (16 * N + 7 * H - 150) ^ 2)
+      ≤ 1000 * (23 * ((N - 4 - X - 3 * H) * (2 * N - X - 35) ^ 2)) := by
+    convert mul_le_mul_of_nonneg_left hmul (by norm_num : (0 : ℤ) ≤ 23) using 1; ring
+  have htv := moore_strip_twovar_sharp hN hH h17
+  linarith only [hA, hB, htv]
+
+end ACMax.Arithmetic
diff --git a/LeanPool/ACMax/Counting/Cherry.lean b/LeanPool/ACMax/Counting/Cherry.lean
index 4b0c486acc..32bb6700cf 100644
--- a/LeanPool/ACMax/Counting/Cherry.lean
+++ b/LeanPool/ACMax/Counting/Cherry.lean
@@ -5,9 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Push
-public import Mathlib.Tactic.Ring
 public import LeanPool.ACMax.Counting.PoorCorner
 
 /-!
diff --git a/LeanPool/ACMax/Counting/CherryMShape.lean b/LeanPool/ACMax/Counting/CherryMShape.lean
index e6fef0fdeb..915decc07f 100644
--- a/LeanPool/ACMax/Counting/CherryMShape.lean
+++ b/LeanPool/ACMax/Counting/CherryMShape.lean
@@ -5,11 +5,7 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Push
-public import Mathlib.Tactic.Ring
 public import LeanPool.ACMax.Counting.Cherry
-public import LeanPool.ACMax.Counting.PoorCorner
 
 /-!
 # The M-shape analysis and the complete `Δ ≤ 4` closure
diff --git a/LeanPool/ACMax/Counting/CompactCell.lean b/LeanPool/ACMax/Counting/CompactCell.lean
index 731703a8fe..89d09253e0 100644
--- a/LeanPool/ACMax/Counting/CompactCell.lean
+++ b/LeanPool/ACMax/Counting/CompactCell.lean
@@ -6,7 +6,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 module
 
 public import LeanPool.ACMax.Counting.CherryMShape
-public import LeanPool.ACMax.Reduction.Reduction
 
 /-!
 # The compact-cell reduction of the `Δ ≥ 5` fat side
diff --git a/LeanPool/ACMax/Counting/CompactLedgers.lean b/LeanPool/ACMax/Counting/CompactLedgers.lean
index 8079dfb0ce..3f4f73e243 100644
--- a/LeanPool/ACMax/Counting/CompactLedgers.lean
+++ b/LeanPool/ACMax/Counting/CompactLedgers.lean
@@ -5,14 +5,7 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.IntervalCases
-public import Mathlib.Tactic.Linarith
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Push
-public import Mathlib.Tactic.Ring
-public import Mathlib.Tactic.Tauto
 public import LeanPool.ACMax.Counting.CompactCell
-public import LeanPool.ACMax.Counting.DoubleStar
 
 /-!
 # Compact-cell counting ledgers
diff --git a/LeanPool/ACMax/Counting/DecoratedC4.lean b/LeanPool/ACMax/Counting/DecoratedC4.lean
index a88f682298..26cbf2c8f5 100644
--- a/LeanPool/ACMax/Counting/DecoratedC4.lean
+++ b/LeanPool/ACMax/Counting/DecoratedC4.lean
@@ -5,7 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.NormNum
 public import LeanPool.ACMax.Counting.SparseCore
 
 /-!
diff --git a/LeanPool/ACMax/Counting/DoubleStar.lean b/LeanPool/ACMax/Counting/DoubleStar.lean
index 0ace5c8087..398a454be7 100644
--- a/LeanPool/ACMax/Counting/DoubleStar.lean
+++ b/LeanPool/ACMax/Counting/DoubleStar.lean
@@ -5,8 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Tauto
 public import LeanPool.ACMax.InternalEdgesEven
 public import LeanPool.ACMax.Reduction.Residual
 
diff --git a/LeanPool/ACMax/Counting/FarPair.lean b/LeanPool/ACMax/Counting/FarPair.lean
index 6498f2d209..dfad998df5 100644
--- a/LeanPool/ACMax/Counting/FarPair.lean
+++ b/LeanPool/ACMax/Counting/FarPair.lean
@@ -5,11 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.Linarith
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Positivity
-public import Mathlib.Tactic.Ring
-public import Mathlib.Tactic.Tauto
 public import LeanPool.ACMax.Spectral.TestVector
 
 /-!
@@ -164,7 +159,7 @@ private theorem algConn_le_two_of_weighted_double_star_hterm : ∀ {V : Type u_1
         ite_eq_left ⟨hadj, hiu⟩
       have hxi : x i = au := by rw [hiu]; exact hxu
       rw [hxi, hxA j hjA]
-      linarith [nn2, nn3, nn4, nn5, nn6, nn7, nn8, nn9, nn10]
+      linarith only [nn2, nn3, nn4, nn5, nn6, nn7, nn8, nn9, nn10, e1]
     · by_cases hju : j = u
       · -- `N(u) → u` edge.
         have hiA : i ∈ A := (hmemA i).mpr (G.adj_symm (hju ▸ hadj))
@@ -173,7 +168,7 @@ private theorem algConn_le_two_of_weighted_double_star_hterm : ∀ {V : Type u_1
         have hxj : x j = au := by rw [hju]; exact hxu
         have hval : (p i - au) ^ 2 = (au - p i) ^ 2 := by ring
         rw [hxj, hxA i hiA, hval]
-        linarith [nn1, nn3, nn4, nn5, nn6, nn7, nn8, nn9, nn10]
+        linarith only [nn1, nn3, nn4, nn5, nn6, nn7, nn8, nn9, nn10, e2]
       · by_cases hiv : i = v
         · -- `v → N(v)` edge.
           have hjB : j ∈ B := (hmemB j).mpr (hiv ▸ hadj)
@@ -182,7 +177,7 @@ private theorem algConn_le_two_of_weighted_double_star_hterm : ∀ {V : Type u_1
           have hxi : x i = -av := by rw [hiv]; exact hxv
           have hval : (-av - -(q j)) ^ 2 = (av - q j) ^ 2 := by ring
           rw [hxi, hxB j hjB, hval]
-          linarith [nn1, nn2, nn4, nn5, nn6, nn7, nn8, nn9, nn10]
+          linarith only [nn1, nn2, nn4, nn5, nn6, nn7, nn8, nn9, nn10, e3]
         · by_cases hjv : j = v
           · -- `N(v) → v` edge.
             have hiB : i ∈ B := (hmemB i).mpr (G.adj_symm (hjv ▸ hadj))
@@ -191,7 +186,7 @@ private theorem algConn_le_two_of_weighted_double_star_hterm : ∀ {V : Type u_1
             have hxj : x j = -av := by rw [hjv]; exact hxv
             have hval : (-(q i) - -av) ^ 2 = (av - q i) ^ 2 := by ring
             rw [hxj, hxB i hiB, hval]
-            linarith [nn1, nn2, nn3, nn5, nn6, nn7, nn8, nn9, nn10]
+            linarith only [nn1, nn2, nn3, nn5, nn6, nn7, nn8, nn9, nn10, e4]
           · -- Neither endpoint is a centre.
             by_cases hiA : i ∈ A
             · by_cases hjB : j ∈ B
@@ -200,7 +195,7 @@ private theorem algConn_le_two_of_weighted_double_star_hterm : ∀ {V : Type u_1
                     = (p i + q j) ^ 2 := ite_eq_left ⟨hadj, hiA, hjB⟩
                 have hval : (p i - -(q j)) ^ 2 = (p i + q j) ^ 2 := by ring
                 rw [hxA i hiA, hxB j hjB, hval]
-                linarith [nn1, nn2, nn3, nn4, nn6, nn7, nn8, nn9, nn10]
+                linarith only [nn1, nn2, nn3, nn4, nn6, nn7, nn8, nn9, nn10, e5]
               · by_cases hjA : j ∈ A
                 · -- internal `N(u)` edge: charge both slots.
                   have e7 : (if G.Adj i j ∧ i ∈ A ∧ j ≠ u ∧ j ∉ B then p i ^ 2 else 0)
@@ -210,13 +205,13 @@ private theorem algConn_le_two_of_weighted_double_star_hterm : ∀ {V : Type u_1
                   have hb : (p i - p j) ^ 2 ≤ p i ^ 2 + p j ^ 2 := by
                     nlinarith only [mul_nonneg (hp i hiA) (hp j hjA)]
                   rw [hxA i hiA, hxA j hjA]
-                  linarith [nn1, nn2, nn3, nn4, nn5, nn6, nn9, nn10]
+                  linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn9, nn10, e7, e8, hb]
                 · -- leak `N(u) → Z`.
                   have e7 : (if G.Adj i j ∧ i ∈ A ∧ j ≠ u ∧ j ∉ B then p i ^ 2 else 0)
                       = p i ^ 2 := ite_eq_left ⟨hadj, hiA, hju, hjB⟩
                   have hval : (p i - 0) ^ 2 = p i ^ 2 := by ring
                   rw [hxA i hiA, hxZ j hju hjv hjA hjB, hval]
-                  linarith [nn1, nn2, nn3, nn4, nn5, nn6, nn8, nn9, nn10]
+                  linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn8, nn9, nn10, e7]
             · by_cases hiB : i ∈ B
               · by_cases hjA : j ∈ A
                 · -- cross edge `N(v) → N(u)`.
@@ -224,7 +219,7 @@ private theorem algConn_le_two_of_weighted_double_star_hterm : ∀ {V : Type u_1
                       = (p j + q i) ^ 2 := ite_eq_left ⟨hadj, hiB, hjA⟩
                   have hval : (-(q i) - p j) ^ 2 = (p j + q i) ^ 2 := by ring
                   rw [hxB i hiB, hxA j hjA, hval]
-                  linarith [nn1, nn2, nn3, nn4, nn5, nn7, nn8, nn9, nn10]
+                  linarith only [nn1, nn2, nn3, nn4, nn5, nn7, nn8, nn9, nn10, e6]
                 · by_cases hjB : j ∈ B
                   · -- internal `N(v)` edge.
                     have e9 : (if G.Adj i j ∧ i ∈ B ∧ j ≠ v ∧ j ∉ A then q i ^ 2 else 0)
@@ -234,31 +229,31 @@ private theorem algConn_le_two_of_weighted_double_star_hterm : ∀ {V : Type u_1
                     have hb : (-(q i) - -(q j)) ^ 2 ≤ q i ^ 2 + q j ^ 2 := by
                       nlinarith only [mul_nonneg (hq i hiB) (hq j hjB)]
                     rw [hxB i hiB, hxB j hjB]
-                    linarith [nn1, nn2, nn3, nn4, nn5, nn6, nn7, nn8]
+                    linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn7, nn8, e9, e10, hb]
                   · -- leak `N(v) → Z`.
                     have e9 : (if G.Adj i j ∧ i ∈ B ∧ j ≠ v ∧ j ∉ A then q i ^ 2 else 0)
                         = q i ^ 2 := ite_eq_left ⟨hadj, hiB, hjv, hjA⟩
                     have hval : (-(q i) - 0) ^ 2 = q i ^ 2 := by ring
                     rw [hxB i hiB, hxZ j hju hjv hjA hjB, hval]
-                    linarith [nn1, nn2, nn3, nn4, nn5, nn6, nn7, nn8, nn10]
+                    linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn7, nn8, nn10, e9]
               · by_cases hjA : j ∈ A
                 · -- leak `Z → N(u)`.
                   have e8 : (if G.Adj i j ∧ j ∈ A ∧ i ≠ u ∧ i ∉ B then p j ^ 2 else 0)
                       = p j ^ 2 := ite_eq_left ⟨hadj, hjA, hiu, hiB⟩
                   have hval : (0 - p j) ^ 2 = p j ^ 2 := by ring
                   rw [hxZ i hiu hiv hiA hiB, hxA j hjA, hval]
-                  linarith [nn1, nn2, nn3, nn4, nn5, nn6, nn7, nn9, nn10]
+                  linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn7, nn9, nn10, e8]
                 · by_cases hjB : j ∈ B
                   · -- leak `Z → N(v)`.
                     have e10 : (if G.Adj i j ∧ j ∈ B ∧ i ≠ v ∧ i ∉ A then q j ^ 2 else 0)
                         = q j ^ 2 := ite_eq_left ⟨hadj, hjB, hiv, hiA⟩
                     have hval : (0 - -(q j)) ^ 2 = q j ^ 2 := by ring
                     rw [hxZ i hiu hiv hiA hiB, hxB j hjB, hval]
-                    linarith [nn1, nn2, nn3, nn4, nn5, nn6, nn7, nn8, nn9]
+                    linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn7, nn8, nn9, e10]
                   · -- `Z → Z`: zero.
                     rw [hxZ i hiu hiv hiA hiB, hxZ j hju hjv hjA hjB]
                     norm_num
-                    linarith [nn1, nn2, nn3, nn4, nn5, nn6, nn7, nn8, nn9, nn10]
+                    linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn7, nn8, nn9, nn10]
   · simp [hadj]
 
 open Classical in
@@ -679,33 +674,30 @@ private theorem algConn_le_two_of_apex_double_star_hterm : ∀ {V : Type u_1} [F
         have e11 : (if i = u ∧ j = g then au ^ 2 else 0) = au ^ 2 := ite_eq_left ⟨hiu, hjg⟩
         have hxi : x i = au := by rw [hiu]; exact hxu
         have hxj : x j = 0 := by rw [hjg]; exact hxg
-        have hval : (au - 0) ^ 2 = au ^ 2 := by ring
-        rw [hxi, hxj, hval]
-        linarith
+        rw [hxi, hxj, sub_zero]
+        linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn7, nn8, nn9, nn10, nn12, nn13, nn14, e11]
       · -- `u → A` edge.
         have hjA : j ∈ A := (hmemA j).mpr ⟨hjg, hiu ▸ hadj⟩
         have e1 : (if i = u ∧ j ∈ A then (au - p j) ^ 2 else 0) = (au - p j) ^ 2 :=
           ite_eq_left ⟨hiu, hjA⟩
         have hxi : x i = au := by rw [hiu]; exact hxu
         rw [hxi, hxA j hjA]
-        linarith
+        linarith only [nn2, nn3, nn4, nn5, nn6, nn7, nn8, nn9, nn10, nn11, nn12, nn13, nn14, e1]
     · by_cases hju : j = u
       · by_cases hig : i = g
         · -- apex edge `g → u`.
           have e12 : (if j = u ∧ i = g then au ^ 2 else 0) = au ^ 2 := ite_eq_left ⟨hju, hig⟩
           have hxi : x i = 0 := by rw [hig]; exact hxg
           have hxj : x j = au := by rw [hju]; exact hxu
-          have hval : ((0:ℝ) - au) ^ 2 = au ^ 2 := by ring
-          rw [hxi, hxj, hval]
-          linarith
+          rw [hxi, hxj, zero_sub, neg_sq]
+          linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn7, nn8, nn9, nn10, nn11, nn13, nn14, e12]
         · -- `A → u` edge.
           have hiA : i ∈ A := (hmemA i).mpr ⟨hig, G.adj_symm (hju ▸ hadj)⟩
           have e2 : (if j = u ∧ i ∈ A then (au - p i) ^ 2 else 0) = (au - p i) ^ 2 :=
             ite_eq_left ⟨hju, hiA⟩
           have hxj : x j = au := by rw [hju]; exact hxu
-          have hval : (p i - au) ^ 2 = (au - p i) ^ 2 := by ring
-          rw [hxj, hxA i hiA, hval]
-          linarith
+          rw [hxj, hxA i hiA, sub_sq_comm (p i) au]
+          linarith only [nn1, nn3, nn4, nn5, nn6, nn7, nn8, nn9, nn10, nn11, nn12, nn13, nn14, e2]
       · by_cases hiv : i = v
         · by_cases hjg : j = g
           · -- apex edge `v → g`.
@@ -713,9 +705,8 @@ private theorem algConn_le_two_of_apex_double_star_hterm : ∀ {V : Type u_1} [F
               ite_eq_left ⟨hiv, hjg⟩
             have hxi : x i = -av := by rw [hiv]; exact hxv
             have hxj : x j = 0 := by rw [hjg]; exact hxg
-            have hval : (-av - 0) ^ 2 = av ^ 2 := by ring
-            rw [hxi, hxj, hval]
-            linarith
+            rw [hxi, hxj, sub_zero, neg_sq]
+            linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn7, nn8, nn9, nn10, nn11, nn12, nn14, e13]
           · -- `v → B` edge.
             have hjB : j ∈ B := (hmemB j).mpr ⟨hjg, hiv ▸ hadj⟩
             have e3 : (if i = v ∧ j ∈ B then (av - q j) ^ 2 else 0) = (av - q j) ^ 2 :=
@@ -723,7 +714,7 @@ private theorem algConn_le_two_of_apex_double_star_hterm : ∀ {V : Type u_1} [F
             have hxi : x i = -av := by rw [hiv]; exact hxv
             have hval : (-av - -(q j)) ^ 2 = (av - q j) ^ 2 := by ring
             rw [hxi, hxB j hjB, hval]
-            linarith
+            linarith only [nn1, nn2, nn4, nn5, nn6, nn7, nn8, nn9, nn10, nn11, nn12, nn13, nn14, e3]
         · by_cases hjv : j = v
           · by_cases hig : i = g
             · -- apex edge `g → v`.
@@ -731,9 +722,9 @@ private theorem algConn_le_two_of_apex_double_star_hterm : ∀ {V : Type u_1} [F
                 ite_eq_left ⟨hjv, hig⟩
               have hxi : x i = 0 := by rw [hig]; exact hxg
               have hxj : x j = -av := by rw [hjv]; exact hxv
-              have hval : ((0:ℝ) - -av) ^ 2 = av ^ 2 := by ring
-              rw [hxi, hxj, hval]
-              linarith
+              rw [hxi, hxj, zero_sub, neg_neg]
+              linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn7,
+                nn8, nn9, nn10, nn11, nn12, nn13, e14]
             · -- `B → v` edge.
               have hiB : i ∈ B := (hmemB i).mpr ⟨hig, G.adj_symm (hjv ▸ hadj)⟩
               have e4 : (if j = v ∧ i ∈ B then (av - q i) ^ 2 else 0)
@@ -741,16 +732,17 @@ private theorem algConn_le_two_of_apex_double_star_hterm : ∀ {V : Type u_1} [F
               have hxj : x j = -av := by rw [hjv]; exact hxv
               have hval : (-(q i) - -av) ^ 2 = (av - q i) ^ 2 := by ring
               rw [hxj, hxB i hiB, hval]
-              linarith
+              linarith only [nn1, nn2, nn3, nn5, nn6, nn7, nn8,
+                nn9, nn10, nn11, nn12, nn13, nn14, e4]
           · -- Neither endpoint is a centre.
             by_cases hiA : i ∈ A
             · by_cases hjB : j ∈ B
               · -- cross edge `A → B`.
                 have e5 : (if G.Adj i j ∧ i ∈ A ∧ j ∈ B then (p i + q j) ^ 2 else 0)
                     = (p i + q j) ^ 2 := ite_eq_left ⟨hadj, hiA, hjB⟩
-                have hval : (p i - -(q j)) ^ 2 = (p i + q j) ^ 2 := by ring
-                rw [hxA i hiA, hxB j hjB, hval]
-                linarith
+                rw [hxA i hiA, hxB j hjB, sub_neg_eq_add]
+                linarith only [nn1, nn2, nn3, nn4, nn6, nn7, nn8,
+                  nn9, nn10, nn11, nn12, nn13, nn14, e5]
               · by_cases hjA : j ∈ A
                 · -- internal `A` edge: charge both slots.
                   have e7 : (if G.Adj i j ∧ i ∈ A ∧ j ≠ u ∧ j ∉ B then p i ^ 2 else 0)
@@ -760,13 +752,14 @@ private theorem algConn_le_two_of_apex_double_star_hterm : ∀ {V : Type u_1} [F
                   have hb : (p i - p j) ^ 2 ≤ p i ^ 2 + p j ^ 2 := by
                     nlinarith only [mul_nonneg (hp i hiA) (hp j hjA)]
                   rw [hxA i hiA, hxA j hjA]
-                  linarith
+                  linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn9,
+                    nn10, nn11, nn12, nn13, nn14, e7, e8, hb]
                 · -- leak `A → Z`.
                   have e7 : (if G.Adj i j ∧ i ∈ A ∧ j ≠ u ∧ j ∉ B then p i ^ 2 else 0)
                       = p i ^ 2 := ite_eq_left ⟨hadj, hiA, hju, hjB⟩
-                  have hval : (p i - 0) ^ 2 = p i ^ 2 := by ring
-                  rw [hxA i hiA, hxZ j hju hjv hjA hjB, hval]
-                  linarith
+                  rw [hxA i hiA, hxZ j hju hjv hjA hjB, sub_zero]
+                  linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn8,
+                    nn9, nn10, nn11, nn12, nn13, nn14, e7]
             · by_cases hiB : i ∈ B
               · by_cases hjA : j ∈ A
                 · -- cross edge `B → A`.
@@ -774,7 +767,8 @@ private theorem algConn_le_two_of_apex_double_star_hterm : ∀ {V : Type u_1} [F
                       = (p j + q i) ^ 2 := ite_eq_left ⟨hadj, hiB, hjA⟩
                   have hval : (-(q i) - p j) ^ 2 = (p j + q i) ^ 2 := by ring
                   rw [hxB i hiB, hxA j hjA, hval]
-                  linarith
+                  linarith only [nn1, nn2, nn3, nn4, nn5, nn7, nn8,
+                    nn9, nn10, nn11, nn12, nn13, nn14, e6]
                 · by_cases hjB : j ∈ B
                   · -- internal `B` edge.
                     have e9 : (if G.Adj i j ∧ i ∈ B ∧ j ≠ v ∧ j ∉ A then q i ^ 2 else 0)
@@ -784,33 +778,35 @@ private theorem algConn_le_two_of_apex_double_star_hterm : ∀ {V : Type u_1} [F
                     have hb : (-(q i) - -(q j)) ^ 2 ≤ q i ^ 2 + q j ^ 2 := by
                       nlinarith only [mul_nonneg (hq i hiB) (hq j hjB)]
                     rw [hxB i hiB, hxB j hjB]
-                    linarith
+                    linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn7,
+                      nn8, nn11, nn12, nn13, nn14, e9, e10, hb]
                   · -- leak `B → Z`.
                     have e9 : (if G.Adj i j ∧ i ∈ B ∧ j ≠ v ∧ j ∉ A then q i ^ 2 else 0)
                         = q i ^ 2 := ite_eq_left ⟨hadj, hiB, hjv, hjA⟩
-                    have hval : (-(q i) - 0) ^ 2 = q i ^ 2 := by ring
-                    rw [hxB i hiB, hxZ j hju hjv hjA hjB, hval]
-                    linarith
+                    rw [hxB i hiB, hxZ j hju hjv hjA hjB, sub_zero, neg_sq]
+                    linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn7,
+                      nn8, nn10, nn11, nn12, nn13, nn14, e9]
               · by_cases hjA : j ∈ A
                 · -- leak `Z → A`.
                   have e8 : (if G.Adj i j ∧ j ∈ A ∧ i ≠ u ∧ i ∉ B then p j ^ 2 else 0)
                       = p j ^ 2 := ite_eq_left ⟨hadj, hjA, hiu, hiB⟩
-                  have hval : (0 - p j) ^ 2 = p j ^ 2 := by ring
-                  rw [hxZ i hiu hiv hiA hiB, hxA j hjA, hval]
-                  linarith
+                  rw [hxZ i hiu hiv hiA hiB, hxA j hjA, zero_sub, neg_sq]
+                  linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn7,
+                    nn9, nn10, nn11, nn12, nn13, nn14, e8]
                 · by_cases hjB : j ∈ B
                   · -- leak `Z → B`.
                     have e10 : (if G.Adj i j ∧ j ∈ B ∧ i ≠ v ∧ i ∉ A then q j ^ 2
                         else 0) = q j ^ 2 := ite_eq_left ⟨hadj, hjB, hiv, hiA⟩
-                    have hval : (0 - -(q j)) ^ 2 = q j ^ 2 := by ring
-                    rw [hxZ i hiu hiv hiA hiB, hxB j hjB, hval]
-                    linarith
+                    rw [hxZ i hiu hiv hiA hiB, hxB j hjB, zero_sub, neg_neg]
+                    linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn7,
+                      nn8, nn9, nn11, nn12, nn13, nn14, e10]
                   · -- `Z → Z`: zero.
                     rw [hxZ i hiu hiv hiA hiB, hxZ j hju hjv hjA hjB]
                     norm_num
-                    linarith
+                    linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn7,
+                      nn8, nn9, nn10, nn11, nn12, nn13, nn14]
   · rw [ite_eq_right hadj]
-    linarith
+    linarith only [nn1, nn2, nn3, nn4, nn5, nn6, nn7, nn8, nn9, nn10, nn11, nn12, nn13, nn14]
 
 open Classical in
 private theorem algConn_le_two_of_apex_double_star_hC5 : ∀ {V : Type u_1} [Fintype V] (G :
diff --git a/LeanPool/ACMax/Counting/HubCross.lean b/LeanPool/ACMax/Counting/HubCross.lean
index 4012557cf0..ac427680b8 100644
--- a/LeanPool/ACMax/Counting/HubCross.lean
+++ b/LeanPool/ACMax/Counting/HubCross.lean
@@ -5,14 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import LeanPool.ACMax.Counting.Incidence
-public import Mathlib.Tactic.FieldSimp
-public import Mathlib.Tactic.Linarith
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Positivity
-public import Mathlib.Tactic.Ring
-public import LeanPool.ACMax.Counting.FarPair
-public import LeanPool.ACMax.Counting.CompactCell
 public import LeanPool.ACMax.Counting.CompactLedgers
 
 /-!
diff --git a/LeanPool/ACMax/Counting/LargeN.lean b/LeanPool/ACMax/Counting/LargeN.lean
index 5c75c59a9f..86a6a0c4ca 100644
--- a/LeanPool/ACMax/Counting/LargeN.lean
+++ b/LeanPool/ACMax/Counting/LargeN.lean
@@ -5,18 +5,8 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.IntervalCases
-public import Mathlib.Tactic.Linarith
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Push
-public import Mathlib.Tactic.Ring
-public import LeanPool.ACMax.Counting.CompactLedgers
 public import LeanPool.ACMax.Counting.XBoundAssembly
-public import LeanPool.ACMax.Counting.CompactCell
 public import LeanPool.ACMax.Cuts.TwoCut
-public import LeanPool.ACMax.Counting.HubCross
-public import LeanPool.ACMax.Counting.FarPair
-public import LeanPool.ACMax.Reduction.Residual
 
 /-!
 # The large-`n` assembly and the cloud bound
diff --git a/LeanPool/ACMax/Counting/MEdgeSparse.lean b/LeanPool/ACMax/Counting/MEdgeSparse.lean
index 5b2c0afc93..804bff7e2a 100644
--- a/LeanPool/ACMax/Counting/MEdgeSparse.lean
+++ b/LeanPool/ACMax/Counting/MEdgeSparse.lean
@@ -5,7 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.Push
 public import LeanPool.ACMax.Counting.Moats
 public import LeanPool.ACMax.Counting.SparseCore
 
diff --git a/LeanPool/ACMax/Counting/Moats.lean b/LeanPool/ACMax/Counting/Moats.lean
index 5e16f6178e..f5fa5248c0 100644
--- a/LeanPool/ACMax/Counting/Moats.lean
+++ b/LeanPool/ACMax/Counting/Moats.lean
@@ -6,8 +6,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 module
 
 public import LeanPool.ACMax.Counting.Quotient
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Ring
 public import Mathlib.Combinatorics.SimpleGraph.DegreeSum
 
 /-!
diff --git a/LeanPool/ACMax/Counting/PoorCorner.lean b/LeanPool/ACMax/Counting/PoorCorner.lean
index f9475fe31d..2d85c837c0 100644
--- a/LeanPool/ACMax/Counting/PoorCorner.lean
+++ b/LeanPool/ACMax/Counting/PoorCorner.lean
@@ -5,13 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.IntervalCases
-public import Mathlib.Tactic.Linarith
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Push
-public import Mathlib.Tactic.Ring
-public import Mathlib.Tactic.Tauto
-public import LeanPool.ACMax.Reduction.Residual
 public import LeanPool.ACMax.Counting.FarPair
 public import LeanPool.ACMax.Counting.DoubleStar
 
@@ -181,7 +174,8 @@ theorem algConn_le_two_of_far_deg3_pair [Nonempty V]
             exact_mod_cast this
           push_cast at hcast
           linarith
-        nlinarith [h2]
+        norm_num only [show (2 : ℝ) ^ 2 = 4 by norm_num]
+        exact mul_le_mul_of_nonneg_right h2 (by norm_num)
       calc (∑ w ∈ G.neighborFinset t,
             ((G.neighborFinset w \ insert t (G.neighborFinset t')).card : ℝ)
               * (2:ℝ) ^ 2)
@@ -218,7 +212,8 @@ theorem algConn_le_two_of_far_deg3_pair [Nonempty V]
             exact_mod_cast this
           push_cast at hcast
           linarith
-        nlinarith [h2]
+        norm_num only [show (2 : ℝ) ^ 2 = 4 by norm_num]
+        exact mul_le_mul_of_nonneg_right h2 (by norm_num)
       calc (∑ w ∈ G.neighborFinset t',
             ((G.neighborFinset w \ insert t' (G.neighborFinset t)).card : ℝ)
               * (2:ℝ) ^ 2)
diff --git a/LeanPool/ACMax/Counting/Quotient.lean b/LeanPool/ACMax/Counting/Quotient.lean
index 7de5b8a397..96a642ccb8 100644
--- a/LeanPool/ACMax/Counting/Quotient.lean
+++ b/LeanPool/ACMax/Counting/Quotient.lean
@@ -250,7 +250,8 @@ theorem algConn_le_two_of_sparse_cut [Nonempty V]
       Nat.cast_nonneg _
     have hsum0 : (0 : ℝ) ≤ (S.card : ℝ) + (Sᶜ.card : ℝ) := by linarith
     rw [hVn] at hcutR
-    nlinarith [mul_le_mul_of_nonneg_left hcutR hsum0, hcS, hcSc, hEc]
+    convert mul_le_mul_of_nonneg_left hcutR
+      (mul_nonneg (by norm_num : (0 : ℝ) ≤ 2) hsum0) using 1 <;> ring
 
 /-! ## Handshake identities for the quotient data -/
 
diff --git a/LeanPool/ACMax/Counting/ResidualInterface.lean b/LeanPool/ACMax/Counting/ResidualInterface.lean
index 7049a5e448..f39997e099 100644
--- a/LeanPool/ACMax/Counting/ResidualInterface.lean
+++ b/LeanPool/ACMax/Counting/ResidualInterface.lean
@@ -5,14 +5,8 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.Push
-public import LeanPool.ACMax.Reduction.Residual
-public import LeanPool.ACMax.Spectral.AlgConn
-public import LeanPool.ACMax.Spectral.RayleighUpper
-public import LeanPool.ACMax.Spectral.TestVector
 public import Mathlib.Combinatorics.SimpleGraph.Metric
 public import LeanPool.ACMax.Counting.CompactCell
-public import LeanPool.ACMax.Counting.DoubleStar
 
 /-!
 # The residual-core interface lemmas
diff --git a/LeanPool/ACMax/Counting/SigmaCloud.lean b/LeanPool/ACMax/Counting/SigmaCloud.lean
index 7363b42fe5..1cf6e1e33d 100644
--- a/LeanPool/ACMax/Counting/SigmaCloud.lean
+++ b/LeanPool/ACMax/Counting/SigmaCloud.lean
@@ -5,9 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import LeanPool.ACMax.Counting.FarPair
-public import LeanPool.ACMax.Counting.CompactCell
-public import LeanPool.ACMax.Counting.CompactLedgers
 public import LeanPool.ACMax.Counting.HubCross
 public import LeanPool.ACMax.Counting.Quotient
 
@@ -850,6 +847,24 @@ theorem sigma_transfer_sat {d : ℕ} (hd : 16 ≤ d) :
   nlinarith [mul_nonneg (show (0 : ℝ) ≤ (d : ℝ) - 16 by linarith)
     (show (0 : ℝ) ≤ (d : ℝ) - 2 by linarith)]
 
+/-- The usable transfer follows from four nonnegative polynomial terms. -/
+private theorem sigma_usable_transfer_arithmetic (d f j S : ℝ)
+    (hd : 6 ≤ d) (hf : 0 ≤ f) (hfj : 3 ≤ f + j) (hSj : 2 / 3 * j ≤ S) :
+    (d - 3) * (d - f) ≤ (5 / 4 * (d - 4) + S) * (d - 2) := by
+  have hd2 : 0 ≤ d - 2 := by linarith only [hd]
+  have h1 := mul_nonneg (show 0 ≤ d - 4 by linarith only [hd])
+    (show 0 ≤ d - 6 by linarith only [hd])
+  have h2 := mul_nonneg hf (show 0 ≤ d - 5 by linarith only [hd])
+  have h3 := mul_nonneg (sub_nonneg.mpr hfj) hd2
+  have h4 := mul_le_mul_of_nonneg_right hSj hd2
+  nlinarith only [h1, h2, h3, h4]
+/-- The non-usable transfer is its degree certificate plus the positive mass gap. -/
+private theorem sigma_nonusable_transfer_arithmetic (d f S : ℝ)
+    (hd : 0 < d - 2) (hdf : 0 ≤ (d - 4) * (d - 6 + 2 * f))
+    (hS : 2 - 1 / 2 * f < S) :
+    (d - 3) * (d - f) ≤ (5 / 4 * (d - 4) + S) * (d - 2) := by
+  nlinarith only [hdf, mul_pos hd (sub_pos.mpr hS)]
+
 open Classical in
 /-- **The non-usable transfer** (suppressed heavy vertices): if `deg w = d ≥ 5`
 and `sigS w > 2`, then `σ(d)(a₃ + j) ≤ (5/4)(d−4) + S_w`.  The real relaxation
@@ -914,7 +929,7 @@ theorem sigma_transfer_nonusable (G : SimpleGraph (Fin n)) (w : Fin n)
     have hd5R : (5 : ℝ) ≤ (d : ℝ) := by exact_mod_cast hd
     have hpos : (0 : ℝ) < (d : ℝ) - 2 := by linarith
     rw [sigma, div_mul_eq_mul_div, div_le_iff₀ hpos]
-    nlinarith [mul_pos hpos (show (0 : ℝ) < S - (2 - (1 / 2) * (f : ℝ)) by linarith)]
+    exact sigma_nonusable_transfer_arithmetic d f S hpos hdfR hSgt
 
 open Classical in
 /-- **The usable transfer** (uncapped, non-`W₅`): if `deg w = d ≥ 5`,
@@ -974,17 +989,10 @@ theorem sigma_transfer_usable (G : SimpleGraph (Fin n)) (w : Fin n)
   · -- `d ≥ 6`
     have hd6R : (6 : ℝ) ≤ (d : ℝ) := by exact_mod_cast hd6
     have hfR : (0 : ℝ) ≤ (f : ℝ) := by positivity
-    have hjR : (0 : ℝ) ≤ (j : ℝ) := by positivity
     have hfj3R : (3 : ℝ) ≤ (f : ℝ) + (j : ℝ) := by exact_mod_cast hfj3
     have hpos : (0 : ℝ) < (d : ℝ) - 2 := by linarith
     rw [sigma, div_mul_eq_mul_div, div_le_iff₀ hpos]
-    -- goal: (d−3)(d−f) ≤ ((5/4)(d−4) + S)(d−2); use S ≥ (2/3)j, j ≥ 3−f
-    nlinarith [mul_nonneg (show (0 : ℝ) ≤ (d : ℝ) - 4 by linarith)
-        (show (0 : ℝ) ≤ (d : ℝ) - 6 by linarith),
-      mul_nonneg hfR (show (0 : ℝ) ≤ (d : ℝ) - 5 by linarith),
-      mul_nonneg hjR (show (0 : ℝ) ≤ (d : ℝ) - 5 by linarith),
-      mul_pos hpos (show (0 : ℝ) < (d : ℝ) - 2 by linarith),
-      mul_le_mul_of_nonneg_right hSj (le_of_lt hpos)]
+    exact sigma_usable_transfer_arithmetic d f j S hd6R hfR hfj3R hSj
 
 open Classical in
 /-- **The `W₅` transfer with overflow `1/12`**: a usable degree-5 vertex with
@@ -1223,7 +1231,7 @@ theorem capped_overflow_le (n : ℕ) (G : SimpleGraph (Fin n))
       = ∑ w ∈ Q, (sigma (G.degree w) * ((G.degree w : ℝ))
         - (5 / 4) * ((G.degree w : ℝ) - 4)) := by rw [hQ]
   rw [hQC]
-  nlinarith [hMpart, hQpart, hgrid]
+  linarith only [hMpart, hQpart, hgrid]
 
 /-! ## The exchange identity and the summed transfer -/
 
diff --git a/LeanPool/ACMax/Counting/SparseCore.lean b/LeanPool/ACMax/Counting/SparseCore.lean
index ec24cfd175..3bdf5225dc 100644
--- a/LeanPool/ACMax/Counting/SparseCore.lean
+++ b/LeanPool/ACMax/Counting/SparseCore.lean
@@ -5,7 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.Ring
 public import Mathlib.Combinatorics.SimpleGraph.DegreeSum
 public import LeanPool.ACMax.Counting.Quotient
 public import LeanPool.ACMax.Cuts.WeightedCut
diff --git a/LeanPool/ACMax/Counting/SqrtGirth.lean b/LeanPool/ACMax/Counting/SqrtGirth.lean
index bf5bddab3c..55953eae07 100644
--- a/LeanPool/ACMax/Counting/SqrtGirth.lean
+++ b/LeanPool/ACMax/Counting/SqrtGirth.lean
@@ -5,14 +5,7 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Combinatorics.SimpleGraph.Acyclic
 public import Mathlib.Combinatorics.SimpleGraph.Girth
-public import Mathlib.Combinatorics.SimpleGraph.DegreeSum
-public import Mathlib.Combinatorics.SimpleGraph.Maps
-public import Mathlib.Combinatorics.SimpleGraph.Paths
-public import Mathlib.Combinatorics.SimpleGraph.Metric
-public import Mathlib.Combinatorics.SimpleGraph.Finite
-public import Mathlib.Data.ZMod.Basic
 public import Mathlib.Tactic.Ring
 
 /-!
diff --git a/LeanPool/ACMax/Counting/StarMoatSharp.lean b/LeanPool/ACMax/Counting/StarMoatSharp.lean
index e1184bfc8e..74f18e3fd7 100644
--- a/LeanPool/ACMax/Counting/StarMoatSharp.lean
+++ b/LeanPool/ACMax/Counting/StarMoatSharp.lean
@@ -7,10 +7,7 @@ module
 
 public import LeanPool.ACMax.Counting.StarNeighbors
 public import LeanPool.ACMax.Counting.Incidence
-public import Mathlib.Tactic.Linarith
-public import Mathlib.Tactic.Push
 public import LeanPool.ACMax.Counting.Moats
-public import LeanPool.ACMax.Counting.SparseCore
 public import LeanPool.ACMax.Counting.TripleCensus
 public import LeanPool.ACMax.Counting.DecoratedC4
 
@@ -2936,7 +2933,8 @@ theorem z1_star_moat_fires_core {n : ℕ} [Nonempty (Fin n)] (hn : 10 ≤ n)
   by_cases hcheap : ((S₂ ×ˢ F).filter (fun q => G.Adj q.1 q.2)).card ≤ 2 * S₂.card
   · refine algConn_le_two_of_two_clusters G S₁ S₂ hS1ne hS2ne hdisj hnc ?_
     rw [hFeq, hS1card]
-    nlinarith [he1, hcheap, Nat.zero_le S₂.card]
+    nlinarith only [Nat.mul_le_mul_right (S₂.card ^ 2) he1,
+      Nat.mul_le_mul_right 9 hcheap]
   · by_cases hlarge : 2 * ∑ v ∈ S₂, (G.degree v - 3) < internalPairCount G S₂
     · obtain ⟨T, hTsub, hTne, hTslice⟩ :=
         exists_sparse_core_of_twice_excess_lt_pairs G h3 S₂ hlarge
diff --git a/LeanPool/ACMax/Counting/StarvedCensus.lean b/LeanPool/ACMax/Counting/StarvedCensus.lean
index 952e92ea48..761f21ba1c 100644
--- a/LeanPool/ACMax/Counting/StarvedCensus.lean
+++ b/LeanPool/ACMax/Counting/StarvedCensus.lean
@@ -5,14 +5,9 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.FinCases
-public import Mathlib.Tactic.GCongr
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Ring
 public import LeanPool.ACMax.Counting.Moats
 public import LeanPool.ACMax.Counting.ResidualInterface
 public import LeanPool.ACMax.Counting.XBoundAssembly
-public import LeanPool.ACMax.Reduction.Residual
 
 /-!
 # The starved-world census and the owner-choke rows
@@ -869,6 +864,7 @@ theorem owner_sat_independence {n : ℕ} [Nonempty (Fin n)] (hn : 39 ≤ n)
     have e2 : (![o, s, t] : Fin 3 → Fin n) 2 = t := rfl
     refine master_cycle_fires (k := 3) (by norm_num) G hm h3 ![o, s, t] ?_ ?_ ?_ ?_
     · intro i j hij
+      clear * - hij hne_os hne_ot hne_st
       fin_cases i <;> fin_cases j <;> simp_all <;> rfl
     · intro i
       fin_cases i
@@ -1660,6 +1656,7 @@ theorem sat_sat_independence {n : ℕ} [Nonempty (Fin n)] (hn : 48 ≤ n)
     have e3 : (![s₁, t₁, s₂, t₂] : Fin 4 → Fin n) 3 = t₂ := rfl
     refine master_cycle_fires (k := 4) (by norm_num) G hm h3 ![s₁, t₁, s₂, t₂] ?_ ?_ ?_ ?_
     · intro i j hij
+      clear * - hij hne ht12ne hs1t1 hs1t2 hs2t1 hs2t2
       fin_cases i <;> fin_cases j <;> simp_all <;> rfl
     · intro i
       fin_cases i
diff --git a/LeanPool/ACMax/Counting/TripleCensus.lean b/LeanPool/ACMax/Counting/TripleCensus.lean
index 23fcec8cdf..ae04224c48 100644
--- a/LeanPool/ACMax/Counting/TripleCensus.lean
+++ b/LeanPool/ACMax/Counting/TripleCensus.lean
@@ -9,7 +9,6 @@ public import Mathlib.Algebra.BigOperators.Ring.Finset
 public import Mathlib.Algebra.Order.BigOperators.Group.Finset
 public import Mathlib.Algebra.Order.Ring.Nat
 public import Mathlib.Data.Nat.Cast.Order.Basic
-public import Mathlib.Tactic.Push
 
 /-!
 # A six-column three-group census
diff --git a/LeanPool/ACMax/Counting/V9Discharge.lean b/LeanPool/ACMax/Counting/V9Discharge.lean
index 0078fc3cde..e21825a51e 100644
--- a/LeanPool/ACMax/Counting/V9Discharge.lean
+++ b/LeanPool/ACMax/Counting/V9Discharge.lean
@@ -5,14 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.Convert
-public import Mathlib.Tactic.GCongr
-public import Mathlib.Tactic.Lift
-public import Mathlib.Tactic.Linarith
-public import Mathlib.Tactic.Push
-public import Mathlib.Tactic.Ring
-public import LeanPool.ACMax.Counting.CompactCell
-public import LeanPool.ACMax.Counting.DoubleStar
 public import LeanPool.ACMax.Counting.StarvedCensus
 public import LeanPool.ACMax.Counting.SqrtGirth
 
@@ -456,7 +448,7 @@ theorem girth_excess_bound_holds (n : ℕ) (G : SimpleGraph (Fin n)) : GirthExce
       obtain ⟨d, hd⟩ : ∃ d, S.card = NN + d := ⟨S.card - NN, by omega⟩
       have h1 : d * (2 * r + 1) ≤ d * NN := Nat.mul_le_mul_left d h2r1
       rw [hd]
-      nlinarith [h1]
+      linarith [h1, Nat.zero_le (d * NN), Nat.zero_le (d ^ 2)]
     -- (iv) Collide with the side condition.
     omega
   -- Lift the short cycle from the component graph to `G` and convert to `ZMod`.
diff --git a/LeanPool/ACMax/Counting/V9DischargeSharp.lean b/LeanPool/ACMax/Counting/V9DischargeSharp.lean
index 0710d58b13..090e12c2ac 100644
--- a/LeanPool/ACMax/Counting/V9DischargeSharp.lean
+++ b/LeanPool/ACMax/Counting/V9DischargeSharp.lean
@@ -5,6 +5,7 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
+public import LeanPool.ACMax.Counting.Arithmetic
 public import LeanPool.ACMax.Counting.V9Discharge
 public import LeanPool.ACMax.Counting.MoatSharp
 
@@ -47,11 +48,10 @@ open Classical in
 /-- **The sharp strip cubic.**  The single-variable inequality the `n ≥ 123` region arithmetic
 bottoms out at, after `X` is pushed to its master maximum and `H` to the end of its range.
 Substituting `N = 123 + u` makes every coefficient non-negative
-(`1068496017 + 1122649307u + 11552736u² + 20700u³`), which is what `nlinarith` finds. -/
+(`1068496017 + 1122649307u + 11552736u² + 20700u³`), giving an explicit positive certificate. -/
 theorem strip_cubic_sharp {N : ℤ} (hN : 123 ≤ N) :
     779812849 * N + 755972700 < 20700 * N ^ 3 + 3914436 * N ^ 2 := by
-  have hu : (0 : ℤ) ≤ N - 123 := by linarith
-  nlinarith [hu, mul_nonneg hu hu, mul_nonneg (mul_nonneg hu hu) hu]
+  exact Arithmetic.strip_cubic_sharp hN
 
 open Classical in
 /-- **The two-variable core.**  After both `X`-eliminations the target is a cubic in `(N, H)`:
@@ -67,17 +67,7 @@ theorem moore_strip_twovar_sharp {N H : ℤ} (hN : 123 ≤ N) (hH : 0 ≤ H)
     4608000 * (N - H) ^ 2
       < 38400 * ((N - H) * (16 * N + 7 * H - 30))
         + 23 * ((6 * N + 160 - 23 * H) * (16 * N + 7 * H - 150) ^ 2) := by
-  have hd : (0 : ℤ) ≤ (4 * N - 200) - 17 * H := by linarith
-  have hHm : (0 : ℤ) ≤ 17 * H := by linarith
-  have hnc1 : (0 : ℤ) ≤ 104512 * N ^ 2 - 11944120 * N + 18478500 := by nlinarith [hN]
-  have hnc2 : (0 : ℤ) ≤ 111734 * N + 3585580 := by linarith
-  have hsq : (0 : ℤ) ≤ (4 * N - 200) ^ 2 + 17 * H * (4 * N - 200) + (17 * H) ^ 2 := by
-    nlinarith [hHm, hd, sq_nonneg (4 * N - 200), sq_nonneg (17 * H)]
-  have e1 := mul_nonneg hd hnc1
-  have e2 := mul_nonneg (mul_nonneg hd (by linarith : (0 : ℤ) ≤ (4 * N - 200) + 17 * H)) hnc2
-  have e3 := mul_nonneg (mul_nonneg hd hsq) (by norm_num : (0 : ℤ) ≤ 25921)
-  have hcub := strip_cubic_sharp hN
-  linarith [e1, e2, e3, hcub]
+  exact Arithmetic.moore_strip_twovar_sharp hN hH hs
 
 open Classical in
 /-- **The `R`-free core of the sharp strip discharge.**  On the counting region
@@ -93,25 +83,7 @@ theorem moore_strip_core_sharp {N X H : ℤ} (hN : 123 ≤ N) (hH : 0 ≤ H) (hH
     4608 * (N - H) ^ 2
       < 384 * ((N - H) * (2 * N - X - 23))
         + 23 * ((N - 4 - X - 3 * H) * (2 * N - X - 35) ^ 2) := by
-  have h17 : 17 * H ≤ 4 * N - 200 := by linarith
-  have hvpos : (0 : ℤ) ≤ N - H := by linarith
-  have hPpos : (0 : ℤ) ≤ 6 * N + 160 - 23 * H := by linarith
-  have hQpos : (0 : ℤ) ≤ 16 * N + 7 * H - 150 := by linarith
-  have hP : 6 * N + 160 - 23 * H ≤ 10 * (N - 4 - X - 3 * H) := by linarith
-  have hQ : 16 * N + 7 * H - 150 ≤ 10 * (2 * N - X - 35) := by linarith
-  -- the ball factor, pushed to the master maximum
-  have hA : 38400 * ((N - H) * (16 * N + 7 * H - 30))
-      ≤ 1000 * (384 * ((N - H) * (2 * N - X - 23))) := by nlinarith [hvpos, hQ]
-  -- the excess factor, pushed to the master maximum
-  have hQ2 : (16 * N + 7 * H - 150) ^ 2 ≤ (10 * (2 * N - X - 35)) ^ 2 := by
-    nlinarith [hQpos, hQ]
-  have hmul : (6 * N + 160 - 23 * H) * (16 * N + 7 * H - 150) ^ 2
-      ≤ (10 * (N - 4 - X - 3 * H)) * (10 * (2 * N - X - 35)) ^ 2 :=
-    mul_le_mul hP hQ2 (sq_nonneg _) (by linarith)
-  have hB : 23 * ((6 * N + 160 - 23 * H) * (16 * N + 7 * H - 150) ^ 2)
-      ≤ 1000 * (23 * ((N - 4 - X - 3 * H) * (2 * N - X - 35) ^ 2)) := by nlinarith [hmul]
-  have htv := moore_strip_twovar_sharp hN hH h17
-  linarith [hA, hB, htv]
+  exact Arithmetic.moore_strip_core_sharp hN hH hHX hmaster
 
 open Classical in
 /-- **The sharp strip Moore arithmetic.**  On the counting region, `MASTER′` together with
@@ -134,13 +106,19 @@ theorem moore_strip_arith_sharp {N X H R : ℤ} (hN : 123 ≤ N)
   have hcore := moore_strip_core_sharp hN hH hHX hmaster
   -- the ball term: `12(2R + 1) = 24R + 12 ≥ 2N − X − 23`
   have hball : (N - H) * (2 * N - X - 23) ≤ 12 * ((N - H) * (2 * R + 1)) := by
-    nlinarith [hvpos, hR]
+    convert mul_le_mul_of_nonneg_left (add_le_add_right hR 12) hvpos using 1 <;> ring
   -- the excess term
-  have hsq : (2 * N - X - 35) ^ 2 ≤ 576 * R ^ 2 := by nlinarith [hR, hApos]
-  have hRR : 23 * R ^ 2 ≤ 8 * (3 * R ^ 2 - R) := by nlinarith [hR8]
-  have hexc : 23 * (2 * N - X - 35) ^ 2 ≤ 4608 * (3 * R ^ 2 - R) := by nlinarith [hsq, hRR]
+  have hsq : (2 * N - X - 35) ^ 2 ≤ 576 * R ^ 2 := by
+    convert pow_le_pow_left₀ hApos hR 2 using 1; ring
+  have hRR : 23 * R ^ 2 ≤ 8 * (3 * R ^ 2 - R) := by
+    nlinarith only [mul_nonneg (show 0 ≤ R by omega) (sub_nonneg.mpr hR8)]
+  have hexc : 23 * (2 * N - X - 35) ^ 2 ≤ 4608 * (3 * R ^ 2 - R) := by
+    have hleft := mul_le_mul_of_nonneg_left hsq (by norm_num : (0 : ℤ) ≤ 23)
+    have hright := mul_le_mul_of_nonneg_left hRR (by norm_num : (0 : ℤ) ≤ 576)
+    nlinarith only [hleft, hright]
   have hB : 23 * ((N - 4 - X - 3 * H) * (2 * N - X - 35) ^ 2)
-      ≤ 4608 * ((N - 4 - X - 3 * H) * (3 * R ^ 2 - R)) := by nlinarith [hq, hexc]
+      ≤ 4608 * ((N - 4 - X - 3 * H) * (3 * R ^ 2 - R)) := by
+    convert mul_le_mul_of_nonneg_left hexc hq using 1 <;> ring
   linarith [hcore, hball, hB]
 
 /-! ## The graph-level dispatch -/
diff --git a/LeanPool/ACMax/Counting/Windows.lean b/LeanPool/ACMax/Counting/Windows.lean
index 1bf38b134c..91d836aec5 100644
--- a/LeanPool/ACMax/Counting/Windows.lean
+++ b/LeanPool/ACMax/Counting/Windows.lean
@@ -6,9 +6,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 module
 
 public import LeanPool.ACMax.Spectral.AlgConnK2
-public import LeanPool.ACMax.Cuts.LowDegreeVertex
-public import LeanPool.ACMax.Counting.ResidualInterface
-public import LeanPool.ACMax.Counting.XBoundAssembly
 public import LeanPool.ACMax.Counting.StarvedCensus
 public import LeanPool.ACMax.Counting.MEdgeSparse
 public import LeanPool.ACMax.Counting.SmallDegreeThreeCore
diff --git a/LeanPool/ACMax/Counting/XBoundAssembly.lean b/LeanPool/ACMax/Counting/XBoundAssembly.lean
index e7f2d48caa..d35b1cb490 100644
--- a/LeanPool/ACMax/Counting/XBoundAssembly.lean
+++ b/LeanPool/ACMax/Counting/XBoundAssembly.lean
@@ -5,10 +5,7 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import LeanPool.ACMax.Counting.CompactLedgers
 public import LeanPool.ACMax.Counting.SigmaCloud
-public import LeanPool.ACMax.Counting.CompactCell
-public import LeanPool.ACMax.Counting.DoubleStar
 
 /-!
 # The master X-bound assembly
diff --git a/LeanPool/ACMax/Cuts/Disconnected.lean b/LeanPool/ACMax/Cuts/Disconnected.lean
index 4ed5dbcbe9..ea6fe5985a 100644
--- a/LeanPool/ACMax/Cuts/Disconnected.lean
+++ b/LeanPool/ACMax/Cuts/Disconnected.lean
@@ -5,7 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import LeanPool.ACMax.Spectral.AlgConn
 public import LeanPool.ACMax.Cuts.WeightedCut
 
 /-!
diff --git a/LeanPool/ACMax/Cuts/GoodC4.lean b/LeanPool/ACMax/Cuts/GoodC4.lean
index 8adb1064ff..1de4f8627d 100644
--- a/LeanPool/ACMax/Cuts/GoodC4.lean
+++ b/LeanPool/ACMax/Cuts/GoodC4.lean
@@ -5,8 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.Ring
-public import LeanPool.ACMax.Spectral.AlgConn
 public import LeanPool.ACMax.Cuts.WeightedCut
 
 /-!
diff --git a/LeanPool/ACMax/Cuts/GoodK23.lean b/LeanPool/ACMax/Cuts/GoodK23.lean
index 287c22124f..0d7f37f005 100644
--- a/LeanPool/ACMax/Cuts/GoodK23.lean
+++ b/LeanPool/ACMax/Cuts/GoodK23.lean
@@ -5,8 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.Ring
-public import LeanPool.ACMax.Spectral.AlgConn
 public import LeanPool.ACMax.Cuts.WeightedCut
 
 /-!
diff --git a/LeanPool/ACMax/Cuts/Ind2K2.lean b/LeanPool/ACMax/Cuts/Ind2K2.lean
index 6c7641025c..480e0f38b1 100644
--- a/LeanPool/ACMax/Cuts/Ind2K2.lean
+++ b/LeanPool/ACMax/Cuts/Ind2K2.lean
@@ -5,10 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.GCongr
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Tauto
-public import LeanPool.ACMax.Spectral.AlgConn
 public import LeanPool.ACMax.Cuts.SignedCut
 
 /-!
diff --git a/LeanPool/ACMax/Cuts/LowDegreeVertex.lean b/LeanPool/ACMax/Cuts/LowDegreeVertex.lean
index 7ff5cfd29e..d17aaa6d9d 100644
--- a/LeanPool/ACMax/Cuts/LowDegreeVertex.lean
+++ b/LeanPool/ACMax/Cuts/LowDegreeVertex.lean
@@ -5,11 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.Linarith
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Ring
-public import LeanPool.ACMax.Spectral.AlgConn
-public import LeanPool.ACMax.Spectral.RayleighUpper
 public import LeanPool.ACMax.Spectral.TestVector
 
 /-!
diff --git a/LeanPool/ACMax/Cuts/SignedCut.lean b/LeanPool/ACMax/Cuts/SignedCut.lean
index 13e1e873dc..530e37214c 100644
--- a/LeanPool/ACMax/Cuts/SignedCut.lean
+++ b/LeanPool/ACMax/Cuts/SignedCut.lean
@@ -5,12 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.Linarith
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Ring
-public import Mathlib.Tactic.Tauto
-public import LeanPool.ACMax.Spectral.AlgConn
-public import LeanPool.ACMax.Spectral.RayleighUpper
 public import LeanPool.ACMax.Spectral.TestVector
 
 /-!
diff --git a/LeanPool/ACMax/Cuts/TriangleFree2K2.lean b/LeanPool/ACMax/Cuts/TriangleFree2K2.lean
index d9b99922b6..13c7a734b2 100644
--- a/LeanPool/ACMax/Cuts/TriangleFree2K2.lean
+++ b/LeanPool/ACMax/Cuts/TriangleFree2K2.lean
@@ -5,11 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Algebra.Order.BigOperators.Group.Finset
-public import Mathlib.Combinatorics.SimpleGraph.Finite
-public import Mathlib.Tactic.Push
-public import Mathlib.Tactic.Ring
-public import Mathlib.Tactic.Ring.Basic
 public import LeanPool.ACMax.Spectral.AlgConn
 
 /-!
diff --git a/LeanPool/ACMax/Cuts/TwoCut.lean b/LeanPool/ACMax/Cuts/TwoCut.lean
index 541bf6e3bc..b55ce48f3c 100644
--- a/LeanPool/ACMax/Cuts/TwoCut.lean
+++ b/LeanPool/ACMax/Cuts/TwoCut.lean
@@ -5,11 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.Linarith
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Ring
-public import LeanPool.ACMax.Spectral.AlgConn
-public import LeanPool.ACMax.Spectral.RayleighUpper
 public import LeanPool.ACMax.Spectral.TestVector
 
 /-!
diff --git a/LeanPool/ACMax/Cuts/WeightedCut.lean b/LeanPool/ACMax/Cuts/WeightedCut.lean
index a62cba42b7..f03e841baf 100644
--- a/LeanPool/ACMax/Cuts/WeightedCut.lean
+++ b/LeanPool/ACMax/Cuts/WeightedCut.lean
@@ -5,12 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.Linarith
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Ring
-public import Mathlib.Tactic.Tauto
-public import LeanPool.ACMax.Spectral.AlgConn
-public import LeanPool.ACMax.Spectral.RayleighUpper
 public import LeanPool.ACMax.Spectral.TestVector
 
 /-!
diff --git a/LeanPool/ACMax/Imports.lean b/LeanPool/ACMax/Imports.lean
index 3f6b9dc700..12045e3d96 100644
--- a/LeanPool/ACMax/Imports.lean
+++ b/LeanPool/ACMax/Imports.lean
@@ -21,6 +21,7 @@ public import LeanPool.ACMax.Band.KillSharp
 public import LeanPool.ACMax.Band.Rows
 public import LeanPool.ACMax.Band.Subset
 public import LeanPool.ACMax.Band.Sum
+public import LeanPool.ACMax.Counting.Arithmetic
 public import LeanPool.ACMax.Counting.Cherry
 public import LeanPool.ACMax.Counting.CherryMShape
 public import LeanPool.ACMax.Counting.CompactCell
diff --git a/LeanPool/ACMax/Reduction/GapReduction.lean b/LeanPool/ACMax/Reduction/GapReduction.lean
index 475113cb87..9c44fa55e9 100644
--- a/LeanPool/ACMax/Reduction/GapReduction.lean
+++ b/LeanPool/ACMax/Reduction/GapReduction.lean
@@ -5,7 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.NormNum
 public import LeanPool.ACMax.Counting.LargeN
 public import LeanPool.ACMax.Spectral.AlgConnK2
 
diff --git a/LeanPool/ACMax/Reduction/Reduction.lean b/LeanPool/ACMax/Reduction/Reduction.lean
index f999a85a33..871ab53b8b 100644
--- a/LeanPool/ACMax/Reduction/Reduction.lean
+++ b/LeanPool/ACMax/Reduction/Reduction.lean
@@ -5,12 +5,8 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.Convert
-public import Mathlib.Tactic.Ring
 public import Mathlib.Combinatorics.SimpleGraph.DegreeSum
-public import LeanPool.ACMax.Spectral.AlgConn
 public import LeanPool.ACMax.Cuts.LowDegreeVertex
-public import LeanPool.ACMax.Cuts.WeightedCut
 public import LeanPool.ACMax.Cuts.Ind2K2
 public import LeanPool.ACMax.Cuts.TriangleFree2K2
 public import LeanPool.ACMax.Cuts.Disconnected
diff --git a/LeanPool/ACMax/Reduction/Residual.lean b/LeanPool/ACMax/Reduction/Residual.lean
index 1cde1dde0b..ca460f25d5 100644
--- a/LeanPool/ACMax/Reduction/Residual.lean
+++ b/LeanPool/ACMax/Reduction/Residual.lean
@@ -6,9 +6,7 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 module
 
 public import LeanPool.ACMax.Counting.Incidence
-public import Mathlib.Tactic.Ring
 public import LeanPool.ACMax.Reduction.Reduction
-public import LeanPool.ACMax.Cuts.SignedCut
 
 /-!
 # Uniformly-provable foundation layers for the general ACMAX residual program
diff --git a/LeanPool/ACMax/Spectral/AlgConn.lean b/LeanPool/ACMax/Spectral/AlgConn.lean
index ab42ce2b20..30eeebbf21 100644
--- a/LeanPool/ACMax/Spectral/AlgConn.lean
+++ b/LeanPool/ACMax/Spectral/AlgConn.lean
@@ -7,7 +7,6 @@ module
 
 public import Mathlib.Analysis.Matrix.Spectrum
 public import Mathlib.Combinatorics.SimpleGraph.LapMatrix
-public import Mathlib.Tactic.NormNum
 
 /-!
 # Algebraic connectivity of a finite simple graph
diff --git a/LeanPool/ACMax/Spectral/AlgConnK2.lean b/LeanPool/ACMax/Spectral/AlgConnK2.lean
index 0805a90c4c..4bc598a7e4 100644
--- a/LeanPool/ACMax/Spectral/AlgConnK2.lean
+++ b/LeanPool/ACMax/Spectral/AlgConnK2.lean
@@ -5,10 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.Linarith
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Ring
-public import LeanPool.ACMax.Spectral.AlgConn
 public import LeanPool.ACMax.Spectral.RayleighUpper
 public import LeanPool.ACMax.Spectral.RayleighLower
 
diff --git a/LeanPool/ACMax/Spectral/RayleighLower.lean b/LeanPool/ACMax/Spectral/RayleighLower.lean
index 34de383fe9..e5e98be4de 100644
--- a/LeanPool/ACMax/Spectral/RayleighLower.lean
+++ b/LeanPool/ACMax/Spectral/RayleighLower.lean
@@ -5,9 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.Linarith
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Ring
 public import LeanPool.ACMax.Spectral.AlgConn
 
 /-!
@@ -138,12 +135,15 @@ theorem le_algConn_of_forall {V : Type*} [Fintype V] [Nonempty V] [Nontrivial V]
     rw [hsqw, hnormw, hquadw] at hbnd
     have hpos : 0 < (∑ k, v0 k) ^ 2 + (∑ k, v1 k) ^ 2 := by
       have h2 : 0 < (∑ k, v0 k) ^ 2 := by rw [pow_two]; exact mul_self_pos.mpr hS0
-      nlinarith [sq_nonneg (∑ k, v1 k)]
+      exact add_pos_of_pos_of_nonneg h2 (sq_nonneg _)
     have hub : (∑ k, v1 k) ^ 2 * lam j0 + (∑ k, v0 k) ^ 2 * lam j1
         ≤ algConn G * ((∑ k, v0 k) ^ 2 + (∑ k, v1 k) ^ 2) := by
       rw [hlamj0]
-      nlinarith [mul_le_mul_of_nonneg_left hlamj1 (sq_nonneg (∑ k, v0 k)),
-        sq_nonneg (∑ k, v1 k), sq_nonneg (∑ k, v0 k)]
+      calc
+        _ ≤ (∑ k, v1 k) ^ 2 * algConn G + (∑ k, v0 k) ^ 2 * algConn G :=
+          add_le_add le_rfl
+            (mul_le_mul_of_nonneg_left hlamj1 (sq_nonneg (∑ k, v0 k)))
+        _ = _ := by ring
     have hfin : c * ((∑ k, v0 k) ^ 2 + (∑ k, v1 k) ^ 2)
         ≤ algConn G * ((∑ k, v0 k) ^ 2 + (∑ k, v1 k) ^ 2) := le_trans hbnd hub
     exact le_of_mul_le_mul_right hfin hpos
diff --git a/LeanPool/ACMax/Spectral/RayleighUpper.lean b/LeanPool/ACMax/Spectral/RayleighUpper.lean
index c4e8f35728..20a259e460 100644
--- a/LeanPool/ACMax/Spectral/RayleighUpper.lean
+++ b/LeanPool/ACMax/Spectral/RayleighUpper.lean
@@ -6,10 +6,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 module
 
 public import Mathlib.Analysis.Matrix.PosDef
-public import Mathlib.Tactic.Linarith
-public import Mathlib.Tactic.NormNum
-public import Mathlib.Tactic.Positivity
-public import Mathlib.Tactic.Ring
 public import LeanPool.ACMax.Spectral.AlgConn
 
 /-!
diff --git a/LeanPool/ACMax/Spectral/TestVector.lean b/LeanPool/ACMax/Spectral/TestVector.lean
index 601dd3159f..eaba8ba03d 100644
--- a/LeanPool/ACMax/Spectral/TestVector.lean
+++ b/LeanPool/ACMax/Spectral/TestVector.lean
@@ -5,8 +5,6 @@ Authors: Zeru Zhu, Jinzheng Li, Yuanjie Ren
 -/
 module
 
-public import Mathlib.Tactic.Positivity
-public import LeanPool.ACMax.Spectral.AlgConn
 public import LeanPool.ACMax.Spectral.RayleighUpper
 
 /-!