Modular counts and prime selection for integer Exact Triangle

A minimum-count prime in [sqrt D / 2, sqrt D) also minimises false positives. For weights bounded by n^κ, with 16 ≤ D ≤ n and 1 ≤ κ, a universal constant bounds its false positives by C * κ * n^3 * log n / sqrt D. The prime count used here is proved for every admitted D.

Main definitions

• countZeroMod, falsePositiveCount, zeroCount: counts of finite triples.
• IsSelectedPrime: a minimum-count prime in the specified window.
• matP, matQ: cyclic polynomial matrices encoding edge residues.

Main results

• countZeroMod_eq: modular count is the sum of false positives and true zeros.
• coeff_matP_mul_matQ, falsePositiveCount_add_zeroCount_eq_sum_coeff: coefficient identities.
• exists_isSelectedPrime: the minimum exists.
• falsePositiveCount_le_const_mul: the uniform false-positive bound.

This is a mathematical reduction step. No native program or charged running-time bound is asserted. The supplied three matrices retain the existing HasZeroTriangle semantics.

References

The modular reduction is part of [AlmanWilliams2026, Section 3]. Direct adaptation of Anthropic's Hashing.lean, with the minimal count/selection definitions extracted from its PaperStatements.lean. The declaration docstrings describe the Lean definitions and statements in local notation. The source pin is anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5.

