From f84ae1775cc62b8a491e0fef5fb1e2077e9ab0f0 Mon Sep 17 00:00:00 2001
From: Vasily Ilin <vasilin97@gmail.com>
Date: Sun, 18 Oct 2026 17:13:32 +0000
Subject: [PATCH 1/2] Narrow NonSoficGroup imports and arithmetic fact sets

---
 LeanPool/NonSoficGroup/Compression.lean |  56 +++++----
 LeanPool/NonSoficGroup/Foundations.lean |  99 +++++++---------
 LeanPool/NonSoficGroup/Spectral.lean    | 148 +++++++++---------------
 3 files changed, 120 insertions(+), 183 deletions(-)

diff --git a/LeanPool/NonSoficGroup/Compression.lean b/LeanPool/NonSoficGroup/Compression.lean
index 0a87203d8e..cabf390e2e 100644
--- a/LeanPool/NonSoficGroup/Compression.lean
+++ b/LeanPool/NonSoficGroup/Compression.lean
@@ -507,7 +507,7 @@ private theorem card_symmDiff_upperLevel_le_nine_sq_error {V : Type*}
         exact hxlevel
           (Finset.mem_filter.mpr ⟨Finset.mem_univ x, h⟩)
       simp only [ite_eq_left hxT]
-      nlinarith [sq_nonneg (3 * f x - 2)]
+      nlinarith only [hhigh, hfx, sq_nonneg (3 * f x - 2)]
   have hcard :
       (D.card : ℝ) = ∑ x : V, if x ∈ D then (1 : ℝ) else 0 := by
     simp only [Finset.sum_ite_mem, Finset.univ_inter, Finset.sum_const, nsmul_eq_mul, mul_one]
@@ -664,8 +664,7 @@ private theorem sum_sq_le_card_of_unit_interval_mass
     (∑ x : V, f x ^ 2) ≤ ∑ x : V, f x := by
       apply Finset.sum_le_sum
       intro x _
-      nlinarith [mul_nonneg (hfzero x)
-        (sub_nonneg.mpr (hfone x))]
+      nlinarith only [mul_nonneg (hfzero x) (sub_nonneg.mpr (hfone x))]
     _ = (T.card : ℝ) := hmass
 
 private theorem realMarkov_residual_pairing_le_sqrt_card_mul_residual
@@ -713,8 +712,7 @@ private theorem sum_sum_sq_displacement_le_twice_card_mul_sqrt_card_mul_residual
   have hpair := realMarkov_residual_pairing_le_sqrt_card_mul_residual
     σ T f hfzero hfone hmass
   have hfactor : 0 ≤ 2 * (Fintype.card ι : ℝ) := by positivity
-  nlinarith [mul_nonneg hfactor
-    (sub_nonneg.mpr hpair)]
+  nlinarith only [hpair, hfactor, mul_nonneg hfactor (sub_nonneg.mpr hpair)]
 
 private theorem card_highSupport_le_three_card
     {V : Type*} [Fintype V]
@@ -1160,7 +1158,7 @@ private theorem lt_exp_mul_of_equal_log_floor
     rw [add_mul, div_mul_cancel₀ _ hH.ne', one_mul]
   have hlog : Real.log y < Real.log x + H := by
     rw [div_mul_cancel₀ _ hH.ne', hcancel] at hscaled
-    linarith
+    linarith only [hscaled]
   have hexp := (Real.exp_lt_exp).2 hlog
   rw [Real.exp_log hy, Real.exp_add, Real.exp_log hx] at hexp
   simpa only [mul_comm, gt_iff_lt] using hexp
@@ -1301,7 +1299,7 @@ theorem symmDiff_density_tendsto_zero_of_log_rank_bounds
   have hexp : 1 ≤ Real.exp (H n) := by
     simpa only [Real.one_le_exp_iff, Real.exp_zero] using (Real.exp_le_exp.mpr (hH n))
   have hnonneg : 0 ≤ Real.exp (H n) - 1 + 2 * eta n := by
-    nlinarith [heta n]
+    nlinarith only [hexp, heta n]
   have hmassnat :
       (∑ C ∈ R n, C.card) ≤ (U n).card := by
     calc
@@ -1706,7 +1704,7 @@ private theorem matchedRetained_boundary_density_tendsto_zero
       ((U n).card : ℝ) ≤
         2 * (matchedRetainedSupport (R n)).card := by
     have h := (le_div_iff₀ hucard).1 hn
-    linarith
+    linarith only [h]
   have hsum :
       (∑ C ∈ R n, (boundary (σ n) C : ℝ)) ≤
         ∑ C ∈ (P n).parts, (boundary (σ n) C : ℝ) := by
@@ -2266,7 +2264,7 @@ private theorem reference_difference_le_of_good_root_threshold
             (permutationCommutationDefect σ p : ℝ) +
               2 * (Fintype.card ι : ℝ) * (B.card : ℝ) := by
       exact_mod_cast hboundary
-    linarith
+    linarith only [hbad, hdefect_real, hbound]
   have hmissing_real :
       ((permutationGraph p \ T).card : ℝ) ≤
         (t : ℝ) / (Fintype.card ι : ℝ) := by
@@ -2275,7 +2273,7 @@ private theorem reference_difference_le_of_good_root_threshold
           2 * (B.card : ℝ) := by
       exact_mod_cast hmissing
     apply (le_div_iff₀ hd).2
-    nlinarith
+    nlinarith only [hbad, hm]
   have htransfer :
       (((U \ permutationGraph p).card +
         (permutationGraph p \ U).card : ℕ) : ℝ) ≤
@@ -2312,7 +2310,7 @@ private theorem rooted_reference_cut_bounds_of_slow_tolerance
     2 * Δ ≤ N ∧
       (h + 8 * d) * e ≤ h * t ∧
       5 * (4 * e + h * Δ) ≤ h * N := by
-  have hden : 0 < h + 8 * d := by linarith
+  have hden : 0 < h + 8 * d := by linarith only [hh, hd]
   have hCt : 5 * (C * t) ≤ N := by
     have hscaled : h * (5 * (C * t)) ≤ h * N := by
       linarith only [hslow, ht]
@@ -2741,7 +2739,7 @@ private theorem exists_rooted_word_radius_sparse_cut_of_boundary
       _ ≤ η * b := by
         apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)
         dsimp [ε]
-        linarith
+        linarith only [hk]
   have hfzero : ∀ x : X.carrier, 0 ≤ f x := by
     intro x
     exact
@@ -2760,7 +2758,7 @@ private theorem exists_rooted_word_radius_sparse_cut_of_boundary
         2 * (boundary X.generator T : ℝ) /
           (S.card : ℝ) := by
     simpa only [Fintype.card_coe] using rooted_indicator_defect_sq_le_boundary X.generator T
-  have hgaple : 1 - q ≤ 1 := by linarith
+  have hgaple : 1 - q ≤ 1 := by linarith only [hqzero]
   have hgapzero : 0 ≤ 1 - q := hgap.le
   have hgap_sq_le_one : (1 - q) ^ 2 ≤ 1 :=
     pow_le_one₀ hgapzero hgaple
@@ -2964,7 +2962,7 @@ private theorem witnessless_component_card_le_twice_rankChanging
       (C.card : ℝ) ≤
         2 * ((C ∩ RankArcCharging.rankChangingArc
           (Finset.univ : Finset V) b T.symm).card : ℝ) := by
-    linarith
+    linarith only [hoverlap, hcard, hhalf]
   exact_mod_cast hreal
 
 private theorem witnesslessComponents_mass_le_twice_rankChanging
@@ -3522,7 +3520,7 @@ private theorem rooted_graph_boundary_lt_of_slow_tolerance
     apply (le_div_iff₀ hd).2
     linarith only [hbad]
   have hgraph : N - t / d ≤ c := by
-    linarith
+    linarith only [hmissing, hb]
   have hgraphscaled : γ * (N - t / d) ≤ γ * c :=
     mul_le_mul_of_nonneg_left hgraph hγ.le
   have hNscaled : γ * (5 * C * t) ≤ γ * N :=
@@ -4535,7 +4533,7 @@ theorem exists_uniform_radius_hasAlmostCentralizerImprovement
         (permutationCommutationDefect σ p : ℝ) ≤
           2 * (tolerance : ℝ) := by
       exact_mod_cast hp
-    linarith
+    linarith only [hbad, hbound_real, hp_real]
   have hsparse :
       (boundary
         (fun i : ↥S => (σ i).prodCongr (σ i)) T : ℝ) <
@@ -5308,7 +5306,7 @@ private theorem exists_source_full_finpartition_sequence_of_kazhdan
     have hgap : 0 < (S.card : ℝ) * (1 - q) ^ 2 := by
       positivity
     dsimp [γ, q]
-    nlinarith
+    nlinarith only [hgap]
   let α : ℕ → ℝ := fun j => 1 / ((j : ℝ) + 1)
   have hα (j : ℕ) : 0 < α j := by
     dsimp [α]
@@ -6156,7 +6154,7 @@ private theorem comparisonBad_subset_partitionWordCrossing
   have hnonneg : (0 : ℝ) ≤
       (partitionComponentSize Q x : ℝ) := by
     positivity
-  nlinarith
+  nlinarith only [heta]
 
 private noncomputable def overlapRetainedComponents
     {V : Type*} [Fintype V] [DecidableEq V]
@@ -6314,7 +6312,7 @@ private theorem cast_card_sdiff_eq_sub_card_inter
   have hreal : ((C \ D).card : ℝ) +
       ((C ∩ D).card : ℝ) = (C.card : ℝ) := by
     exact_mod_cast hnat
-  linarith
+  linarith only [hreal]
 
 private theorem subgroup_comparisonBad_density_tendsto_zero
     (V : ℕ → Type*) [∀ n, Fintype (V n)]
@@ -7348,9 +7346,9 @@ private theorem additive_permutation_small_support_coarea
         intro x
         by_cases hx : x ∈ A
         · simp only [g, ite_eq_left hx]
-          linarith [hfM x]
+          linarith only [hfM x]
         · simp only [g, ite_eq_right hx]
-          linarith
+          linarith only [hmM]
       have hgsub :
           CheegerPoincare.positiveSupport g ⊆ A := by
         intro x hx
@@ -7390,7 +7388,7 @@ private theorem additive_permutation_small_support_coarea
         exact_mod_cast hhalf
       have hmin :
           (A.card : ℝ) ≤ (Fintype.card V : ℝ) - A.card := by
-        linarith
+        linarith only [hhalfre]
       have hcut :
           γ * (A.card : ℝ) ≤
             (boundary σ A : ℝ) + ε := by
@@ -7559,12 +7557,12 @@ private theorem additive_permutation_median_absolute_deviation
   have hp_one : ∀ x, p x ≤ 1 := by
     intro x
     apply max_le
-    · linarith [hf_one x]
+    · linarith only [hm_nonnegative, hf_one x]
     · norm_num
   have hq_one : ∀ x, q x ≤ 1 := by
     intro x
     apply max_le
-    · linarith [hf x]
+    · linarith only [hm_one, hf x]
     · norm_num
   have hp_half :
       2 * (CheegerPoincare.positiveSupport p).card ≤
@@ -7607,7 +7605,7 @@ private theorem additive_permutation_median_absolute_deviation
     exact hpoint x
   refine ⟨m, hm_nonnegative, hm_one, ?_⟩
   rw [← hmass, ← hvariation]
-  nlinarith [hp_coarea, hq_coarea]
+  nlinarith only [hp_coarea, hq_coarea]
 
 private theorem additive_permutation_median_variance
     {V ι : Type*} [Fintype V] [Nonempty V]
@@ -7636,9 +7634,9 @@ private theorem additive_permutation_median_variance
       linarith [hf_one x]
     rcases le_total 0 (f x - m) with hx | hx
     · rw [abs_of_nonneg hx]
-      nlinarith
+      nlinarith only [hupper, hx]
     · rw [abs_of_nonpos hx]
-      nlinarith
+      nlinarith only [hlower, hx]
   have hsq :
       (∑ x : V, (f x - m) ^ 2) ≤
         ∑ x : V, |f x - m| := by
@@ -7676,7 +7674,7 @@ private theorem additive_permutation_finiteVariance
     σ γ ε hγ hε hexp f hf hf_one
   rw [← CheegerPoincare.card_mul_finiteVariance f]
     at hvariance
-  nlinarith
+  nlinarith only [hvariance]
 
 end KunAdditiveMedianPoincare
 
@@ -8935,7 +8933,7 @@ private theorem eventually_five_mul_sourceCompletionBad_le_of_density
     exact_mod_cast (show
       (5 : ℝ) * (sourceCompletionBad
         (σ n) (p n) F (Z n)).card < (Z n).card by
-          linarith)
+          linarith only [hreal])
   exact hstrict.le
 
 public
