refactor(exact-triangle): move reusable bounds and clarify finite APIs

Complexity.lean

@@ -31,9 +31,18 @@ public import Complexity.Algorithms.Lean.VanEmdeBoas.Insert
 public import Complexity.Algorithms.Lean.VanEmdeBoas.Layout
 public import Complexity.Algorithms.Lean.VanEmdeBoas.Successor
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Alphabets
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Batch
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Full
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Identity
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Layout
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Levels
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Magnitude
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Orders
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Parameters
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Pruned
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Sparse
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.ThinProduct
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Tiling
 public import Complexity.Algorithms.Reachability.BreadthFirst
 public import Complexity.Algorithms.Reachability.InductiveCounting
 public import Complexity.Algorithms.Reachability.InductiveCounting.Bounds
@@ -1930,6 +1939,8 @@ public import Complexity.Crypto.Protocols.SigmaProtocol.Lyubashevsky.NativeExtra
 public import Complexity.Crypto.Protocols.SigmaProtocol.SchnorrIdentification
 public import Complexity.Crypto.Protocols.SigmaProtocol.SchnorrSignature
 public import Complexity.Crypto.Protocols.Signature.RandomOracle
+public import Complexity.Foundations.Algebra.FiniteMagnitude
+public import Complexity.Foundations.Algebra.GeometricTail
 public import Complexity.Foundations.Analysis.BernoulliInequality
 public import Complexity.Foundations.Analysis.HarmonicMean
 public import Complexity.Foundations.Analysis.InnerProductSpace.Basic
@@ -2034,6 +2045,7 @@ public import Complexity.Foundations.Combinatorics.Expander.Walk
 public import Complexity.Foundations.Combinatorics.Expander.Zigzag
 public import Complexity.Foundations.Combinatorics.FiniteCover
 public import Complexity.Foundations.Combinatorics.FiniteCover.Basic
+public import Complexity.Foundations.Combinatorics.FunctionPlaces
 public import Complexity.Foundations.Combinatorics.FunctionalGraph
 public import Complexity.Foundations.Combinatorics.FunctionalGraph.Active
 public import Complexity.Foundations.Combinatorics.FunctionalGraph.CheckpointForest
@@ -2145,13 +2157,15 @@ public import Complexity.Foundations.Data.Finset.Average
 public import Complexity.Foundations.Data.Finset.Expect
 public import Complexity.Foundations.Data.Finset.Finpartition
 public import Complexity.Foundations.Data.Finset.Markov
+public import Complexity.Foundations.Data.Finset.OrderGlue
 public import Complexity.Foundations.Data.Finset.Quantile
 public import Complexity.Foundations.Data.Finset.Quotient
 public import Complexity.Foundations.Data.Finset.Sampling
 public import Complexity.Foundations.Data.Finset.SubsetSum
 public import Complexity.Foundations.Data.Finset.SymmDiff
 public import Complexity.Foundations.Data.Hamming
 public import Complexity.Foundations.Data.Hamming.Expansion
+public import Complexity.Foundations.Data.Int.LogBounds
 public import Complexity.Foundations.Data.Int.Order
 public import Complexity.Foundations.Data.Int.Residue
 public import Complexity.Foundations.Data.List.Append
@@ -2284,6 +2298,7 @@ public import Complexity.Foundations.NumberTheory.AKS.SmallR
 public import Complexity.Foundations.NumberTheory.Harmonic
 public import Complexity.Foundations.NumberTheory.PrimeCounting
 public import Complexity.Foundations.NumberTheory.PrimeWindow
+public import Complexity.Foundations.NumberTheory.SqrtPrimeWindow
 public import Complexity.Foundations.Order.BooleanSubalgebra
 public import Complexity.Foundations.Order.Changes
 public import Complexity.Foundations.Order.UpperLower

Complexity/Algorithms/ExactTriangle/Lopsided.lean

@@ -31,11 +31,12 @@ fast solver or subquadratic running time.
 
 * `LopsidedGraph.matX_mul_matY_apply`: entries count common middle neighbors.
 * `LopsidedGraph.matX_mul_matY_apply_ne_zero_iff`: nonzero entries detect common neighbors.