def Cslib.Algorithms.ExactTriangle.countZeroMod {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (p : ℕ) : ℕ

Count vertex triples whose three edge weights have sum congruent to zero modulo p.

def Cslib.Algorithms.ExactTriangle.IsSelectedPrime {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (D p : ℕ) : Prop

A prime in Nat.sqrtPrimeWindow D whose modular-zero count is minimal among all primes in that window. Tied minima all satisfy this predicate.

Counting triples with a vanishing modular weight sum

@[reducible, inline]

abbrev Cslib.Algorithms.ExactTriangle.IsFalsePositive {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (p : ℕ) (t : Fin n × Fin n × Fin n) : Prop

A vertex triple has a nonzero integer weight sum that is congruent to zero modulo p.

def Cslib.Algorithms.ExactTriangle.falsePositiveCount {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (p : ℕ) : ℕ

Count vertex triples satisfying IsFalsePositive for the supplied three weight matrices and modulus.

def Cslib.Algorithms.ExactTriangle.zeroCount {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) : ℕ

Count vertex triples whose three supplied edge weights sum to zero as an integer.

theorem Cslib.Algorithms.ExactTriangle.zeroCount_pos_iff {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) : 0 < zeroCount wAB wBC wAC ↔ HasZeroTriangle wAB wBC wAC

The zero-triple count is positive exactly when the supplied matrices satisfy HasZeroTriangle.

theorem Cslib.Algorithms.ExactTriangle.countZeroMod_eq {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (p : ℕ) : countZeroMod wAB wBC wAC p = falsePositiveCount wAB wBC wAC p + zeroCount wAB wBC wAC

Partition the modular-zero triples into false positives and exact zero-sum triples. The exact-zero count is independent of the modulus.

noncomputable def Cslib.Algorithms.ExactTriangle.matP {n : ℕ} (wAC : Fin n → Fin n → ℤ) (p : ℕ) : Matrix (Fin n) (Fin n) (CyclicIntRing p)

Encode the A–C weight at (a,c) as a power of the cyclic polynomial generator, with exponent equal to its nonnegative residue modulo p.

noncomputable def Cslib.Algorithms.ExactTriangle.matQ {n : ℕ} (wBC : Fin n → Fin n → ℤ) (p : ℕ) : Matrix (Fin n) (Fin n) (CyclicIntRing p)

Encode the B–C weight at (b,c) in matrix position (c,b). This orientation makes the product sum over the middle index c.

theorem Cslib.Algorithms.ExactTriangle.coeff_matP_mul_matQ {n : ℕ} (wBC wAC : Fin n → Fin n → ℤ) {p : ℕ} (hp : p ≠ 0) (a b : Fin n) (r : ℕ) (hr : r < p) : (CyclicIntRing.coeff hp r) ((matP wAC p * matQ wBC p) a b) = ↑{c : Fin n | wAC a c + wBC b c ≡ ↑r [ZMOD ↑p]}.card

For a nonzero modulus and a residue r < p, the coefficient of degree r in the cyclic matrix product counts middle vertices whose two incident weights sum to r modulo p.

theorem Cslib.Algorithms.ExactTriangle.falsePositiveCount_add_zeroCount_eq_sum_coeff {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) {p : ℕ} (hp : p ≠ 0) : ↑(falsePositiveCount wAB wBC wAC p + zeroCount wAB wBC wAC) = ∑ a : Fin n, ∑ b : Fin n, (CyclicIntRing.coeff hp (-wAB a b % ↑p).toNat) ((matP wAC p * matQ wBC p) a b)

Recover the total modular-zero count from the cyclic matrix product by summing, over (a,b), the coefficient at the residue of -wAB a b.

Selecting the prime

theorem Cslib.Algorithms.ExactTriangle.exists_isSelectedPrime {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (D : ℕ) (hD : 16 ≤ D) : ∃ (p : ℕ), IsSelectedPrime wAB wBC wAC D p

For every D ≥ 16 and every three supplied weight matrices, the prime window contains a minimum of the modular-zero count.

theorem Cslib.Algorithms.ExactTriangle.IsSelectedPrime.falsePositiveCount_le {n D p : ℕ} {wAB wBC wAC : Fin n → Fin n → ℤ} (hp : IsSelectedPrime wAB wBC wAC D p) (q : ℕ) : q ∈ D.sqrtPrimeWindow → falsePositiveCount wAB wBC wAC p ≤ falsePositiveCount wAB wBC wAC q

A selected minimum of the modular-zero count also minimizes the false-positive count over the same prime window.

The bound on the number of false positives of the selected prime

theorem Cslib.Algorithms.ExactTriangle.card_falsePositive_primes_le {n D : ℕ} {κ : ℝ} (wAB wBC wAC : Fin n → Fin n → ℤ) (hD : 16 ≤ D) (hT : WeightsBoundedBy wAB wBC wAC (↑n ^ κ)) (t : Fin n × Fin n × Fin n) (ht : weightSum wAB wBC wAC t.1 t.2.1 t.2.2 ≠ 0) : ↑{p ∈ D.sqrtPrimeWindow | IsFalsePositive wAB wBC wAC p t}.card ≤ Real.logb (√↑D / 2) (3 * ↑n ^ κ)

For a fixed nonzero-sum triple and edge weights bounded by n^κ, bound the number of window primes accepting that triple by the base-sqrt D / 2 logarithm of 3*n^κ.

theorem Cslib.Algorithms.ExactTriangle.sum_falsePositiveCount_le {n D : ℕ} {κ : ℝ} (wAB wBC wAC : Fin n → Fin n → ℤ) (hD : 16 ≤ D) (hκ : 1 ≤ κ) (hT : WeightsBoundedBy wAB wBC wAC (↑n ^ κ)) : ↑(∑ p ∈ D.sqrtPrimeWindow, falsePositiveCount wAB wBC wAC p) ≤ ↑n ^ 3 * Real.logb (√↑D / 2) (3 * ↑n ^ κ)

Sum the per-triple prime-divisibility bound over all n^3 triples. For D ≥ 16, κ ≥ 1 and edge weights bounded by n^κ, the sum of false-positive counts is at most n^3 * logb (sqrt D / 2) (3*n^κ).

theorem Cslib.Algorithms.ExactTriangle.IsSelectedPrime.falsePositiveCount_mul_card_le_sum {n D p : ℕ} {wAB wBC wAC : Fin n → Fin n → ℤ} (hp : IsSelectedPrime wAB wBC wAC D p) : falsePositiveCount wAB wBC wAC p * D.sqrtPrimeWindow.card ≤ ∑ q ∈ D.sqrtPrimeWindow, falsePositiveCount wAB wBC wAC q

Multiply the selected prime’s minimum false-positive count by the number of window primes to obtain a bound by the sum of their false-positive counts.

theorem Cslib.Algorithms.ExactTriangle.falsePositiveCount_le_of_le_card_sqrtPrimeWindow {n D p : ℕ} {κ c : ℝ} (wAB wBC wAC : Fin n → Fin n → ℤ) (hc : 0 < c) (hcard : c * (√↑D / Real.log ↑D) ≤ ↑D.sqrtPrimeWindow.card) (hD : 16 ≤ D) (hDn : D ≤ n) (hκ : 1 ≤ κ) (hT : WeightsBoundedBy wAB wBC wAC (↑n ^ κ)) (hp : IsSelectedPrime wAB wBC wAC D p) : ↑(falsePositiveCount wAB wBC wAC p) ≤ 4 / c * (↑n ^ 3 * Real.log (3 * ↑n ^ κ) / √↑D)

For 16 ≤ D ≤ n, κ ≥ 1 and edge weights bounded by n^κ, a positive pointwise prime-count lower bound c * sqrt D / log D gives every selected prime at most (4/c) * n^3 * log (3*n^κ) / sqrt D false positives.

theorem Cslib.Algorithms.ExactTriangle.exists_falsePositiveCount_le : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {n D p : ℕ} {κ : ℝ}, 16 ≤ D → D ≤ n → 1 ≤ κ → ∀ (wAB wBC wAC : Fin n → Fin n → ℤ), WeightsBoundedBy wAB wBC wAC (↑n ^ κ) → IsSelectedPrime wAB wBC wAC D p → ↑(falsePositiveCount wAB wBC wAC p) ≤ C * (κ * ↑n ^ 3 * Real.log ↑n / √↑D)

There is a universal C ≥ 1 such that, for 16 ≤ D ≤ n, κ ≥ 1 and edge weights bounded by n^κ, every selected prime has at most C * κ * n^3 * log n / sqrt D false positives.

noncomputable def Cslib.Algorithms.ExactTriangle.falsePositiveConst : ℝ

A universal real constant witnessing exists_falsePositiveCount_le. It depends on none of the input dimensions, weight matrices, exponent or selected prime, and is at least one.

theorem Cslib.Algorithms.ExactTriangle.one_le_falsePositiveConst : 1 ≤ falsePositiveConst

The universal false-positive constant falsePositiveConst is at least one.

theorem Cslib.Algorithms.ExactTriangle.falsePositiveCount_le_const_mul {n D p : ℕ} {κ : ℝ} (hD : 16 ≤ D) (hDn : D ≤ n) (hκ : 1 ≤ κ) (wAB wBC wAC : Fin n → Fin n → ℤ) (hT : WeightsBoundedBy wAB wBC wAC (↑n ^ κ)) (hp : IsSelectedPrime wAB wBC wAC D p) : ↑(falsePositiveCount wAB wBC wAC p) ≤ falsePositiveConst * (κ * ↑n ^ 3 * Real.log ↑n / √↑D)

For 16 ≤ D ≤ n, κ ≥ 1 and edge weights bounded by n^κ, bound every selected prime’s false-positive count by falsePositiveConst * κ * n^3 * log n / sqrt D.