diff --git a/LeanPool/NonSoficGroup/Foundations.lean b/LeanPool/NonSoficGroup/Foundations.lean
index 9d80fbba0e..09fe04ace8 100644
--- a/LeanPool/NonSoficGroup/Foundations.lean
+++ b/LeanPool/NonSoficGroup/Foundations.lean
@@ -16,40 +16,19 @@ public import Mathlib.InformationTheory.Hamming
 public import Mathlib.LinearAlgebra.Matrix.Reindex
 public import Mathlib.Order.Partition.Finpartition
 public import Mathlib.RingTheory.FiniteType
+import Mathlib.Algebra.BigOperators.Field
 import Mathlib.Algebra.Group.MinimalAxioms
-import Mathlib.Algebra.Order.Floor.Extended
-import Mathlib.Algebra.Order.Interval.Basic
-import Mathlib.Algebra.Order.Ring.Star
-import Mathlib.Algebra.Order.Star.Real
 import Mathlib.Data.Finsupp.Encodable
-import Mathlib.Data.NNRat.Floor
-import Mathlib.Data.Nat.Choose.Multinomial
 import Mathlib.Data.Set.FiniteExhaustion
 import Mathlib.LinearAlgebra.Matrix.Unique
-import Mathlib.NumberTheory.Chebyshev
+import Mathlib.MeasureTheory.Function.Floor
+import Mathlib.MeasureTheory.Integral.Average
+import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
 import Mathlib.Order.CompletePartialOrder
-import Mathlib.RingTheory.PiTensorProduct
-import Mathlib.RingTheory.Radical.NatInt
 import Mathlib.RingTheory.TotallySplit
 import Mathlib.SetTheory.Cardinal.Free
-import Mathlib.Tactic.ENatToNat
-import Mathlib.Tactic.NormNum.Irrational
-import Mathlib.Tactic.NormNum.IsCoprime
-import Mathlib.Tactic.NormNum.IsSquare
-import Mathlib.Tactic.NormNum.LegendreSymbol
-import Mathlib.Tactic.NormNum.ModEq
-import Mathlib.Tactic.NormNum.NatFib
-import Mathlib.Tactic.NormNum.NatLog
-import Mathlib.Tactic.NormNum.NatSqrt
-import Mathlib.Tactic.NormNum.Ordinal
-import Mathlib.Tactic.NormNum.Parity
-import Mathlib.Tactic.NormNum.Prime
-import Mathlib.Tactic.NormNum.RealSqrt
-import Mathlib.Tactic.Polynomial.Basic
-import Mathlib.Tactic.ReduceModChar
-import Mathlib.Topology.Separation.CompletelyRegular
-import Mathlib.Topology.Sheaves.Init
-import Std.Tactic.BVDecide.Normalize.Prop
+-- Retain the finite-field and scalar tower instances used by the representation definitions.
+import Mathlib.Tactic.NormNum.LegendreSymbol -- shake: keep
 
 /-!
 # Foundations for the non-sofic group construction
