feat(exactTriangle): prove modular counts and selected-prime bounds

Complexity.lean

@@ -1,7 +1,9 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
 public import Complexity.Algorithms.ExactTriangle.Defs
+public import Complexity.Algorithms.ExactTriangle.Hashing
 public import Complexity.Algorithms.ExactTriangle.Lopsided
+public import Complexity.Algorithms.ExactTriangle.Weights
 public import Complexity.Algorithms.Lean.FusionTree.Capacity
 public import Complexity.Algorithms.Lean.FusionTree.Compression
 public import Complexity.Algorithms.Lean.FusionTree.Correction
@@ -2203,6 +2205,7 @@ public import Complexity.Foundations.NumberTheory.AKS.Introspective
 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.Order.BooleanSubalgebra
 public import Complexity.Foundations.Order.Changes
 public import Complexity.Foundations.Order.UpperLower
@@ -2213,6 +2216,7 @@ public import Complexity.Foundations.Probability.SecondMoment
 public import Complexity.Foundations.Quantum.Measurement
 public import Complexity.Foundations.Relation.InductiveCounting
 public import Complexity.Foundations.Relation.RelatesWithinSteps
+public import Complexity.Foundations.RingTheory.CyclicIntRing
 public import Complexity.Foundations.Semantics.Stateful.Amortized
 public import Complexity.Foundations.Semantics.Stateful.Basic
 public import Complexity.Foundations.Semantics.Stateful.Composition

Complexity/Algorithms/ExactTriangle/Weights.lean