-* `LopsidedGraph.zero_one`: the converse for zero/one matrices.
-* `LopsidedGraph.entries_from_counts`: bounded signed products from `4 * β²` counts.
+* `LopsidedGraph.mul_apply_eq_commonNeighborCount_ofMatrices`: the converse for zero/one matrices.
+* `LopsidedGraph.mul_apply_eq_sum_signedBitInstance_counts`: signed products from `4 * β²` counts.
 
 ## References
 
+The lopsided matrix interface is used in [AlmanWilliams2026, Section 3].
 Adapted from [Anthropic's MatrixLanguage.lean](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Sec3/MatrixLanguage.lean)
 and the lopsided definitions in [PaperStatements.lean](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/PaperStatements.lean#L798-L852).
 The adaptation uses `Set.EqOn`, pointwise signed parts, and direct finite cardinalities.
@@ -73,7 +74,7 @@ noncomputable def commonNeighborCount {n : ℕ} (I : LopsidedGraph n) (a b : Fin
   (Finset.univ.filter fun v : I.M => I.adjA a v ∧ I.adjB v b).card
 
 /-- Two thin matrices describe adjacency where their entries equal one.
-The counting theorem `zero_one` requires all entries to be zero or one. -/
+The theorem `mul_apply_eq_commonNeighborCount_ofMatrices` requires zero/one entries. -/
 def ofMatrices {n D : ℕ} (X : Matrix (Fin n) (Fin D) ℤ)
     (Y : Matrix (Fin D) (Fin n) ℤ) (W : Finset (Fin n × Fin n)) : LopsidedGraph n where
   M := Fin D
@@ -180,16 +181,15 @@ theorem counting_eqOn_iff (ans : Fin n × Fin n → ℕ) :
   simp only [Set.EqOn, matX_mul_matY_apply, Nat.cast_inj]
 
 /-- Counts on queried edges provide their detection answers. -/
-theorem detection_eqOn_of_counting (ans : Fin n × Fin n → ℕ)
+theorem detection_iff_of_counting (ans : Fin n × Fin n → ℕ)
     (h : Set.EqOn ans (fun q => I.commonNeighborCount q.1 q.2) (I.W : Set _)) :
-    Set.EqOn (fun q => ans q ≠ 0) (fun q => I.HasCommonNeighbor q.1 q.2) (I.W : Set _) := by
+    ∀ q ∈ I.W, ans q ≠ 0 ↔ I.HasCommonNeighbor q.1 q.2 := by
   intro q hq
-  change (ans q ≠ 0) = I.HasCommonNeighbor q.1 q.2
-  apply propext
   rw [h hq, commonNeighborCount_ne_zero_iff]
 
 /-- For zero/one matrices, each product entry is the count in the graph they describe. -/
-theorem zero_one {n D : ℕ} (X : Matrix (Fin n) (Fin D) ℤ) (Y : Matrix (Fin D) (Fin n) ℤ)
+theorem mul_apply_eq_commonNeighborCount_ofMatrices {n D : ℕ}
+    (X : Matrix (Fin n) (Fin D) ℤ) (Y : Matrix (Fin D) (Fin n) ℤ)
     (W : Finset (Fin n × Fin n)) (hX : ∀ a j, X a j = 0 ∨ X a j = 1)
     (hY : ∀ j b, Y j b = 0 ∨ Y j b = 1) (a b : Fin n) :
     (X * Y) a b = ((ofMatrices X Y W).commonNeighborCount a b : ℤ) := by
@@ -203,8 +203,8 @@ theorem zero_one {n D : ℕ} (X : Matrix (Fin n) (Fin D) ℤ) (Y : Matrix (Fin D
 Every instance has exactly `D` middle vertices and the original queried edges `W`. -/
 def signedBitInstance (X : Matrix (Fin n) (Fin D) ℤ) (Y : Matrix (Fin D) (Fin n) ℤ)
     (W : Finset (Fin n × Fin n)) (negativeX negativeY : Bool) (i j : ℕ) : LopsidedGraph n :=
-  ofMatrices (IntMatrix.bit (if negativeX then (X.map negPart) else (X.map posPart)) i)
-    (IntMatrix.bit (if negativeY then (Y.map negPart) else (Y.map posPart)) j) W
+  ofMatrices (Matrix.bit (if negativeX then (X.map negPart) else (X.map posPart)) i)
+    (Matrix.bit (if negativeY then (Y.map negPart) else (Y.map posPart)) j) W
 
 /-- The finite family of sign/digit instances for a magnitude width `β`.
 Different slots may describe the same graph. -/
@@ -223,18 +223,19 @@ private theorem mul_apply_eq_sum_counts {n D : ℕ} (X : Matrix (Fin n) (Fin D)
     (Y : Matrix (Fin D) (Fin n) ℤ) (W : Finset (Fin n × Fin n)) (β : ℕ)
     (hX : ∀ a j, 0 ≤ X a j ∧ X a j < 2 ^ β) (hY : ∀ j b, 0 ≤ Y j b ∧ Y j b < 2 ^ β) (a b : Fin n) :
     (X * Y) a b = ∑ i ∈ Finset.range β, ∑ j ∈ Finset.range β, (2 : ℤ) ^ (i + j) *
-      ((ofMatrices (IntMatrix.bit X i) (IntMatrix.bit Y j) W).commonNeighborCount a b : ℤ) := by
-  rw [IntMatrix.product X Y β hX hY, Matrix.sum_apply]
+      ((ofMatrices (Matrix.bit X i) (Matrix.bit Y j) W).commonNeighborCount a b : ℤ) := by
+  rw [Matrix.mul_eq_sum_two_pow_smul_bit_mul_bit X Y β hX hY, Matrix.sum_apply]
   refine Finset.sum_congr rfl fun i _ => ?_
   rw [Matrix.sum_apply]
   refine Finset.sum_congr rfl fun j _ => ?_
-  rw [Matrix.smul_apply, smul_eq_mul, zero_one _ _ W (IntMatrix.bit_eq_zero_or_one X i)
-    (IntMatrix.bit_eq_zero_or_one Y j)]
+  rw [Matrix.smul_apply, smul_eq_mul, mul_apply_eq_commonNeighborCount_ofMatrices _ _ W
+    (Matrix.bit_eq_zero_or_one X i)
+    (Matrix.bit_eq_zero_or_one Y j)]
 
 /-- Signed bounded product entries are weighted sums of four count instances per digit
 pair, with signs `+, −, −, +`. Only counts at the same queried edge are needed. The absolute
 bounds are strict; `β = 0` therefore permits only zero entries. -/
-theorem entries_from_counts {n D : ℕ} (X : Matrix (Fin n) (Fin D) ℤ)
+theorem mul_apply_eq_sum_signedBitInstance_counts {n D : ℕ} (X : Matrix (Fin n) (Fin D) ℤ)
     (Y : Matrix (Fin D) (Fin n) ℤ) (W : Finset (Fin n × Fin n)) (β : ℕ)
     (hX : ∀ a j, |X a j| < 2 ^ β) (hY : ∀ j b, |Y j b| < 2 ^ β) (a b : Fin n) :
     (X * Y) a b = ∑ i ∈ Finset.range β, ∑ j ∈ Finset.range β, (2 : ℤ) ^ (i + j) *
@@ -247,10 +248,10 @@ theorem entries_from_counts {n D : ℕ} (X : Matrix (Fin n) (Fin D) ℤ)
         + ((signedBitInstance X Y W true true i j).commonNeighborCount
             a b : ℤ)) := by
   simp only [signedBitInstance, Bool.false_eq_true, ↓reduceIte]
-  obtain ⟨hXpos, hXneg⟩ := IntMatrix.parts_lt X hX
-  obtain ⟨hYpos, hYneg⟩ := IntMatrix.parts_lt Y hY
+  obtain ⟨hXpos, hXneg⟩ := Matrix.map_posPart_lt_and_map_negPart_lt X hX
+  obtain ⟨hYpos, hYneg⟩ := Matrix.map_posPart_lt_and_map_negPart_lt Y hY
   -- `XY` is a signed sum of the four products of a part of `X` and a part of `Y`.
-  conv_lhs => rw [IntMatrix.parts X, IntMatrix.parts Y]
+  conv_lhs => rw [Matrix.eq_map_posPart_sub_map_negPart X, Matrix.eq_map_posPart_sub_map_negPart Y]
   rw [Matrix.sub_mul, Matrix.mul_sub, Matrix.mul_sub]
   simp only [Matrix.sub_apply]
   rw [mul_apply_eq_sum_counts _ _ W β hXpos hYpos,

Complexity/Algorithms/ExactTriangle/Splitting.lean

@@ -131,23 +131,15 @@ def totalChunks {n : ℕ} (wAB : Fin n → Fin n → ℤ) (D p : ℕ) : ℕ :=
 
 variable {n : ℕ}
 
-/-- `√D ≤ D ≤ n`. -/
-theorem sqrt_le_natCast {D : ℕ} (hD : 1 ≤ D) (hDn : D ≤ n) : Real.sqrt D ≤ n :=
-  calc Real.sqrt D ≤ Real.sqrt D * Real.sqrt D :=
-        le_mul_of_one_le_left (Real.sqrt_nonneg _) (Real.one_le_sqrt.mpr (by exact_mod_cast hD))
-    _ = D := Real.mul_self_sqrt (Nat.cast_nonneg D)
-    _ ≤ n := by exact_mod_cast hDn
-
 /-- The bound `⌊n²/√D⌋` on the size of a chunk is at least 1, because `√D ≤ n ≤ n²`. -/
 theorem one_le_queryCap {D : ℕ} (hD : 1 ≤ D) (hDn : D ≤ n) : 1 ≤ queryCap n D := by
   rw [queryCap_eq_floor]
   have hn : (1 : ℝ) ≤ n := by exact_mod_cast hD.trans hDn
   refine Nat.le_floor ?_
   rw [Nat.cast_one, le_div_iff₀ (Real.sqrt_pos.mpr (by exact_mod_cast hD)), one_mul]
-  exact (sqrt_le_natCast hD hDn).trans (le_self_pow₀ hn two_ne_zero)
-
-private theorem four_le_sqrt {D : ℕ} (hD : 16 ≤ D) : 4 ≤ Real.sqrt (D : ℝ) :=
-  Real.le_sqrt_of_sq_le (by norm_num; exact_mod_cast hD)
+  have hsqrt : Real.sqrt (D : ℝ) ≤ D :=
+    Real.sqrt_le_self_iff.mpr (Or.inr (by exact_mod_cast hD))
+  exact (hsqrt.trans (by exact_mod_cast hDn)).trans (le_self_pow₀ hn two_ne_zero)
 
 variable {n D g p : ℕ}
 
@@ -163,7 +155,7 @@ theorem sqrt_lt_sOf_add_one (D : ℕ) : Real.sqrt D < (sOf D : ℝ) + 1 :=
 
 /-- `s > 0` because `D ≥ 16`. -/
 private theorem sOf_pos (hD : 16 ≤ D) : (0 : ℝ) < sOf D := by
-  linarith [four_le_sqrt hD, sqrt_lt_sOf_add_one D]
+  linarith [Real.four_le_sqrt_natCast hD, sqrt_lt_sOf_add_one D]
 
 /-- The bound `⌈s/g⌉` on the size of a piece is at least 1. -/
 theorem pieceSize_pos (hD : 16 ≤ D) (hg1 : 1 ≤ g) : 0 < pieceSize D g := by
@@ -270,7 +262,7 @@ private theorem sq_lt_mul_queryCap_add (hD : 16 ≤ D) (hDn : D ≤ n)
   set r := Real.sqrt D with hr
   set δ := (sOf D : ℝ) + 1 - r with hδ
   set x := (n : ℝ) ^ 2 / r with hx
-  have hr4 : 4 ≤ r := four_le_sqrt hD
+  have hr4 : 4 ≤ r := Real.four_le_sqrt_natCast hD
   have hxr : x * r = (n : ℝ) ^ 2 := div_mul_cancel₀ _ (by linarith)
   have hx3 : r ^ 3 ≤ x := by
     rw [hx, le_div_iff₀ (by linarith)]
@@ -304,8 +296,8 @@ private theorem sq_lt_mul_queryCap_add (hD : 16 ≤ D) (hDn : D ≤ n)
 because D ≥ 16, and √D ≤ √n ≤ 2n/3 because D ≤ n and we may assume n ≥ 3". -/
 theorem le_sOf_and_sqrt_le (hD : 16 ≤ D) (hDn : D ≤ n) :
     3 * Real.sqrt D / 4 ≤ (sOf D : ℝ) ∧ Real.sqrt D ≤ 2 * (n : ℝ) / 3 := by
-  have hsqrtD := four_le_sqrt hD
-  have hsqrtn := four_le_sqrt (hD.trans hDn)
+  have hsqrtD := Real.four_le_sqrt_natCast hD
+  have hsqrtn := Real.four_le_sqrt_natCast (hD.trans hDn)
   constructor
   · calc 3 * Real.sqrt D / 4 ≤ Real.sqrt D - 1 := by linarith
       _ ≤ (sOf D : ℝ) := by linarith [sqrt_lt_sOf_add_one D]
@@ -385,10 +377,10 @@ private theorem totalChunks_le_add_sOf (hD : 16 ≤ D) (hDn : D ≤ n) (hp0 : p
 NOTE.  A chunk holds a whole number of pairs, at most `⌊n²/√D⌋`, so the count is at most
 `p + (n² − p)/⌊n²/√D⌋`, and the second term can exceed `√D` slightly.  The printed bound is still
 true, because the count is an integer, `D` is an integer and `D ≤ n` (`sq_lt_mul_queryCap_add`). -/
-theorem totalChunks_le (hD : 16 ≤ D) (hDn : D ≤ n) (hp : p ∈ primesInRange D) :
+theorem totalChunks_le (hD : 16 ≤ D) (hDn : D ≤ n) (hp : p ∈ Nat.sqrtPrimeWindow D) :
     (totalChunks wAB D p : ℝ) ≤ (p : ℝ) + Real.sqrt D ∧
     (p : ℝ) + Real.sqrt D ≤ 2 * Real.sqrt D := by
-  obtain ⟨hprime, hge, hlt⟩ := mem_primesInRange.mp hp
+  obtain ⟨hprime, hge, hlt⟩ := Nat.mem_sqrtPrimeWindow.mp hp
   have hnat : (totalChunks wAB D p : ℝ) ≤ (p : ℝ) + (sOf D : ℝ) := by
     exact_mod_cast totalChunks_le_add_sOf wAB hD hDn hprime.ne_zero hge
   exact ⟨by linarith [sOf_le_sqrt D], by linarith⟩
@@ -397,9 +389,9 @@ theorem totalChunks_le (hD : 16 ≤ D) (hDn : D ≤ n) (hp : p ∈ primesInRange
 
 /-- Proof of Theorem 17: "middle part C_k × ℤ_p, of size at most sp ≤ D".  So each instance is an
 instance of Lop-AE-SparseTri(n, D). -/
-theorem card_middle_lopInstance (hD : 16 ≤ D) (hg1 : 1 ≤ g) (hp : p ∈ primesInRange D)
+theorem card_middle_lopInstance (hD : 16 ≤ D) (hg1 : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow D)
     (ι : InstanceIndex p) : Fintype.card (lopInstance wAB wBC wAC D g p ι).M ≤ D := by
-  obtain ⟨-, -, hlt⟩ := mem_primesInRange.mp hp
+  obtain ⟨-, -, hlt⟩ := Nat.mem_sqrtPrimeWindow.mp hp
   have hsp : (sOf D : ℝ) * (p : ℝ) ≤ D :=
     calc (sOf D : ℝ) * (p : ℝ) ≤ Real.sqrt D * Real.sqrt D :=
           mul_le_mul (sOf_le_sqrt D) hlt.le (Nat.cast_nonneg p) (Real.sqrt_nonneg _)
@@ -475,7 +467,7 @@ theorem card_instanceIndices (D g p : ℕ) :
 
 /-- Proof of Theorem 17: "There are at most 2√D h ≤ 2√D(ng/s + 1) ≤ 4ng instances". -/
 theorem card_instanceIndices_le (hD : 16 ≤ D) (hDn : D ≤ n) (hg1 : 1 ≤ g)
-    (hp : p ∈ primesInRange D) :
+    (hp : p ∈ Nat.sqrtPrimeWindow D) :
     ((instanceIndices wAB D g p).card : ℝ) ≤ 4 * (n : ℝ) * (g : ℝ) := by
   obtain ⟨hs, hsqrt⟩ := le_sOf_and_sqrt_le hD hDn
   obtain ⟨hchunks, hchunks'⟩ := totalChunks_le wAB hD hDn hp