@@ -911,14 +890,14 @@ private theorem hamming_dichotomy_of_expansion {V ι : Type*}
         (Fintype.card V : ℝ) -
           hammingDist (fun x => c x) (fun x => c' x) =
             (agreementSet c c').card := by
-      linarith [hcard']
+      linarith only [hcard']
     simpa only [hident, Nat.cast_add, ge_iff_le] using hcut
   · left
     rw [min_eq_right (le_of_not_ge hhalf)] at hcut
     have hident :
         (Fintype.card V : ℝ) - (agreementSet c c').card =
           hammingDist (fun x => c x) (fun x => c' x) := by
-      linarith [hcard']
+      linarith only [hcard']
     simpa only [Nat.cast_add, ge_iff_le, hident] using hcut
 
 /-- Internal interface connecting the split non-sofic proof modules. -/
@@ -997,7 +976,7 @@ private theorem maximal_bad_cut_induced_lower {V ι : Type*}
     exact_mod_cast Finset.card_union_of_disjoint hdisj
   have hbad : (boundary σ (B ∪ E) : ℝ) < ell * ((B ∪ E).card : ℝ) := by
     rw [hcard]
-    nlinarith
+    nlinarith only [hB, h, hcut]
   have hsize := hmax (B ∪ E) hhalf hbad
   have hepos : 0 < E.card := Finset.card_pos.mpr hne
   have hnat := Finset.card_union_of_disjoint hdisj
@@ -1019,11 +998,11 @@ private theorem large_cut_lower {γ ell a d N b e q : ℝ}
     (hcut : γ * e - a * N - d * b ≤ q) :
     ell * e ≤ q := by
   have hδ : 0 < γ - ell := sub_pos.mpr hgap
-  have hδd : 0 ≤ (γ - ell) + d := by linarith
+  have hδd : 0 ≤ (γ - ell) + d := by linarith only [hgap, hd]
   have hscaledDeleted := mul_le_mul_of_nonneg_left hdeleted hδd
   have hscaledSmall := mul_le_mul_of_nonneg_right hsmall hN
   have hscaledLarge := mul_lt_mul_of_pos_left hlarge hδ
-  nlinarith
+  nlinarith only [hgap, hcut, hscaledDeleted, hscaledSmall, hscaledLarge]
 
 private theorem prune_permutation_multigraph {V ι : Type*}
     [Fintype V] [Fintype ι] [DecidableEq V]
@@ -1053,19 +1032,19 @@ private theorem prune_permutation_multigraph {V ι : Type*}
       (B.card : ℝ) ≤ (Fintype.card V : ℝ) - (B.card : ℝ) := by
     have hcast : 2 * (B.card : ℝ) ≤ (Fintype.card V : ℝ) := by
       exact_mod_cast hBhalf
-    linarith
+    linarith only [hcast]
   have haddB := hadd B
   rw [min_eq_left hBhalfReal] at haddB
   have hdeleted :
       (γ - ell) * (B.card : ℝ) ≤ a * (Fintype.card V : ℝ) := by
-    linarith
+    linarith only [hB, haddB]
   have hEhalfNat : 2 * E.card ≤ Fintype.card V :=
     hEhalf.trans (Nat.sub_le _ _)
   have hEhalfReal :
       (E.card : ℝ) ≤ (Fintype.card V : ℝ) - (E.card : ℝ) := by
     have hcast : 2 * (E.card : ℝ) ≤ (Fintype.card V : ℝ) := by
       exact_mod_cast hEhalfNat
-    linarith
+    linarith only [hcast]
   have haddE := hadd E
   rw [min_eq_left hEhalfReal] at haddE
   have hremoval :
@@ -1076,7 +1055,7 @@ private theorem prune_permutation_multigraph {V ι : Type*}
       γ * (E.card : ℝ) - a * (Fintype.card V : ℝ) -
         (Fintype.card ι : ℝ) * (B.card : ℝ) ≤
         (inducedBoundary σ B E : ℝ) := by
-    linarith
+    linarith only [haddE, hremoval]
   have hcard := Finset.card_union_of_disjoint hdisj
   have hlargeNat : Fintype.card V < 2 * (B.card + E.card) := by
     simpa only [hcard] using Nat.lt_of_not_ge hunion
@@ -1085,7 +1064,7 @@ private theorem prune_permutation_multigraph {V ι : Type*}
     exact_mod_cast hlargeNat
   have hlarge :
       (Fintype.card V : ℝ) / 2 - (B.card : ℝ) < (E.card : ℝ) := by
-    linarith
+    linarith only [hlargeCast]
   exact large_cut_lower hgap (Nat.cast_nonneg _) (Nat.cast_nonneg _)
     hdeleted hsmall hlarge hcut
 
@@ -1152,7 +1131,7 @@ theorem exists_pruned_expander {V ι : Type*}
         (B.card : ℝ) ≤ (Fintype.card V : ℝ) - (B.card : ℝ) := by
       have hcast : 2 * (B.card : ℝ) ≤ (Fintype.card V : ℝ) := by
         exact_mod_cast hhalf
-      linarith
+      linarith only [hcast]
     have hlow := hadd B
     rw [min_eq_left hhalfReal] at hlow
     exact bad_cut_card_bound hgap hlow hB
@@ -1478,7 +1457,7 @@ private theorem permutation_squared_increment_le_twice_decreasing
         (fun x : α => d x < 0) (fun x => |d x|)
   have habs_total : (∑ x, |d x|) = -2 * B.sum d := by
     rw [← habs_split, habs_bad, habs_good]
-    linarith
+    linarith only [hsplit]
   have hbad : -(B.sum d) ≤ (B.card : ℝ) := by
     calc
       -(B.sum d) = B.sum (fun x => -d x) := by
@@ -1493,10 +1472,10 @@ private theorem permutation_squared_increment_le_twice_decreasing
     intro x _
     by_cases h : 0 ≤ d x
     · rw [abs_of_nonneg h]
-      nlinarith [hupper x]
+      nlinarith only [h, hupper x]
     · have hneg : d x < 0 := lt_of_not_ge h
       rw [abs_of_neg hneg]
-      nlinarith [hlower x]
+      nlinarith only [h, hlower x]
   rw [habs_total] at hsquare
   have hfinal : (∑ x, d x ^ 2) ≤ 2 * (B.card : ℝ) := by
     linarith
@@ -1685,7 +1664,7 @@ theorem retained_bad_density_tendsto_zero
     exact_mod_cast (hU n).card_pos
   have hmass : ((V n).card : ℝ) ≤ 2 * (U n).card := by
     have h := (le_div_iff₀ hv).1 hn
-    linarith
+    linarith only [h]
   have hbadcard :
       ((U n ∩ B n).card : ℝ) ≤ (V n ∩ B n).card := by
     exact_mod_cast Finset.card_le_card
@@ -4169,7 +4148,7 @@ theorem componentVertexMidrank_le_one {V : Type*}
     apply (div_le_one hc).2
     have heq : 0 ≤ ((C.filter fun z => b z = b x).card : ℝ) := by
       positivity
-    linarith
+    linarith only [hcard']
 
 private theorem componentVertexMidrank_mono {V : Type*}
     (C : Finset V) (b : V → ℤ) {x y : V}
@@ -5381,10 +5360,10 @@ private theorem shifted_floor_drop_subset_two_intervals
   rcases hcases with hcase | hcase
   · left
     rw [hcase] at hv' hu'
-    exact ⟨by linarith, by linarith⟩
+    exact ⟨by linarith only [hu'], by linarith only [hv']⟩
   · right
     rw [hcase] at hv' hu'
-    exact ⟨by linarith, by linarith⟩
+    exact ⟨by linarith only [hu'], by linarith only [hv']⟩
 
 private theorem measurableSet_shifted_floor_drop (u v H : ℝ) :
     MeasurableSet
@@ -5578,11 +5557,11 @@ private theorem shifted_floor_drop_volume_bound_sharp
   have hc0 : 0 ≤ c := by
     dsimp [c]
     push_cast
-    linarith
+    linarith only [hkhi']
   have hcH : c ≤ H := by
     dsimp [c]
     push_cast
-    linarith
+    linarith only [hklo']
   let A : Set ℝ := Set.Ico 0 (max 0 (c - H + d))
   let B : Set ℝ := Set.Ico c (min H (c + d))
   have hsubset :
@@ -5598,7 +5577,7 @@ private theorem shifted_floor_drop_volume_bound_sharp
       · have hupper := hleft.2
         dsimp [c, d]
         push_cast
-        linarith
+        linarith only [hupper]
       · exact le_max_right _ _
     · right
       change r ∈ Set.Ico c (min H (c + d))
@@ -5609,7 +5588,7 @@ private theorem shifted_floor_drop_volume_bound_sharp
       · have hupper := hright.2
         dsimp [c, d]
         push_cast at hupper ⊢
-        linarith
+        linarith only [hupper]
   have hA : MeasureTheory.volume A =
       ENNReal.ofReal (max 0 (c - H + d)) := by
     dsimp [A]
@@ -5621,13 +5600,13 @@ private theorem shifted_floor_drop_volume_bound_sharp
   have hA0 : 0 ≤ max 0 (c - H + d) := le_max_left _ _
   have hB0 : 0 ≤ min H (c + d) - c := by
     apply sub_nonneg.mpr
-    exact le_min hcH (by linarith)
+    exact le_min hcH (by linarith only [hvu])
   have hlength : max 0 (c - H + d) + (min H (c + d) - c) = d := by
     by_cases hshort : d ≤ H - c
-    · rw [max_eq_left (by linarith), min_eq_right (by linarith)]
+    · rw [max_eq_left (by linarith only [hshort]), min_eq_right (by linarith only [hshort])]
       ring
     · have hlong : H - c < d := lt_of_not_ge hshort
-      rw [max_eq_right (by linarith), min_eq_left (by linarith)]
+      rw [max_eq_right (by linarith only [hshort]), min_eq_left (by linarith only [hshort])]
       ring
   calc
     MeasureTheory.volume
@@ -5707,7 +5686,7 @@ private theorem exists_common_rank_offset_one_sided_sharp
     intro i hi
     by_cases hle : v i ≤ u i
     · rw [min_eq_left hle]
-      linarith [hone i]
+      linarith only [hone i]
     · rw [min_eq_right (le_of_not_ge hle), sub_self]
       exact hdelta i
   calc
@@ -5762,7 +5741,7 @@ private theorem abs_log_one_sub_le_two_mul
     |Real.log (1 - eta)| ≤ 2 * eta := by
   have hfactor : 0 < 1 - eta := by linarith
   have hlog : Real.log (1 - eta) ≤ 0 :=
-    Real.log_nonpos hfactor.le (by linarith)
+    Real.log_nonpos hfactor.le (by linarith only [heta0])
   rw [abs_of_nonpos hlog]
   have hlower := Real.one_sub_inv_le_log_of_pos hfactor
   have hratio : eta / (1 - eta) ≤ 2 * eta := by
@@ -6357,7 +6336,7 @@ theorem matchedRetainedSupport_cover_density_tendsto_one
     have hden : ((U n).card : ℝ) ≠ 0 := by
       exact_mod_cast (hU n).card_pos.ne'
     field_simp
-    linarith
+    linarith only [hreal]
   have hlimit : Tendsto
       (fun n =>
         (1 : ℝ) - (((U n \ matchedRetainedSupport (R n)).card : ℝ) /
@@ -6598,7 +6577,7 @@ theorem matchedRetained_bad_density_tendsto_zero
   have hmass :
       ((U n).card : ℝ) ≤ 2 * (matchedRetainedSupport (R n)).card := by
     have h := (le_div_iff₀ hucard).1 hn
-    linarith
+    linarith only [h]
   have hbadcard :
       ((matchedRetainedSupport (R n) ∩ B n).card : ℝ) ≤
         (U n ∩ B n).card := by
@@ -7780,7 +7759,7 @@ private theorem partitionVertexMidrank_permutation_energy_le
         ((partitionWordCrossing P p).card : ℝ) +
           ((rankDecreasingVertices Finset.univ b p).card : ℝ) := by
     exact_mod_cast hcard
-  nlinarith
+  nlinarith only [hbase, hcast]
 
 private theorem sum_partitionVertexMidrank_permutation_energy_le
     {V ι : Type*} [Fintype V] [DecidableEq V]
@@ -8305,7 +8284,7 @@ private theorem almostCentralizerGap_of_expansion {V ι : Type*}
       mul_pos hpositive (sub_pos.mpr hlarge')
     change h * (permutationDistance p.permutation q.permutation : ℝ) ≤ _
       at hnear
-    nlinarith
+    nlinarith only [hsmall, hdef, hpos, hnear]
   · right
     by_contra hnot
     have hlarge :
@@ -8321,7 +8300,7 @@ private theorem almostCentralizerGap_of_expansion {V ι : Type*}
       mul_nonneg hpositive.le (sub_nonneg.mpr hlarge')
     change h * ((Fintype.card V : ℝ) -
       permutationDistance p.permutation q.permutation) ≤ _ at hfar
-    nlinarith
+    nlinarith only [hsmall, hdef, hpos, hfar]
 
 private def almostCentralizerSetoid {V ι : Type*}
     [Fintype V] [Fintype ι] [DecidableEq V]
@@ -8917,7 +8896,7 @@ theorem exists_positive_antitone_slow_overlap_scales
   have hquot (n : ℕ) : eta n / H n = H n := by
     dsimp [H]
     apply (div_eq_iff (Real.sqrt_pos.2 (heta_pos n)).ne').2
-    nlinarith [Real.sq_sqrt (heta_pos n).le]
+    nlinarith only [heta_pos, Real.sq_sqrt (heta_pos n).le]
   have hquot_zero : Tendsto (fun n => eta n / H n) atTop (nhds 0) := by
     have hfun : (fun n => eta n / H n) = H := funext hquot
     rw [hfun]
diff --git a/LeanPool/NonSoficGroup/Spectral.lean b/LeanPool/NonSoficGroup/Spectral.lean
index cab70580ea..8ac1b31600 100644
--- a/LeanPool/NonSoficGroup/Spectral.lean
+++ b/LeanPool/NonSoficGroup/Spectral.lean
@@ -18,7 +18,8 @@ import Mathlib.Data.Nat.Dist
 import Mathlib.Data.Finset.CastCard
 import Mathlib.Dynamics.FixedPoints.Topology
 import Mathlib.RepresentationTheory.Invariants
-import Mathlib.Topology.Algebra.LinearMapCompletion
+-- Retain the instance environment used by the finite-field basis.
+import Mathlib.Topology.Algebra.LinearMapCompletion -- shake: keep
 
 /-!
 # Spectral and finite-model estimates for the non-sofic group construction
@@ -48,7 +49,8 @@ theorem three_pair_sum_norm_sq (a b c : H) :
       RCLike.re (inner ℂ c a) = RCLike.re (inner ℂ a c) := by
     exact @inner_re_symm ℂ H _ _ _ c a
   simp only [@norm_add_sq ℂ H, inner_add_left, map_add]
-  nlinarith
+  rw [hca]
+  ring
 
 omit [InnerProductSpace ℂ H] in
 private theorem norm_add_three_sq_le_three_mul (a b c : H) :
@@ -60,7 +62,7 @@ private theorem norm_add_three_sq_le_three_mul (a b c : H) :
   have hsquare :
       ‖a + b + c‖ ^ 2 ≤ (‖a‖ + ‖b‖ + ‖c‖) ^ 2 :=
     (sq_le_sq₀ (norm_nonneg _) (by positivity)).mpr htriangle
-  nlinarith [sq_nonneg (‖a‖ - ‖b‖),
+  linarith only [hsquare, sq_nonneg (‖a‖ - ‖b‖),
     sq_nonneg (‖b‖ - ‖c‖), sq_nonneg (‖c‖ - ‖a‖)]
 
 private theorem three_pairwise_residual_spectral_gap
@@ -70,7 +72,7 @@ private theorem three_pairwise_residual_spectral_gap
     (hca : (1 - ε) * (‖c‖ ^ 2 + ‖a‖ ^ 2) ≤ ‖c + a‖ ^ 2) :
     (1 - 2 * ε) * (‖a‖ ^ 2 + ‖b‖ ^ 2 + ‖c‖ ^ 2) ≤
       ‖a + b + c‖ ^ 2 := by
-  nlinarith [three_pair_sum_norm_sq a b c]
+  linarith only [hab, hbc, hca, three_pair_sum_norm_sq a b c]
 
 end ThreeProjectionSumOfSquares
 
@@ -107,7 +109,8 @@ private theorem inner_sq_le_of_orthogonal_two_sector
       8 * (‖inner ℂ a₀ b₀‖ + ‖inner ℂ a₁ b₁‖) ^ 2 ≤
         (‖a₀‖ ^ 2 + ‖a₁‖ ^ 2) *
           (‖b₀‖ ^ 2 + ‖b₁‖ ^ 2) := by
-    nlinarith [sq_nonneg (‖a₀‖ * ‖b₁‖ - ‖a₁‖ * ‖b₀‖)]
+    linarith only [h₀, h₁, hcross,
+      sq_nonneg (‖a₀‖ * ‖b₁‖ - ‖a₁‖ * ‖b₀‖)]
   have hinner :
       inner ℂ (a₀ + a₁) (b₀ + b₁) =
         inner ℂ a₀ b₀ + inner ℂ a₁ b₁ := by
@@ -129,7 +132,7 @@ private theorem inner_sq_le_of_orthogonal_two_sector
     rw [norm_add_sq (𝕜 := ℂ), hb]
     simp only [RCLike.re_to_complex, Complex.zero_re, mul_zero, add_zero]
   rw [ha', hb']
-  nlinarith
+  exact (mul_le_mul_of_nonneg_left hnormsq (by norm_num : (0 : ℝ) ≤ 8)).trans hscalar
 
 private theorem inner_sq_le_of_finite_orthogonal_sector_splitting
     {ι : Type*} [Finite ι]
@@ -244,24 +247,7 @@ private theorem ejStarProjection_re_inner (W : Submodule ℂ H)
     [W.HasOrthogonalProjection] (x : H) :
     RCLike.re (inner ℂ (W.starProjection x) x) =
       ‖W.starProjection x‖ ^ 2 := by
-  have hidem : W.starProjection (W.starProjection x) =
-      W.starProjection x :=
-    Submodule.starProjection_eq_self_iff.mpr
-      (Submodule.starProjection_apply_mem W x)
-  have hinner :
-      inner ℂ (W.starProjection x) x =
-        inner ℂ (W.starProjection x) (W.starProjection x) := by
-    calc
-      inner ℂ (W.starProjection x) x =
-          inner ℂ x (W.starProjection x) :=
-        Submodule.inner_starProjection_left_eq_right W x x
-      _ = inner ℂ x (W.starProjection (W.starProjection x)) :=
-        congrArg (inner ℂ x) hidem.symm
-      _ = inner ℂ (W.starProjection x) (W.starProjection x) :=
-        (Submodule.inner_starProjection_left_eq_right W x
-          (W.starProjection x)).symm
-  rw [hinner]
-  exact (norm_sq_eq_re_inner _).symm
+  exact W.re_inner_starProjection_eq_normSq x
 
 private def ejResidualProjection (V : Submodule ℂ H)
     [V.HasOrthogonalProjection] : H →L[ℂ] H :=
@@ -291,24 +277,7 @@ private theorem ejResidualProjection_re_inner (V : Submodule ℂ H)
     [V.HasOrthogonalProjection] (x : H) :
     RCLike.re (inner ℂ (ejResidualProjection V x) x) =
       ‖ejResidualProjection V x‖ ^ 2 := by
-  have hinner :
-      inner ℂ (ejResidualProjection V x) x =
-        inner ℂ (ejResidualProjection V x)
-          (ejResidualProjection V x) := by
-    calc
-      inner ℂ (ejResidualProjection V x) x =
-          inner ℂ x (ejResidualProjection V x) :=
-        ejResidualProjection_inner V x x
-      _ = inner ℂ x
-          (ejResidualProjection V (ejResidualProjection V x)) :=
-        congrArg (inner ℂ x)
-          (ejResidualProjection_idempotent V x).symm
-      _ = inner ℂ (ejResidualProjection V x)
-          (ejResidualProjection V x) :=
-        (ejResidualProjection_inner V x
-          (ejResidualProjection V x)).symm
-  rw [hinner]
-  exact (norm_sq_eq_re_inner _).symm
+  exact ejStarProjection_re_inner Vᗮ x
 
 variable (V : Fin 3 → Submodule ℂ H)
   [∀ i, (V i).HasOrthogonalProjection]
@@ -357,10 +326,9 @@ private theorem ejThreeResidualEnergy_eq_re_inner (x : H) :
 private theorem ejThreeResidualMap_norm_sq_le (x : H) :
     ‖ejThreeResidualMap V x‖ ^ 2 ≤
       3 * ejThreeResidualEnergy V x := by
-  simpa only [ejThreeResidualMap_apply, Fin.isValue, ejResidualProjection_apply,
-    ejThreeResidualEnergy] using
-    norm_add_three_sq_le_three_mul (ejResidualProjection (V 0) x) (ejResidualProjection (V 1) x)
-      (ejResidualProjection (V 2) x)
+  exact norm_add_three_sq_le_three_mul
+    (ejResidualProjection (V 0) x) (ejResidualProjection (V 1) x)
+    (ejResidualProjection (V 2) x)
 
 private theorem ejResidualProjection_norm_le (i : Fin 3) (x : H) :
     ‖ejResidualProjection (V i) x‖ ≤ ‖x‖ :=
@@ -453,7 +421,7 @@ private theorem ejThreeResidualEnergy_average (x : H) :
     ejResidualProjection_average_norm_sq (V 1),
     ejResidualProjection_average_norm_sq (V 2)]
   have hcross := ejThreeResidual_cross_re_inner V x
-  nlinarith
+  linarith only [hcross]
 
 private theorem ejThreeResidualMap_spectral_gap (x : H) (ε : ℝ)
     (h01 : (1 - ε) *
@@ -488,7 +456,7 @@ private theorem ejThreeResidualEnergy_average_le
   rw [ejThreeResidualEnergy_average]
   have hupper := ejThreeResidualEnergy_le_three_norm_sq V
     (ejThreeResidualMap V x)
-  nlinarith
+  linarith only [hupper, hgap]
 
 private theorem ejStarProjection_mem_inf_orthogonal
     (U V : Submodule ℂ H) [U.HasOrthogonalProjection]
@@ -531,7 +499,7 @@ private theorem ejTwoProjection_norm_sq_sum_le_of_angle
       ‖u + v‖ ^ 2 ≤
         (1 + c) * (‖u‖ ^ 2 + ‖v‖ ^ 2) := by
     rw [norm_add_sq (𝕜 := ℂ)]
-    nlinarith [mul_nonneg hc (sq_nonneg (‖u‖ - ‖v‖))]
+    linarith only [hre, mul_nonneg hc (sq_nonneg (‖u‖ - ‖v‖))]
   have huinner :
       (inner ℂ (U.starProjection w) w).re =
         ‖U.starProjection w‖ ^ 2 := by
@@ -607,7 +575,7 @@ private theorem ejTwoResidualEnergy_ge_of_angle
       ‖ejResidualProjection V w‖ ^ 2 at hV
   have hsum :=
     ejTwoProjection_norm_sq_sum_le_of_angle U V c hc hangle w hw
-  nlinarith
+  linarith only [hU, hV, hsum]
 
 private theorem ejTwoResidual_sum_re_inner
     (U V : Submodule ℂ H)
@@ -617,21 +585,8 @@ private theorem ejTwoResidual_sum_re_inner
       (ejResidualProjection U w + ejResidualProjection V w) w) =
         ‖ejResidualProjection U w‖ ^ 2 +
           ‖ejResidualProjection V w‖ ^ 2 := by
-  have hU :
-      (inner ℂ (ejResidualProjection U w) w).re =
-        ‖ejResidualProjection U w‖ ^ 2 := by
-    change RCLike.re (inner ℂ (ejResidualProjection U w) w) = _
-    exact ejResidualProjection_re_inner U w
-  have hV :
-      (inner ℂ (ejResidualProjection V w) w).re =
-        ‖ejResidualProjection V w‖ ^ 2 := by
-    change RCLike.re (inner ℂ (ejResidualProjection V w) w) = _
-    exact ejResidualProjection_re_inner V w
-  change
-    (inner ℂ
-      (ejResidualProjection U w + ejResidualProjection V w) w).re = _
-  simp only [inner_add_left, Complex.add_re]
-  rw [hU, hV]
+  rw [inner_add_left, map_add, ejResidualProjection_re_inner,
+    ejResidualProjection_re_inner]
 
 private theorem ejTwoResidual_spectral_gap_of_angle
     (U V : Submodule ℂ H)
@@ -722,7 +677,7 @@ private theorem ejThreeProjectionAverage_dist_sq_le (x : H) :
       ejThreeResidualEnergy V x / 3 := by
   rw [ejThreeProjectionAverage_dist_sq]
   have h := ejThreeResidualMap_norm_sq_le V x
-  nlinarith
+  linarith only [h]
 
 private theorem ejThreeResidualEnergy_iterate_le
     (δ : ℝ) (hδ : δ ≤ 3)
@@ -848,7 +803,7 @@ private theorem ejThreeProjectionAverage_iterate_dist_le_of_pair_angles
         (1 - (1 - 2 * c) / 6) ^ n := by
   have hc' : c ≤ 1 := by linarith
   apply ejThreeProjectionAverage_iterate_dist_le_geometric V
-    (1 - 2 * c) (by linarith)
+    (1 - 2 * c) (by linarith only [hc])
   intro y
   exact ejThreeResidual_spectral_gap_of_pair_angles
     V c hc hc' hangle y
@@ -867,7 +822,7 @@ private theorem ejThreeResidualEnergy_sqrt_div_three_le
   apply Real.sqrt_le_iff.mpr
   refine ⟨hT, ?_⟩
   unfold ejThreeResidualEnergy
-  nlinarith
+  linarith only [h₀, h₁, h₂]
 
 private theorem ejThreeProjectionAverage_fixed_iff_residualMap_eq_zero (x : H) :
     ejThreeProjectionAverage V x = x ↔
@@ -896,13 +851,16 @@ private theorem ejThreeResidualEnergy_eq_zero_iff (x : H) :
     fin_cases i
     · change ejResidualProjection (V 0) x = 0
       apply norm_eq_zero.mp
-      nlinarith [norm_nonneg (ejResidualProjection (V 0) x)]
+      apply sq_eq_zero_iff.mp
+      linarith only [h, h₀, h₁, h₂]
     · change ejResidualProjection (V 1) x = 0
       apply norm_eq_zero.mp
-      nlinarith [norm_nonneg (ejResidualProjection (V 1) x)]
+      apply sq_eq_zero_iff.mp
+      linarith only [h, h₀, h₁, h₂]
     · change ejResidualProjection (V 2) x = 0
       apply norm_eq_zero.mp
-      nlinarith [norm_nonneg (ejResidualProjection (V 2) x)]
+      apply sq_eq_zero_iff.mp
+      linarith only [h, h₀, h₁, h₂]
   · intro h
     unfold ejThreeResidualEnergy
     simp only [Fin.isValue, h 0, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow,
@@ -1136,7 +1094,7 @@ private theorem hasPropertyT_of_geometric_finite_averaging
       _ < (1 - q) / 2 := by
         dsimp [δ]
         have hpos : 0 < (1 - q) := sub_pos.mpr hq1
-        have hc : (S.card : ℝ) < (S.card : ℝ) + 1 := by linarith
+        have hc : (S.card : ℝ) < (S.card : ℝ) + 1 := by linarith only []
         have hcpos : 0 < (S.card : ℝ) + 1 := by positivity
         rw [show (2 * (↑S.card + 1) : ℝ) =
           2 * ((S.card : ℝ) + 1) by norm_cast]
@@ -1158,8 +1116,8 @@ private theorem hasPropertyT_of_geometric_finite_averaging
     rw [hone] at hdist
     have hden : 0 < 1 - q := sub_pos.mpr hq1
     have hlt : C / (1 - q) < 1 / 2 :=
-      (div_lt_iff₀ hden).mpr (by nlinarith [hhalf])
-    linarith
+      (div_lt_iff₀ hden).mpr (by nlinarith only [hhalf])
+    linarith only [hdist, hlt]
   exact ⟨η, hηne, hfixed η hηfixed⟩
 
 private def threeFiniteSubgroupGenerators
@@ -1259,10 +1217,10 @@ private theorem norm_inner_le_inv_sqrt_eight_of_sq
       ‖inner ℂ a b‖ ^ 2 ≤
           (‖a‖ ^ 2 * ‖b‖ ^ 2) / 8 := by
             apply (le_div_iff₀ (show (0 : ℝ) < 8 by norm_num)).mpr
-            nlinarith
+            nlinarith only [h]
       _ = ((Real.sqrt (8 : ℝ))⁻¹ * ‖a‖ * ‖b‖) ^ 2 := by
         field_simp
-        nlinarith
+        nlinarith only [h, hsquare]
   exact (sq_le_sq₀ (norm_nonneg _) (by positivity)).mp hsq
 
 private theorem hasPropertyT_of_three_finite_subgroups_friedrichs_angle
@@ -1292,7 +1250,7 @@ private theorem hasPropertyT_of_three_finite_subgroups_friedrichs_angle
     linarith
   have hqnonneg : 0 ≤ q := by
     dsimp [q]
-    linarith
+    linarith only [hc]
   apply hasPropertyT_of_three_finite_subgroups_geometric K hgen q hq
   intro H _ _ _ π
   let V : Fin 3 → Submodule ℂ H :=
@@ -3884,7 +3842,7 @@ private theorem excess_mass_le_of_diagonal_variation
       (permutationVariation σ (fun x => f x - 1) : ℝ) ≤
         2 * (B : ℝ) := by
     exact_mod_cast htotal
-  linarith
+  linarith only [hcoarea, htotal_real]
 
 private theorem zero_mass_le_of_diagonal_variation
     {V ι : Type*} [Fintype V] [Fintype ι] [DecidableEq V]
@@ -3915,7 +3873,7 @@ private theorem zero_mass_le_of_diagonal_variation
         (Finset.univ.filter fun x : V => f x = 0).card := by
     simp only [Finset.sum_boole, Nat.cast_id]
   rw [hsum] at hcoarea
-  linarith
+  linarith only [hcoarea, htotal_real]
 
 private theorem first_excess_mass_le_diagonalBoundary
     {V ι : Type*} [Fintype V] [Fintype ι] [DecidableEq V]
@@ -4285,7 +4243,7 @@ private theorem matchedFiberEdges_relation_loss_bound
       ring
     _ ≤ 4 * (boundary
           (fun i => (σ i).prodCongr (σ i)) U : ℝ) := by
-      linarith
+      linarith only [hrow', hcol']
 
 private theorem matchedFiberEdges_vertex_loss_bound
     {V ι : Type*} [Fintype V] [Fintype ι] [DecidableEq V]
@@ -4342,7 +4300,7 @@ private theorem matchedFiberEdges_vertex_loss_bound
       ring
     _ ≤ 4 * (boundary
           (fun i => (σ i).prodCongr (σ i)) U : ℝ) := by
-      linarith
+      linarith only [hzero, hrow', hcol']
 
 private theorem exists_permutation_extending_matchedFiberEdges
     {V : Type*} [DecidableEq V] (U : Finset (V × V)) :
@@ -4564,7 +4522,7 @@ private theorem exists_boundary_controlled_permutation_repair
             ((U \ matchedFiberEdges U).card : ℝ)) ≤
         8 * (boundary
           (fun i => (σ i).prodCongr (σ i)) U : ℝ) := by
-    nlinarith
+    nlinarith only [hvertex, hrelation]
   have hdnonneg : (0 : ℝ) ≤ Fintype.card ι := by
     positivity
   have hscaled := mul_le_mul_of_nonneg_left hsum hdnonneg
@@ -4581,7 +4539,7 @@ private theorem exists_boundary_controlled_permutation_repair
     _ ≤ (h + 8 * (Fintype.card ι : ℝ)) *
           (boundary
             (fun i => (σ i).prodCongr (σ i)) U : ℝ) := by
-      nlinarith
+      nlinarith only [hscaled]
 
 private theorem permutationDistance_eq_card_permutationGraph_sdiff
     {V : Type*} [Fintype V] [DecidableEq V]
@@ -4684,7 +4642,7 @@ private theorem exists_boundary_controlled_permutation_repair_close_to_reference
     σ U h hpositive hexp hfirst hsecond
   refine ⟨q, ?_, hdefect⟩
   have hscaled := mul_le_mul_of_nonneg_left hdistance_real hpositive.le
-  nlinarith
+  nlinarith only [hvertex, hscaled]
 
 private theorem hasAlmostCentralizerImprovement_of_expanding_diagonal_cuts
     {V ι : Type*} [Fintype V] [Fintype ι] [DecidableEq V]
@@ -4720,7 +4678,7 @@ private theorem hasAlmostCentralizerImprovement_of_expanding_diagonal_cuts
   have hdefect_real :
       (permutationCommutationDefect σ q : ℝ) ≤
         (tolerance : ℝ) := by
-    nlinarith
+    nlinarith only [hpositive, hcutdefect, hqdefect]
   have hdefect :
       permutationCommutationDefect σ q ≤ tolerance := by
     exact_mod_cast hdefect_real
@@ -4729,7 +4687,7 @@ private theorem hasAlmostCentralizerImprovement_of_expanding_diagonal_cuts
   have hdistance_real :
       (5 : ℝ) * (permutationDistance q p : ℝ) ≤
         (Fintype.card V : ℝ) := by
-    nlinarith
+    nlinarith only [hpositive, hcutdistance, hqdistance]
   have hdistance :
       5 * permutationDistance q p ≤ Fintype.card V := by
     exact_mod_cast hdistance_real
@@ -6359,13 +6317,15 @@ private theorem norm_add_le_two_sub_sq_div_four
     (sq_le_sq₀ (mul_nonneg hδ (norm_nonneg x))
       (norm_nonneg (x - y))).mpr hseparated
   have hδsq : δ ^ 2 ≤ 4 := by
-    nlinarith [sq_nonneg (2 - δ), sq_nonneg δ]
+    calc
+      δ ^ 2 ≤ 2 ^ 2 := pow_le_pow_left₀ hδ hδtwo 2
+      _ = 4 := by norm_num
   have htarget : 0 ≤ (2 - δ ^ 2 / 4) * ‖x‖ :=
-    mul_nonneg (by nlinarith) (norm_nonneg x)
+    mul_nonneg (by linarith only [hδsq]) (norm_nonneg x)
   have hadd :
       ‖x + y‖ ^ 2 ≤ ((2 - δ ^ 2 / 4) * ‖x‖) ^ 2 := by
     rw [hnorm] at hpar
-    nlinarith [sq_nonneg (δ ^ 2 * ‖x‖)]
+    linarith only [hpar, hsq, sq_nonneg (δ ^ 2 * ‖x‖)]
   exact (sq_le_sq₀ (norm_nonneg (x + y)) htarget).mp hadd
 
 omit [InnerProductSpace ℂ H] in
@@ -7412,7 +7372,7 @@ private theorem modelSeparationBad_density_tendsto_zero
   simp only [modelSeparationBad, normalizedHamming,
     Fintype.card_fin]
   field_simp
-  linarith
+  linarith only [hreal]
 
 private def finiteMultiplicationBad {G : Type*} [Group G]
     (M : PermutationModel G) (F : Finset G) :
@@ -8710,11 +8670,11 @@ private theorem exists_expanding_residual_finpartition
             _ ≤ (boundary σ R : ℝ) +
                   2 * (boundary σ U : ℝ) +
                     4 * α * ((R \ C).card : ℝ) := by
-                  linarith
+                  linarith only [hsplit]
             _ ≤ (boundary σ R : ℝ) +
                   4 * α * (C.card : ℝ) +
                     4 * α * ((R \ C).card : ℝ) := by
-                  linarith
+                  linarith only [hUcost]
             _ = (boundary σ R : ℝ) +
                   4 * α * (R.card : ℝ) := by
                   linear_combination (4 * α) * hcard
@@ -8775,7 +8735,7 @@ private theorem exists_expanding_clean_finpartition
                 (boundary σ B : ℝ) ≤
                   (Fintype.card ι : ℝ) * (B.card : ℝ) := by
               exact_mod_cast hdegree
-            linarith
+            linarith only [hdegreeReal]
 
 private noncomputable def completeCleanFinpartition
     {V : Type*} [Fintype V] [DecidableEq V]
@@ -8942,7 +8902,7 @@ private theorem exists_expanding_full_finpartition
             add_le_add hQbudget hbad
       _ ≤ 2 * (Fintype.card ι : ℝ) * (B.card : ℝ) +
           4 * α * (Fintype.card V : ℝ) := by
-            nlinarith
+            nlinarith only [hscaled]
 
 public
 theorem exists_expanding_full_finpartition_sequence

From c0f50e5a68a929ed8327b5dcb8cc2ebbb8c03217 Mon Sep 17 00:00:00 2001
From: Vasily Ilin <vasilin97@gmail.com>
Date: Sun, 18 Oct 2026 18:21:03 +0000
Subject: [PATCH 2/2] Factor central-sector projection proofs and preserve
 exact declaration types

---
 LeanPool/NonSoficGroup/Compression.lean |  48 ++++-----
 LeanPool/NonSoficGroup/Conclusion.lean  |   3 -
 LeanPool/NonSoficGroup/Foundations.lean |  42 +++-----
 LeanPool/NonSoficGroup/Spectral.lean    | 138 ++++++++++++------------
 4 files changed, 108 insertions(+), 123 deletions(-)

diff --git a/LeanPool/NonSoficGroup/Compression.lean b/LeanPool/NonSoficGroup/Compression.lean
index cabf390e2e..838e8212fa 100644
--- a/LeanPool/NonSoficGroup/Compression.lean
+++ b/LeanPool/NonSoficGroup/Compression.lean
@@ -499,7 +499,7 @@ private theorem card_symmDiff_upperLevel_le_nine_sq_error {V : Type*}
     · obtain ⟨hxlevel, hxT⟩ := hx
       have hfx : t < f x := (Finset.mem_filter.mp hxlevel).2
       simp only [ite_eq_right hxT]
-      nlinarith [sq_nonneg (3 * f x - 1)]
+      linarith only [hlow, hfx, sq_nonneg (3 * f x - 1)]
     · obtain ⟨hxT, hxlevel⟩ := hx
       have hfx : f x ≤ t := by
         apply le_of_not_gt
@@ -507,7 +507,7 @@ private theorem card_symmDiff_upperLevel_le_nine_sq_error {V : Type*}
         exact hxlevel
           (Finset.mem_filter.mpr ⟨Finset.mem_univ x, h⟩)
       simp only [ite_eq_left hxT]
-      nlinarith only [hhigh, hfx, sq_nonneg (3 * f x - 2)]
+      linarith only [hhigh, hfx, sq_nonneg (3 * f x - 2)]
   have hcard :
       (D.card : ℝ) = ∑ x : V, if x ∈ D then (1 : ℝ) else 0 := by
     simp only [Finset.sum_ite_mem, Finset.univ_inter, Finset.sum_const, nsmul_eq_mul, mul_one]
@@ -631,9 +631,6 @@ private theorem sum_sum_sq_displacement_eq_twice_card_mul_realMarkov_residual
       2 * (Fintype.card ι : ℝ) *
         ∑ x : V, f x * (f x - realMarkov σ f x) := by
   classical
-  have hd : 0 < (Fintype.card ι : ℝ) := by
-    exact_mod_cast Fintype.card_pos_iff.mpr
-      (inferInstance : Nonempty ι)
   calc
     (∑ i : ι, ∑ x : V, (f (σ i x) - f x) ^ 2) =
         2 * ∑ x : V, ∑ i : ι,
@@ -664,7 +661,10 @@ private theorem sum_sq_le_card_of_unit_interval_mass
     (∑ x : V, f x ^ 2) ≤ ∑ x : V, f x := by
       apply Finset.sum_le_sum
       intro x _
-      nlinarith only [mul_nonneg (hfzero x) (sub_nonneg.mpr (hfone x))]
+      calc
+        f x ^ 2 = f x * f x := pow_two _
+        _ ≤ f x * 1 := mul_le_mul_of_nonneg_left (hfone x) (hfzero x)
+        _ = f x := mul_one _
     _ = (T.card : ℝ) := hmass
 
 private theorem realMarkov_residual_pairing_le_sqrt_card_mul_residual
@@ -712,7 +712,7 @@ private theorem sum_sum_sq_displacement_le_twice_card_mul_sqrt_card_mul_residual
   have hpair := realMarkov_residual_pairing_le_sqrt_card_mul_residual
     σ T f hfzero hfone hmass
   have hfactor : 0 ≤ 2 * (Fintype.card ι : ℝ) := by positivity
-  nlinarith only [hpair, hfactor, mul_nonneg hfactor (sub_nonneg.mpr hpair)]
+  linarith only [hpair, hfactor, mul_nonneg hfactor (sub_nonneg.mpr hpair)]
 
 private theorem card_highSupport_le_three_card
     {V : Type*} [Fintype V]
@@ -1230,7 +1230,7 @@ theorem symmDiff_card_lt_of_overlap_and_exp_card
       ((C ∆ D).card : ℝ) + 2 * ((C ∩ D).card : ℝ) =
         (C.card : ℝ) + (D.card : ℝ) := by
     exact_mod_cast card_symmDiff_add_twice_inter C D
-  nlinarith
+  linarith only [hoverlap, hcard, hexact]
 
 public
 theorem target_majority_of_overlap_and_exp_card
@@ -1299,7 +1299,7 @@ theorem symmDiff_density_tendsto_zero_of_log_rank_bounds
   have hexp : 1 ≤ Real.exp (H n) := by
     simpa only [Real.one_le_exp_iff, Real.exp_zero] using (Real.exp_le_exp.mpr (hH n))
   have hnonneg : 0 ≤ Real.exp (H n) - 1 + 2 * eta n := by
-    nlinarith only [hexp, heta n]
+    linarith only [heta, hexp, heta n]
   have hmassnat :
       (∑ C ∈ R n, C.card) ≤ (U n).card := by
     calc
@@ -2248,8 +2248,6 @@ private theorem reference_difference_le_of_good_root_threshold
   have hd : 0 < (Fintype.card ι : ℝ) := by
     exact_mod_cast Fintype.card_pos_iff.mpr
       (inferInstance : Nonempty ι)
-  have hden : 0 < (Fintype.card ι : ℝ) * (1 - q) ^ 2 :=
-    mul_pos hd (sq_pos_of_pos (sub_pos.mpr hq))
   have hdefect_real :
       (permutationCommutationDefect σ p : ℝ) ≤
         2 * (t : ℝ) := by
@@ -2618,7 +2616,7 @@ private theorem close_and_large_of_symmDiff_bound
             mul_le_mul_of_nonneg_left hdistance (by norm_num)
           _ = 216 * boundaryValue / denominator := by ring
       _ < (T.card : ℝ) :=
-        (div_lt_iff₀ hdenominator).2 (by nlinarith only [hscaled])
+        (div_lt_iff₀ hdenominator).2 (by linarith only [hscaled])
   have hclose : 3 * (U ∆ T).card < T.card := by
     exact_mod_cast hcloseReal
   have hsub : T ⊆ U ∪ (U ∆ T) := by
@@ -2778,7 +2776,7 @@ private theorem exists_rooted_word_radius_sparse_cut_of_boundary
     have hboundary' :=
       mul_le_mul_of_nonneg_left hboundary.le
         (by norm_num : (0 : ℝ) ≤ 2)
-    nlinarith only [hscaled, hboundary']
+    linarith only [hboundary, hscaled, hboundary']
   have hsmall :
       486 * (Fintype.card (↥S) : ℝ) ^ 2 * η ≤
         4 * α ^ 2 := by
@@ -2838,7 +2836,7 @@ private theorem exists_rooted_word_radius_sparse_cut_of_boundary
     change
       (boundary X.generator
         (KunSharpThresholdCut.upperLevel f t) : ℝ) ≤ _
-    nlinarith only [hcut, hvariation, hscaledlarge]
+    linarith only [hvariation, hcut, hscaledlarge]
   exact ⟨U, by simpa only [f, χ] using hdistance,
     by simpa only [q] using hquant, hclose, hboundaryU⟩
 
@@ -3507,9 +3505,6 @@ private theorem rooted_graph_boundary_lt_of_slow_tolerance
   have hγ : 0 < γ := by
     dsimp [γ]
     positivity
-  have hC : 0 ≤ C := by
-    dsimp [C]
-    positivity
   have hslowCscaled : h * (5 * C * t) ≤ h * N := by
     have hslow' : 5 * (4 + h * C) * t ≤ h * N := by
       simpa only [C, δ] using hslow
@@ -3554,7 +3549,7 @@ private theorem rooted_graph_coefficient_small
     positivity
   constructor
   · positivity
-  · nlinarith
+  · linarith only [hgap]
 
 end KunRootedUniversalToleranceNumerics
 
@@ -5306,7 +5301,7 @@ private theorem exists_source_full_finpartition_sequence_of_kazhdan
     have hgap : 0 < (S.card : ℝ) * (1 - q) ^ 2 := by
       positivity
     dsimp [γ, q]
-    nlinarith only [hgap]
+    linarith only [hgap]
   let α : ℕ → ℝ := fun j => 1 / ((j : ℝ) + 1)
   have hα (j : ℕ) : 0 < α j := by
     dsimp [α]
@@ -6151,9 +6146,6 @@ private theorem comparisonBad_subset_partitionWordCrossing
     unfold partitionComponentSize
     rw [hpart]
   rw [hsize]
-  have hnonneg : (0 : ℝ) ≤
-      (partitionComponentSize Q x : ℝ) := by
-    positivity
   nlinarith only [heta]
 
 private noncomputable def overlapRetainedComponents
@@ -6839,8 +6831,7 @@ private theorem squaredPermutationEnergy_mul_le
       apply Finset.sum_le_sum
       intro x _
       simp only [Equiv.Perm.mul_apply]
-      nlinarith [sq_nonneg
-        ((f (p (q x)) - f (q x)) - (f (q x) - f x))]
+      linarith only [sq_nonneg ((f (p (q x)) - f (q x)) - (f (q x) - f x))]
     _ = 2 * (∑ x : V, (f (p x) - f x) ^ 2) +
           2 * (∑ x : V, (f (q x) - f x) ^ 2) := by
       rw [Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.mul_sum,
@@ -6864,9 +6855,8 @@ private theorem squaredPermutationEnergy_le_add_hammingDist
       have hp1 := hf1 (p x)
       have hx0 := hf0 x
       have hx1 := hf1 x
-      nlinarith [sq_nonneg (f (q x) - f x),
-        mul_nonneg
-          (show 0 ≤ 1 - (f (p x) - f x) by linarith)
+      linarith only [hp0, hp1, hx0, hx1, sq_nonneg (f (q x) - f x),
+        mul_nonneg (show 0 ≤ 1 - (f (p x) - f x) by linarith)
           (show 0 ≤ 1 + (f (p x) - f x) by linarith)]
   have hindicator :
       (∑ x : V, if p x = q x then (0 : ℝ) else 1) =
@@ -7605,7 +7595,7 @@ private theorem additive_permutation_median_absolute_deviation
     exact hpoint x
   refine ⟨m, hm_nonnegative, hm_one, ?_⟩
   rw [← hmass, ← hvariation]
-  nlinarith only [hp_coarea, hq_coarea]
+  linarith only [hp_coarea, hq_coarea]
 
 private theorem additive_permutation_median_variance
     {V ι : Type*} [Fintype V] [Nonempty V]
@@ -7674,7 +7664,7 @@ private theorem additive_permutation_finiteVariance
     σ γ ε hγ hε hexp f hf hf_one
   rw [← CheegerPoincare.card_mul_finiteVariance f]
     at hvariance
-  nlinarith only [hvariance]
+  linarith only [hvariance]
 
 end KunAdditiveMedianPoincare
 
diff --git a/LeanPool/NonSoficGroup/Conclusion.lean b/LeanPool/NonSoficGroup/Conclusion.lean
index 5ddd13112b..228570634a 100644
--- a/LeanPool/NonSoficGroup/Conclusion.lean
+++ b/LeanPool/NonSoficGroup/Conclusion.lean
@@ -949,8 +949,6 @@ private theorem exists_prescribed_radius_union_source_completed_tolerance
       push_cast
       ring
     · norm_num
-  have hdreal : (0 : ℝ) < d := by
-    exact_mod_cast hd
   have hden : 0 < (2 : ℝ) * (ell + 8 * (d : ℝ)) := by
     positivity
   have htarget (n : ℕ) :
@@ -983,7 +981,6 @@ private theorem exists_prescribed_radius_union_source_completed_tolerance
   let c : ℝ :=
     5 * (4 + ell *
       (216 / ((d : ℝ) * (1 - q) ^ 2) + 1 / (d : ℝ)))
-  have hdiff : 0 < 1 - q := sub_pos.mpr hq
   have hc : 0 < c := by
     dsimp [c]
     positivity
diff --git a/LeanPool/NonSoficGroup/Foundations.lean b/LeanPool/NonSoficGroup/Foundations.lean
index 09fe04ace8..bcb65f8f1e 100644
--- a/LeanPool/NonSoficGroup/Foundations.lean
+++ b/LeanPool/NonSoficGroup/Foundations.lean
@@ -27,8 +27,9 @@ import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
 import Mathlib.Order.CompletePartialOrder
 import Mathlib.RingTheory.TotallySplit
 import Mathlib.SetTheory.Cardinal.Free
--- Retain the finite-field and scalar tower instances used by the representation definitions.
-import Mathlib.Tactic.NormNum.LegendreSymbol -- shake: keep
+import Mathlib.FieldTheory.Finite.GaloisField
+-- Retain the freeness instance used by the existing finite-field basis type.
+import Mathlib.LinearAlgebra.FreeModule.PID -- shake: keep
 
 /-!
 # Foundations for the non-sofic group construction
@@ -117,7 +118,7 @@ public
 theorem normalizedHamming_nonneg {Y : Type*} [Fintype Y] [DecidableEq Y]
     (p q : Equiv.Perm Y) : 0 ≤ normalizedHamming p q := by
   unfold normalizedHamming
-  positivity
+  exact div_nonneg (Nat.cast_nonneg _) (Nat.cast_nonneg _)
 
 public
 theorem normalizedHamming_triangle {Y : Type*} [Fintype Y] [DecidableEq Y]
@@ -967,8 +968,6 @@ private theorem maximal_bad_cut_induced_lower {V ι : Type*}
     ell * (E.card : ℝ) ≤ (inducedBoundary σ B E : ℝ) := by
   classical
   by_contra h
-  have hE : (inducedBoundary σ B E : ℝ) < ell * (E.card : ℝ) :=
-    lt_of_not_ge h
   have hcut : (boundary σ (B ∪ E) : ℝ) ≤
       (boundary σ B : ℝ) + (inducedBoundary σ B E : ℝ) := by
     exact_mod_cast boundary_union_le σ B E
@@ -976,7 +975,7 @@ private theorem maximal_bad_cut_induced_lower {V ι : Type*}
     exact_mod_cast Finset.card_union_of_disjoint hdisj
   have hbad : (boundary σ (B ∪ E) : ℝ) < ell * ((B ∪ E).card : ℝ) := by
     rw [hcard]
-    nlinarith only [hB, h, hcut]
+    linarith only [hB, h, hcut]
   have hsize := hmax (B ∪ E) hhalf hbad
   have hepos : 0 < E.card := Finset.card_pos.mpr hne
   have hnat := Finset.card_union_of_disjoint hdisj
@@ -988,7 +987,7 @@ private theorem bad_cut_card_bound {γ ell a : ℝ} {N b q : ℕ}
     (hbad : (q : ℝ) ≤ ell * (b : ℝ)) :
     (b : ℝ) ≤ a * (N : ℝ) / (γ - ell) := by
   apply (le_div_iff₀ (sub_pos.mpr hgap)).2
-  nlinarith
+  linarith only [hadd, hbad]
 
 private theorem large_cut_lower {γ ell a d N b e q : ℝ}
     (hgap : ell < γ) (hd : 0 ≤ d) (hN : 0 ≤ N)
@@ -4146,8 +4145,6 @@ theorem componentVertexMidrank_le_one {V : Type*}
       exact_mod_cast hcard
     unfold componentVertexMidrank
     apply (div_le_one hc).2
-    have heq : 0 ≤ ((C.filter fun z => b z = b x).card : ℝ) := by
-      positivity
     linarith only [hcard']
 
 private theorem componentVertexMidrank_mono {V : Type*}
@@ -4182,13 +4179,13 @@ private theorem componentVertexMidrank_mono {V : Type*}
             ((C.filter fun z => b z = b x).card : ℝ) ≤
               ((C.filter fun z => b z < b y).card : ℝ) := by
         exact_mod_cast hcard
-      have hex : 0 ≤ ((C.filter fun z => b z = b x).card : ℝ) := by
-        positivity
-      have hey : 0 ≤ ((C.filter fun z => b z = b y).card : ℝ) := by
-        positivity
+      have hex : 0 ≤ ((C.filter fun z => b z = b x).card : ℝ) :=
+        Nat.cast_nonneg _
+      have hey : 0 ≤ ((C.filter fun z => b z = b y).card : ℝ) :=
+        Nat.cast_nonneg _
       unfold componentVertexMidrank
       apply (div_le_div_iff_of_pos_right hc).2
-      linarith
+      linarith only [hcard', hex, hey]
 
 /-- Internal interface connecting the split non-sofic proof modules. -/
 public
@@ -5545,7 +5542,6 @@ private theorem shifted_floor_drop_volume_bound_sharp
   let k : ℤ := ⌊u / H⌋
   let c : ℝ := (((k + 1 : ℤ) : ℝ) * H - u)
   let d : ℝ := u - v
-  have hd : 0 ≤ d := sub_nonneg.mpr hvu
   have hklo : (k : ℝ) ≤ u / H := by
     dsimp [k]
     exact Int.floor_le _
@@ -5554,10 +5550,6 @@ private theorem shifted_floor_drop_volume_bound_sharp
     exact Int.lt_floor_add_one _
   have hklo' : (k : ℝ) * H ≤ u := (le_div_iff₀ hH).mp hklo
   have hkhi' : u < ((k : ℝ) + 1) * H := (div_lt_iff₀ hH).mp hkhi
-  have hc0 : 0 ≤ c := by
-    dsimp [c]
-    push_cast
-    linarith only [hkhi']
   have hcH : c ≤ H := by
     dsimp [c]
     push_cast
@@ -5746,7 +5738,7 @@ private theorem abs_log_one_sub_le_two_mul
   have hlower := Real.one_sub_inv_le_log_of_pos hfactor
   have hratio : eta / (1 - eta) ≤ 2 * eta := by
     apply (div_le_iff₀ hfactor).2
-    nlinarith [mul_nonneg heta0 (by linarith : 0 ≤ 1 - 2 * eta)]
+    linarith only [heta0, hetaHalf, mul_nonneg heta0 (by linarith : 0 ≤ 1 - 2 * eta)]
   have hidentity : (1 - eta)⁻¹ - 1 = eta / (1 - eta) := by
     field_simp
     ring
@@ -7759,7 +7751,7 @@ private theorem partitionVertexMidrank_permutation_energy_le
         ((partitionWordCrossing P p).card : ℝ) +
           ((rankDecreasingVertices Finset.univ b p).card : ℝ) := by
     exact_mod_cast hcard
-  nlinarith only [hbase, hcast]
+  linarith only [hbase, hcast]
 
 private theorem sum_partitionVertexMidrank_permutation_energy_le
     {V ι : Type*} [Fintype V] [DecidableEq V]
@@ -8284,7 +8276,7 @@ private theorem almostCentralizerGap_of_expansion {V ι : Type*}
       mul_pos hpositive (sub_pos.mpr hlarge')
     change h * (permutationDistance p.permutation q.permutation : ℝ) ≤ _
       at hnear
-    nlinarith only [hsmall, hdef, hpos, hnear]
+    linarith only [hsmall, hdef, hpos, hnear]
   · right
     by_contra hnot
     have hlarge :
@@ -8300,7 +8292,7 @@ private theorem almostCentralizerGap_of_expansion {V ι : Type*}
       mul_nonneg hpositive.le (sub_nonneg.mpr hlarge')
     change h * ((Fintype.card V : ℝ) -
       permutationDistance p.permutation q.permutation) ≤ _ at hfar
-    nlinarith only [hsmall, hdef, hpos, hfar]
+    linarith only [hsmall, hdef, hpos, hfar]
 
 private def almostCentralizerSetoid {V ι : Type*}
     [Fintype V] [Fintype ι] [DecidableEq V]
@@ -8866,7 +8858,7 @@ private theorem exists_positive_antitone_slow_vanishing_threshold
       _ ≤ d n + q n := le_add_of_nonneg_right (hq_pos n).le
       _ = eta n * eta n := by
         dsimp [eta]
-        nlinarith [Real.sq_sqrt (add_nonneg (hd_nonneg n) (hq_pos n).le)]
+        linarith only [hd_nonneg, hq_pos, Real.sq_sqrt (add_nonneg (hd_nonneg n) (hq_pos n).le)]
   refine ⟨eta, heta_pos, heta_antitone, heta_zero, ?_⟩
   exact squeeze_zero (fun n => div_nonneg (he_nonneg n) (heta_pos n).le)
     hratio_bound heta_zero
@@ -8896,7 +8888,7 @@ theorem exists_positive_antitone_slow_overlap_scales
   have hquot (n : ℕ) : eta n / H n = H n := by
     dsimp [H]
     apply (div_eq_iff (Real.sqrt_pos.2 (heta_pos n)).ne').2
-    nlinarith only [heta_pos, Real.sq_sqrt (heta_pos n).le]
+    exact (Real.mul_self_sqrt (heta_pos n).le).symm
   have hquot_zero : Tendsto (fun n => eta n / H n) atTop (nhds 0) := by
     have hfun : (fun n => eta n / H n) = H := funext hquot
     rw [hfun]
diff --git a/LeanPool/NonSoficGroup/Spectral.lean b/LeanPool/NonSoficGroup/Spectral.lean
index 8ac1b31600..25cb3f12fd 100644
--- a/LeanPool/NonSoficGroup/Spectral.lean
+++ b/LeanPool/NonSoficGroup/Spectral.lean
@@ -312,7 +312,7 @@ private theorem ejThreeProjectionAverage_apply (x : H) :
 private theorem ejThreeResidualEnergy_nonneg (x : H) :
     0 ≤ ejThreeResidualEnergy V x := by
   unfold ejThreeResidualEnergy
-  positivity
+  exact add_nonneg (add_nonneg (sq_nonneg _) (sq_nonneg _)) (sq_nonneg _)
 
 private theorem ejThreeResidualEnergy_eq_re_inner (x : H) :
     ejThreeResidualEnergy V x =
@@ -1116,7 +1116,7 @@ private theorem hasPropertyT_of_geometric_finite_averaging
     rw [hone] at hdist
     have hden : 0 < 1 - q := sub_pos.mpr hq1
     have hlt : C / (1 - q) < 1 / 2 :=
-      (div_lt_iff₀ hden).mpr (by nlinarith only [hhalf])
+      (div_lt_iff₀ hden).mpr (by linarith only [hhalf])
     linarith only [hdist, hlt]
   exact ⟨η, hηne, hfixed η hηfixed⟩
 
@@ -1207,7 +1207,6 @@ private theorem norm_inner_le_inv_sqrt_eight_of_sq
     (h : 8 * ‖inner ℂ a b‖ ^ 2 ≤ ‖a‖ ^ 2 * ‖b‖ ^ 2) :
     ‖inner ℂ a b‖ ≤
       (Real.sqrt (8 : ℝ))⁻¹ * ‖a‖ * ‖b‖ := by
-  have hsqrt : 0 < Real.sqrt (8 : ℝ) := by positivity
   have hsquare : Real.sqrt (8 : ℝ) ^ 2 = 8 :=
     Real.sq_sqrt (by norm_num)
   have hsq :
@@ -1217,7 +1216,7 @@ private theorem norm_inner_le_inv_sqrt_eight_of_sq
       ‖inner ℂ a b‖ ^ 2 ≤
           (‖a‖ ^ 2 * ‖b‖ ^ 2) / 8 := by
             apply (le_div_iff₀ (show (0 : ℝ) < 8 by norm_num)).mpr
-            nlinarith only [h]
+            linarith only [h]
       _ = ((Real.sqrt (8 : ℝ))⁻¹ * ‖a‖ * ‖b‖) ^ 2 := by
         field_simp
         nlinarith only [h, hsquare]
@@ -2422,6 +2421,64 @@ private theorem inner_eq_zero_of_finite_subgroupAverage_pair_orthogonal
 
 end FiniteSubgroupAveraging
 
+/-- Keep projection algebra abstract before specializing to matrix root subgroups. -/
+private theorem fixed_submodule_inner_square_bound_of_central_sectors
+    {G H ι : Type*} [Group G] [NormedAddCommGroup H]
+    [InnerProductSpace ℂ H] [CompleteSpace H] [Finite ι]
+    (π : UnitaryRepresentation G H) (X Y : Subgroup G) (Z : ι → Subgroup G)
+    (hcentral : ∀ i (z : Z i) (g : (X ⊔ Y : Subgroup G)), Commute (z : G) (g : G))
+    (hcommute : ∀ i j (z : Z i) (w : Z j), Commute (z : G) (w : G))
+    (hsector : ∀ i (x y : H), x ∈ unitaryFixedSubmodule π X →
+      x ∈ (unitaryFixedSubmodule π (Z i))ᗮ → y ∈ unitaryFixedSubmodule π Y →
+      8 * ‖inner ℂ x y‖ ^ 2 ≤ ‖x‖ ^ 2 * ‖y‖ ^ 2)
+    (hterminal : ∀ (x y : H),
+      x ∈ unitaryFixedSubmodule π X ⊓
+        (unitaryFixedSubmodule π X ⊓ unitaryFixedSubmodule π Y)ᗮ →
+      y ∈ unitaryFixedSubmodule π Y ⊓
+        (unitaryFixedSubmodule π X ⊓ unitaryFixedSubmodule π Y)ᗮ →
+      (∀ i, x ∈ unitaryFixedSubmodule π (Z i)) →
+      (∀ i, y ∈ unitaryFixedSubmodule π (Z i)) → inner ℂ x y = 0)
+    {a b : H} (ha : a ∈ unitaryFixedSubmodule π X)
+    (hb : b ∈ unitaryFixedSubmodule π Y)
+    (haQ : a ∈ (unitaryFixedSubmodule π X ⊓ unitaryFixedSubmodule π Y)ᗮ)
+    (hbQ : b ∈ (unitaryFixedSubmodule π X ⊓ unitaryFixedSubmodule π Y)ᗮ) :
+    8 * ‖inner ℂ a b‖ ^ 2 ≤ ‖a‖ ^ 2 * ‖b‖ ^ 2 := by
+  classical
+  let Q := unitaryFixedSubmodule π X ⊓ unitaryFixedSubmodule π Y
+  let U := unitaryFixedSubmodule π X ⊓ Qᗮ
+  let V := unitaryFixedSubmodule π Y ⊓ Qᗮ
+  let F (i : ι) := unitaryFixedSubmodule π (Z i)
+  let (i : ι) : CompleteSpace (F i) := unitaryFixedSubmodule_completeSpace π (Z i)
+  refine inner_sq_le_of_finite_orthogonal_sector_splitting
+    F U V ?_ ?_ ?_ ?_ hterminal a b ⟨ha, haQ⟩ ⟨hb, hbQ⟩
+  · intro i x hx
+    refine ⟨?_, ?_⟩
+    · exact unitaryFixedSubmodule_starProjection_mem_of_commute π (Z i) X
+        (fun z g => hcentral i z ⟨g.val, Subgroup.mem_sup_left g.property⟩) hx.1
+    · have hq : x ∈ (unitaryFixedSubmodule π (X ⊔ Y))ᗮ := by
+        rw [unitaryFixedSubmodule_sup]
+        exact hx.2
+      have hp := unitaryFixedSubmodule_starProjection_mem_orthogonal_of_commute
+        π (Z i) (X ⊔ Y) (hcentral i) hq
+      rw [unitaryFixedSubmodule_sup] at hp
+      exact hp
+  · intro i x hx
+    refine ⟨?_, ?_⟩
+    · exact unitaryFixedSubmodule_starProjection_mem_of_commute π (Z i) Y
+        (fun z g => hcentral i z ⟨g.val, Subgroup.mem_sup_right g.property⟩) hx.1
+    · have hq : x ∈ (unitaryFixedSubmodule π (X ⊔ Y))ᗮ := by
+        rw [unitaryFixedSubmodule_sup]
+        exact hx.2
+      have hp := unitaryFixedSubmodule_starProjection_mem_orthogonal_of_commute
+        π (Z i) (X ⊔ Y) (hcentral i) hq
+      rw [unitaryFixedSubmodule_sup] at hp
+      exact hp
+  · intro i j x hx
+    exact unitaryFixedSubmodule_starProjection_mem_of_commute
+      π (Z i) (Z j) (hcommute i j) hx
+  · intro i x y hx hy hxZ _
+    exact hsector i x y hx.1 hxZ hy.1
+
 private theorem finiteOuterBlockRootSubgroups_pair_inner_sq_le
     {R : Type*} [Ring R] [Algebra (ZMod 2) R]
     {H : Type v₁} [NormedAddCommGroup H]
@@ -2455,14 +2512,7 @@ private theorem finiteOuterBlockRootSubgroups_pair_inner_sq_le
     finiteOuterBlockProductCentralRootSubgroup W i k hik B
   let Q : Submodule ℂ H :=
     unitaryFixedSubmodule π X ⊓ unitaryFixedSubmodule π Y
-  let U : Submodule ℂ H := unitaryFixedSubmodule π X ⊓ Qᗮ
-  let V : Submodule ℂ H := unitaryFixedSubmodule π Y ⊓ Qᗮ
-  let F (B : Matrix (Fin 3) (Fin 3) W) :=
-    unitaryFixedSubmodule π (Z B)
   let : Finite X := finite_finiteOuterBlockRootSubgroup W i j hij
-  let : Fintype X := Fintype.ofFinite X
-  let (B : Matrix (Fin 3) (Fin 3) W) : CompleteSpace (F B) :=
-    unitaryFixedSubmodule_completeSpace π (Z B)
   have hpairCentral (B : Matrix (Fin 3) (Fin 3) W) :
       ∀ z : Z B, ∀ g :
         (X ⊔ Y : Subgroup
@@ -2479,53 +2529,13 @@ private theorem finiteOuterBlockRootSubgroups_pair_inner_sq_le
       (g : elementaryGroup (Fin 3) (Matrix (Fin 3) (Fin 3) R)) *
       (z : elementaryGroup (Fin 3) (Matrix (Fin 3) (Fin 3) R))
     exact hg z z.property
-  refine inner_sq_le_of_finite_orthogonal_sector_splitting
-    F U V ?_ ?_ ?_ ?_ ?_ a b ⟨ha, haQ⟩ ⟨hb, hbQ⟩
-  · intro B x hx
-    change (unitaryFixedSubmodule π (Z B)).starProjection x ∈
-      unitaryFixedSubmodule π X ⊓ Qᗮ
-    refine ⟨?_, ?_⟩
-    · exact unitaryFixedSubmodule_starProjection_mem_of_commute
-        π (Z B) X
-        (fun z x =>
-          (finiteOuterBlockProductCentralRoot_commute_left
-            W i j k hij hik B x z x.property z.property).symm)
-        hx.1
-    · have hq : x ∈ (unitaryFixedSubmodule π (X ⊔ Y))ᗮ := by
-        rw [unitaryFixedSubmodule_sup]
-        exact hx.2
-      have hp := unitaryFixedSubmodule_starProjection_mem_orthogonal_of_commute
-        π (Z B) (X ⊔ Y) (hpairCentral B) hq
-      rw [unitaryFixedSubmodule_sup] at hp
-      exact hp
-  · intro B x hx
-    change (unitaryFixedSubmodule π (Z B)).starProjection x ∈
-      unitaryFixedSubmodule π Y ⊓ Qᗮ
-    refine ⟨?_, ?_⟩
-    · exact unitaryFixedSubmodule_starProjection_mem_of_commute
-        π (Z B) Y
-        (fun z y =>
-          (finiteOuterBlockProductCentralRoot_commute_right
-            W i j k hjk hik B y z y.property z.property).symm)
-        hx.1
-    · have hq : x ∈ (unitaryFixedSubmodule π (X ⊔ Y))ᗮ := by
-        rw [unitaryFixedSubmodule_sup]
-        exact hx.2
-      have hp := unitaryFixedSubmodule_starProjection_mem_orthogonal_of_commute
-        π (Z B) (X ⊔ Y) (hpairCentral B) hq
-      rw [unitaryFixedSubmodule_sup] at hp
-      exact hp
-  · intro B C x hx
-    change (unitaryFixedSubmodule π (Z B)).starProjection x ∈
-      unitaryFixedSubmodule π (Z C)
-    exact unitaryFixedSubmodule_starProjection_mem_of_commute
-      π (Z B) (Z C)
-      (fun z w => finiteOuterBlockProductCentralRoots_commute
-        W i k hik B C z w z.property w.property)
-      hx
-  · intro B x y hx hy hxZ _
-    exact finiteOuterBlockProductCentral_centerComplement_inner_sq_le
-      W i j k hij hjk hik B π hx.1 hxZ hy.1
+  refine fixed_submodule_inner_square_bound_of_central_sectors π X Y Z
+    hpairCentral
+    (fun B C z w => finiteOuterBlockProductCentralRoots_commute
+      W i k hik B C z w z.property w.property)
+    (fun B x y hx hxZ hy => finiteOuterBlockProductCentral_centerComplement_inner_sq_le
+      W i j k hij hjk hik B π hx hxZ hy)
+    ?_ ha hb haQ hbQ
   · intro x y hx hy _ hyF
     apply inner_eq_zero_of_finite_subgroupAverage_pair_orthogonal
       π X Y x y
@@ -4522,7 +4532,7 @@ private theorem exists_boundary_controlled_permutation_repair
             ((U \ matchedFiberEdges U).card : ℝ)) ≤
         8 * (boundary
           (fun i => (σ i).prodCongr (σ i)) U : ℝ) := by
-    nlinarith only [hvertex, hrelation]
+    linarith only [hvertex, hrelation]
   have hdnonneg : (0 : ℝ) ≤ Fintype.card ι := by
     positivity
   have hscaled := mul_le_mul_of_nonneg_left hsum hdnonneg
@@ -4539,7 +4549,7 @@ private theorem exists_boundary_controlled_permutation_repair
     _ ≤ (h + 8 * (Fintype.card ι : ℝ)) *
           (boundary
             (fun i => (σ i).prodCongr (σ i)) U : ℝ) := by
-      nlinarith only [hscaled]
+      linarith only [hscaled]
 
 private theorem permutationDistance_eq_card_permutationGraph_sdiff
     {V : Type*} [Fintype V] [DecidableEq V]
@@ -4642,7 +4652,7 @@ private theorem exists_boundary_controlled_permutation_repair_close_to_reference
     σ U h hpositive hexp hfirst hsecond
   refine ⟨q, ?_, hdefect⟩
   have hscaled := mul_le_mul_of_nonneg_left hdistance_real hpositive.le
-  nlinarith only [hvertex, hscaled]
+  linarith only [hvertex, hscaled]
 
 private theorem hasAlmostCentralizerImprovement_of_expanding_diagonal_cuts
     {V ι : Type*} [Fintype V] [Fintype ι] [DecidableEq V]
@@ -4682,8 +4692,6 @@ private theorem hasAlmostCentralizerImprovement_of_expanding_diagonal_cuts
   have hdefect :
       permutationCommutationDefect σ q ≤ tolerance := by
     exact_mod_cast hdefect_real
-  have hscaled := mul_le_mul_of_nonneg_left hqdistance
-    (show (0 : ℝ) ≤ 5 by norm_num)
   have hdistance_real :
       (5 : ℝ) * (permutationDistance q p : ℝ) ≤
         (Fintype.card V : ℝ) := by
@@ -8902,7 +8910,7 @@ private theorem exists_expanding_full_finpartition
             add_le_add hQbudget hbad
       _ ≤ 2 * (Fintype.card ι : ℝ) * (B.card : ℝ) +
           4 * α * (Fintype.card V : ℝ) := by
-            nlinarith only [hscaled]
+            linarith only [hscaled]
 
 public
 theorem exists_expanding_full_finpartition_sequence
@@ -9672,8 +9680,6 @@ theorem completedRestriction_mul_of_not_mem_sourceCompletionBad
     completedRestriction (p (j * k)) Z z =
       (completedRestriction (p j) Z * completedRestriction (p k) Z) z := by
   have hg := sourceCompletionBad_good σ p F Z z z.property hz
-  have hjT :=
-    CompressionCriterion.mem_productTrackedTable hj
   have hkT :=
     CompressionCriterion.mem_productTrackedTable hk
   have hjkT :=