@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2026 Anthropic, PBC, Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anthropic, PBC, Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.ExactTriangle.Defs
+public import Mathlib.Algebra.Order.Group.Abs
+public import Mathlib.Basic.Real.Basic
+import Mathlib.Tactic.Linarith
+
+/-!
+# Integer triangle sums and magnitude bounds
+
+## Main definitions
+
+* `weightSum`: the sum of the three supplied integer edge weights.
+* `WeightsBoundedBy`: a shared real bound on their absolute values.
+
+## Main results
+
+* `abs_weightSum_le`: a triangle's magnitude is at most three times the edge bound.
+
+## References
+
+Adapted from the weight sum and bound definitions in [Anthropic's
+PaperStatements.lean](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/PaperStatements.lean#L893-L914)
+and the triangle inequality in its
+[Hashing.lean](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Sec3/Theorem17/Hashing.lean#L246-L255).
+The existing `HasZeroTriangle` remains the decision predicate.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.ExactTriangle
+
+variable {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ)
+
+/-- Sum of the A–B, B–C and A–C weights at a triangle. -/
+def weightSum (a b c : Fin n) : ℤ := wAB a b + wBC b c + wAC a c
+
+/-- Every supplied edge weight has absolute value at most `U`. -/
+def WeightsBoundedBy (U : ℝ) : Prop :=
+  (∀ a b, ((|wAB a b| : ℤ) : ℝ) ≤ U) ∧
+  (∀ b c, ((|wBC b c| : ℤ) : ℝ) ≤ U) ∧ ∀ a c, ((|wAC a c| : ℤ) : ℝ) ≤ U
+
+/-- The three edge bounds imply a threefold bound on every triangle sum. -/
+theorem abs_weightSum_le {U : ℝ} (h : WeightsBoundedBy wAB wBC wAC U) (a b c : Fin n) :
+    ((|weightSum wAB wBC wAC a b c| : ℤ) : ℝ) ≤ 3 * U := by
+  obtain ⟨hAB, hBC, hAC⟩ := h
+  have habs : |weightSum wAB wBC wAC a b c| ≤ |wAB a b| + |wBC b c| + |wAC a c| :=
+    abs_add_three _ _ _
+  have hcast : ((|weightSum wAB wBC wAC a b c| : ℤ) : ℝ) ≤
+      ((|wAB a b| : ℤ) : ℝ) + ((|wBC b c| : ℤ) : ℝ) + ((|wAC a c| : ℤ) : ℝ) := by
+    exact_mod_cast habs
+  linarith [hAB a b, hBC b c, hAC a c]
+
+end Cslib.Algorithms.ExactTriangle

Complexity/Foundations/RingTheory/CyclicIntRing.lean

@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2026 Anthropic, PBC, Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anthropic, PBC, Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Init
+public import Mathlib.RingTheory.AdjoinRoot
+
+/-!
+# Integer polynomials modulo `X^p - 1`
+
+## Main definitions
+
+* `CyclicIntRing`: the integer polynomial quotient.
+* `CyclicIntRing.coeff`: coefficients in the unique representative of degree less than `p`.
+
+## Main results
+
+* `CyclicIntRing.coeff_x_pow`: powers have a single coefficient at the residue of their
+  exponent.
+
+## References
+
+Adapted from [Anthropic's
+Hashing.lean](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Sec3/Theorem17/Hashing.lean#L57-L101).
+-/
+
+@[expose] public section
+
+namespace Cslib
+
+open Polynomial in
+/-- The quotient ring `ℤ[X]/(X^p - 1)`. -/
+abbrev CyclicIntRing (p : ℕ) : Type := AdjoinRoot ((X : ℤ[X]) ^ p - C 1)
+
+namespace CyclicIntRing
+
+open Polynomial
+
+variable {p : ℕ}
+
+/-- The element `x` of `ℤ[x]/(x^p − 1)`. -/
+noncomputable def x (p : ℕ) : CyclicIntRing p := AdjoinRoot.root _
+
+/-- The coefficient of degree `r` in an element `z` of the quotient, as a linear map. It is the
+coefficient of `x^r` in the unique polynomial of degree less than `p` that represents `z`
+(Mathlib's `AdjoinRoot.modByMonicHom` gives that polynomial; it asks for the fact that `x^p − 1`
+is monic, which holds as `p ≠ 0`).
+-/
+noncomputable def coeff (hp : p ≠ 0) (r : ℕ) : CyclicIntRing p →ₗ[ℤ] ℤ :=
+  lcoeff ℤ r ∘ₗ AdjoinRoot.modByMonicHom (monic_X_pow_sub_C (1 : ℤ) hp)
+
+/-- The coefficient, in terms of the representing polynomial. -/
+theorem coeff_apply (hp : p ≠ 0) (r : ℕ) (z : CyclicIntRing p) :
+    coeff hp r z = (AdjoinRoot.modByMonicHom (monic_X_pow_sub_C (1 : ℤ) hp) z).coeff r :=
+  rfl
+
+/-- In `ℤ[x]/(x^p − 1)` we have `x^p = 1`. -/
+private theorem x_pow_self (p : ℕ) : x p ^ p = 1 := by
+  have h : AdjoinRoot.mk ((X : ℤ[X]) ^ p - C 1) ((X : ℤ[X]) ^ p - C 1) = 0 := AdjoinRoot.mk_self
+  rw [map_sub, map_pow, AdjoinRoot.mk_X, C_1, map_one] at h
+  exact sub_eq_zero.1 h
+
+/-- The coefficient of `x^r` in the power `x^k` of `ℤ[x]/(x^p − 1)` is 1 if `r = k mod p` and 0
+otherwise.
+-/
+theorem coeff_x_pow (hp : p ≠ 0) (k r : ℕ) :
+    coeff hp r (x p ^ k) = if r = k % p then 1 else 0 := by
+  have hred : x p ^ k = x p ^ (k % p) := by
+    conv_lhs => rw [← Nat.div_add_mod k p, pow_add, pow_mul, x_pow_self, one_pow, one_mul]
+  have hdeg : ((X : ℤ[X]) ^ (k % p)).degree < ((X : ℤ[X]) ^ p - C 1).degree := by
+    rw [degree_X_pow, degree_X_pow_sub_C (Nat.pos_of_ne_zero hp)]
+    exact_mod_cast Nat.mod_lt k (Nat.pos_of_ne_zero hp)
+  rw [coeff_apply, hred, x, ← AdjoinRoot.mk_X, ← map_pow, AdjoinRoot.modByMonicHom_mk,
+    (modByMonic_eq_self_iff (monic_X_pow_sub_C (1 : ℤ) hp)).2 hdeg, coeff_X_pow]
+
+end CyclicIntRing
+
+end Cslib

ComplexityTests/ExactTriangleHashing.lean

@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+import Complexity.Algorithms.ExactTriangle.Hashing
+
+/-!
+# Modular Exact Triangle counting and prime-selection regressions
+
+Concrete zeros, false positives, coefficient wraparound, minimum selection, the integer window
+boundary and an admitted instance of the universal bound. These assert no native running time.
+-/
+
+namespace ComplexityTests.ExactTriangleHashing
+
+open Cslib Cslib.Algorithms.ExactTriangle
+
+private def ab (a _ : Fin 2) : ℤ := if a = 0 then 0 else 2
+private def z (_ _ : Fin 2) : ℤ := 0
+
+private theorem window16 : primesInRange 16 = {2, 3} := by
+  rw [primesInRange_eq_filter]
+  decide
+
+-- Both endpoints matter: prime 2 is admitted at the lower endpoint for D=16;
+-- prime 5 is excluded at the upper endpoint for D=25, and prime 3 is admitted there.
+example : 2 ∈ primesInRange 16 ∧ 5 ∉ primesInRange 25 ∧ 3 ∈ primesInRange 25 := by
+  simp only [mem_primesInRange_iff_sq]
+  decide
+
+example : 2 ∉ primesInRange 17 := by rw [mem_primesInRange_iff_sq]; decide
+
+example : countZeroMod ab z z 2 = 8 ∧ countZeroMod ab z z 3 = 4 := by
+  unfold countZeroMod weightSum ab z
+  decide
+
+example : zeroCount ab z z = 4 ∧ falsePositiveCount ab z z 2 = 4 ∧
+    falsePositiveCount ab z z 3 = 0 := by
+  unfold zeroCount falsePositiveCount IsFalsePositive weightSum ab z
+  decide
+
+example : countZeroMod ab z z 0 = 4 ∧ falsePositiveCount ab z z 0 = 0 := by
+  unfold countZeroMod falsePositiveCount IsFalsePositive weightSum ab z
+  decide
+
+-- Counting distinguishes the two candidate primes; the minimum is 3.
+example : IsSelectedPrime ab z z 16 3 ∧ ¬IsSelectedPrime ab z z 16 2 := by
+  simp only [IsSelectedPrime, window16]
+  unfold countZeroMod weightSum ab z
+  decide
+
+-- A tie permits either minimum prime; the predicate does not impose a tie-break.
+example : IsSelectedPrime (fun _ _ : Fin 1 => 0) (fun _ _ => 0) (fun _ _ => 0) 16 2 ∧
+    IsSelectedPrime (fun _ _ : Fin 1 => 0) (fun _ _ => 0) (fun _ _ => 0) 16 3 := by
+  constructor <;> refine ⟨by rw [window16]; decide, ?_⟩ <;> intro q _ <;>
+    simp [countZeroMod, weightSum]
+
+example : HasZeroTriangle ab z z := ⟨0, 0, 0, rfl⟩
+example : 0 < zeroCount ab z z := (zeroCount_pos_iff ab z z).mpr ⟨0, 0, 0, rfl⟩
+
+private def one (_ _ : Fin 2) : ℤ := 1
+
+example : ¬HasZeroTriangle one one one := by
+  rintro ⟨a, b, c, h⟩
+  norm_num [one] at h
+
+example : zeroCount one one one = 0 ∧ countZeroMod one one one 3 = 8 ∧
+    falsePositiveCount one one one 3 = 8 := by
+  unfold zeroCount countZeroMod falsePositiveCount IsFalsePositive weightSum one
+  decide
+
+-- A negative residue and a positive residue wrap to exponent zero modulo 3.
+example : CyclicIntRing.coeff (by decide : 3 ≠ 0) 0
+    ((matP (fun _ _ : Fin 2 => (-1 : ℤ)) 3 *
+      matQ (fun _ _ : Fin 2 => (1 : ℤ)) 3) 0 0) = 2 := by
+  rw [coeff_matP_mul_matQ (fun _ _ : Fin 2 => (1 : ℤ))
+    (fun _ _ : Fin 2 => (-1 : ℤ)) (by decide) 0 0 0 (by decide)]
+  decide
+
+-- These matrices are asymmetric: transposing either input changes the selected count.
+private def ac (a c : Fin 2) : ℤ := if a = 0 then if c = 0 then -1 else 2 else 0
+private def bc (b c : Fin 2) : ℤ := if b = 0 ∧ c = 1 then 1 else 0
+
+example : CyclicIntRing.coeff (by decide : 3 ≠ 0) 0 ((matP ac 3 * matQ bc 3) 0 0) = 1 := by
+  rw [coeff_matP_mul_matQ bc ac (by decide) 0 0 0 (by decide)]
+  unfold ac bc
+  decide
+
+example : CyclicIntRing.coeff (by decide : 2 ≠ 0) 1 (CyclicIntRing.x 2 ^ 5) = 1 := by
+  rw [CyclicIntRing.coeff_x_pow]
+  norm_num
+
+example : CyclicIntRing.coeff (by decide : 2 ≠ 0) 3 (CyclicIntRing.x 2 ^ 5) = 0 := by
+  rw [CyclicIntRing.coeff_x_pow]
+  norm_num
+
+example : zeroCount (fun _ _ : Fin 0 => 0) (fun _ _ => 0) (fun _ _ => 0) = 0 := by
+  simp [zeroCount]
+
+example : ¬WeightsBoundedBy (fun _ _ : Fin 1 => (0 : ℤ)) (fun _ _ => 0) (fun _ _ => 0) (-1) := by
+  norm_num [WeightsBoundedBy]
+
+-- The full bound's n,D,kappa hypotheses and input bound have a concrete witness.
+example : (falsePositiveCount (fun _ _ : Fin 16 => 0) (fun _ _ => 0) (fun _ _ => 0) 2 : ℝ) ≤
+    Hashing.falsePositiveConst * (1 * (16 : ℝ) ^ 3 * Real.log 16 / Real.sqrt 16) := by
+  apply Hashing.falsePositiveCount_le_const_mul (by decide : 16 ≤ 16) (by decide : 16 ≤ 16)
+    (by norm_num : (1 : ℝ) ≤ 1)
+  · norm_num [WeightsBoundedBy]
+  · refine ⟨by rw [window16]; decide, ?_⟩
+    intro q _
+    simp [countZeroMod, weightSum]
+
+end ComplexityTests.ExactTriangleHashing

NOTICE

@@ -1,10 +1,11 @@
 The 3SUM/Exact Triangle reductions, their finite counting lemmas and native matrix builder in
-Complexity/Algorithms/ExactTriangle/{Defs,Lopsided}.lean,
+Complexity/Algorithms/ExactTriangle/{Defs,Weights,Lopsided,Hashing}.lean,
 Complexity/Algorithms/ThreeSum/,
 Complexity/Algorithms/WordRAM/ThreeSum/,
 Complexity/Foundations/Data/Finset/Average.lean,
 Complexity/Foundations/Data/Matrix/IntegerBits.lean and
-Complexity/Foundations/NumberTheory/PrimeCounting.lean are adapted from
+Complexity/Foundations/NumberTheory/{PrimeCounting,PrimeWindow}.lean and
+Complexity/Foundations/RingTheory/CyclicIntRing.lean are adapted from
 anthropics/formal-math, 3sum-apsp, revision
 16a5ce41304fcdaea4e0be7c132e1c361dc26da5.
 
@@ -13,3 +14,7 @@ Sparse Lopsided Graphs"
 Copyright 2026 Anthropic, PBC
 
 This product is licensed under the Apache License, Version 2.0 (see LICENSE).
+
+The prime-window proof also adapts Mathlib/NumberTheory/Bertrand.lean,
+Copyright (c) 2020 Patrick Stevens; authors Patrick Stevens, Bolton Bailey,
+under the Apache License, Version 2.0.

ROADMAP.md

@@ -422,8 +422,9 @@ each statement against the numbered result. Organize modules by subject, not cha
   has the Convolution-3SUM/Exact Triangle correctness reduction, a charged native single-instance
   matrix builder and the complete finite mathematical Chan–He reduction ([#1435]), including
   ordinary distinct-position inputs and explicit size bounds. The finite lopsided matrix/counting
-  interface ([#1438]) adds padding, detection and signed digit reconstruction; it still needs
-  modular Exact Triangle hashing/false-positive splitting, tensor/sparse-query programs, native
+  interface ([#1438]) adds padding, detection and signed digit reconstruction. Modular counting
+  and the selected-prime false-positive bound ([#1442]) are proved mathematically; it still needs
+  residue/chunk/piece splitting and witness recovery, tensor/sparse-query programs, native
   Chan–He preprocessing, the reduction host, the fast Exact Triangle solver and full input/time/width/
   asymptotic composition, then the improved Section 4 route to exponent 1.9992; size-based width
   selection with an input-fit guarantee and explicit overhead; expected-time rules for unbounded
@@ -560,4 +561,5 @@ not planned, not as proved.
 [#1394]: https://github.com/cslib-community/complexitylib/issues/1394
 [#1435]: https://github.com/cslib-community/complexitylib/issues/1435
 [#1438]: https://github.com/cslib-community/complexitylib/issues/1438
+[#1442]: https://github.com/cslib-community/complexitylib/issues/1442
 [#1449]: https://github.com/cslib-community/complexitylib/issues/1449

UPSTREAM.md

@@ -158,6 +158,13 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   Given its arguments in registers, it writes one instance in at most `131*t² + 5` instructions
   at width `w + 2`, excluding the halt; its theorem identifies the three encoded matrices and
   preserves the input. Layout, signed index/filler bounds and target address bounds are explicit.
+  The existing signed and unsigned APIs were reused; no source machine or separate run semantics
+  were copied. The full reduction host, native Chan–He preprocessing, fast Exact Triangle and full
+  input/time/width/asymptotic composition remain in
+  [#1394](https://github.com/cslib-community/complexitylib/issues/1394), including the improved
+  Section 4 route needed for the published exponent 1.9992. Anthropic's copyright and attribution
+  are retained; the native proofs and representation choices are local.
+
   `Algorithms/ThreeSum/ThreeSets.lean` and `ArrayPacking.lean` provide the generic distinct-position
   frontend and three-array packing. `Algorithms/ThreeSum/ChanHe/` now adapts the core mathematical
   reduction: minimum-prime searches, collision/heavy-element bounds, light-element arrays, bounded
@@ -174,8 +181,16 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   `Set.EqOn`; no additional weighted-triangle predicate or source machine is introduced.
   This is the mathematical interface milestone
   [#1438](https://github.com/cslib-community/complexitylib/issues/1438), with no sparsity assumption,
-  preprocessing/time claim or solver. Modular hashing/false-positive splitting and tensor/sparse
-  query programs remain in #1394, alongside the native and asymptotic composition below.
+  preprocessing/time claim or solver. `Algorithms/ExactTriangle/{Weights,Hashing}.lean` now adapts
+  the modular counting/coefficient identities, minimum-count prime and uniform false-positive
+  bound from `Sec3/Theorem17/Hashing.lean`, using supplied matrices and the existing decision
+  predicate. Its integer-square window characterisation supports later native enumeration.
+  The quotient/coefficient API lives in `Foundations/RingTheory/CyclicIntRing.lean`; the uniform
+  all-window prime-count bound lives in `Foundations/NumberTheory/PrimeWindow.lean`, retaining
+  the source credit to Mathlib, Patrick Stevens and Bolton Bailey. These are mathematical
+  statements, not native instructions or an assumed solver. See
+  [#1442](https://github.com/cslib-community/complexitylib/issues/1442). Residue/chunk/piece splitting,
+  witness recovery and tensor/sparse query programs remain in #1394, alongside native composition.
   The existing signed and unsigned APIs were reused; no source machine or separate run semantics
   were copied. The full reduction host, native Chan–He preprocessing, fast Exact Triangle and full
   input/time/width/asymptotic composition remain in

references.bib

@@ -125,6 +125,18 @@ @article{AllenderRubinstein1988
   doi       = {10.1137/0217075}
 }
 
+@misc{AlmanWilliams2026,
+  author        = {Alman, Josh and Vassilevska Williams, Virginia},
+  title         = {Truly Subquadratic {3SUM} and Truly Subcubic {APSP} via Triangles in
+                   Sparse Lopsided Graphs},
+  year          = {2026},
+  eprint        = {2610.06783},
+  archivePrefix = {arXiv},
+  primaryClass  = {cs.DS},
+  doi           = {10.48550/arXiv.2610.06783},
+  url           = {https://arxiv.org/abs/2610.06783v1}
+}
+
 @article{AlonBoppana1987,
   author    = {Alon, Noga and Boppana, Ravi B.},
   title     = {The Monotone Circuit Complexity of {B}oolean Functions},