perf(ACMax): simplify arithmetic certificates and reduce compile time

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
 
 /-!

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

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
 

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
 
 /-!

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
 
 /-!

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

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,14 +213,17 @@ 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)
   have hQ : 0 ≤ Q := by
     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 <

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

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
 
 /-!

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

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

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

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
 
 /-!

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