diff --git a/Complexity.lean b/Complexity.lean index acebc4b646..a6efd4ca55 100644 --- a/Complexity.lean +++ b/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 diff --git a/Complexity/Algorithms/ExactTriangle/Hashing.lean b/Complexity/Algorithms/ExactTriangle/Hashing.lean new file mode 100644 index 0000000000..fbb2834b6e --- /dev/null +++ b/Complexity/Algorithms/ExactTriangle/Hashing.lean @@ -0,0 +1,508 @@ +/- +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.Weights +public import Complexity.Foundations.NumberTheory.PrimeWindow +public import Complexity.Foundations.RingTheory.CyclicIntRing +public import Mathlib.Data.Matrix.Mul + +/-! +# Modular counts and prime selection for integer Exact Triangle + +Let `S(a,b,c)` denote `weightSum`, `F(p)` the false-positive count and `Z₀` the zero count. 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. +* `Hashing.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](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Sec3/Theorem17/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`. +-/ + +@[expose] public section + +namespace Cslib.Algorithms.ExactTriangle + +open Classical in +/-- Prime numbers in the half-open real interval `[sqrt D / 2, sqrt D)`. +-/ +noncomputable def primesInRange (D : ℕ) : Finset ℕ := + (Finset.range D).filter fun p => p.Prime ∧ Real.sqrt D / 2 ≤ (p : ℝ) ∧ (p : ℝ) < Real.sqrt D + +/-- Count vertex triples whose three edge weights have sum congruent to zero modulo `p`. +-/ +def countZeroMod {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (p : ℕ) : ℕ := + (Finset.univ.filter fun t : Fin n × Fin n × Fin n => + weightSum wAB wBC wAC t.1 t.2.1 t.2.2 ≡ 0 [ZMOD (p : ℤ)]).card + +/-- A prime in `primesInRange D` whose modular-zero count is minimal among all primes in that +window. Tied minima all satisfy this predicate. +-/ +def IsSelectedPrime {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) (D p : ℕ) : Prop := + p ∈ primesInRange D ∧ ∀ q ∈ primesInRange D, + countZeroMod wAB wBC wAC p ≤ countZeroMod wAB wBC wAC q + +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) + +private theorem natCast_toNat_emod {p : ℕ} (hp : 0 < p) (u : ℤ) : + ((u % (p : ℤ)).toNat : ℤ) = u % (p : ℤ) := + Int.toNat_of_nonneg (Int.emod_nonneg _ (by omega)) + +private theorem toNat_emod_lt {p : ℕ} (hp : 0 < p) (u : ℤ) : (u % (p : ℤ)).toNat < p := by + have := Int.emod_nonneg u (by omega : (p : ℤ) ≠ 0) + have := Int.emod_lt_of_pos u (by omega : (0 : ℤ) < p) + omega + +/-! +### The primes in the range -/ + +/-- Window membership is equivalent to primality and the two real endpoint inequalities. The +finite enumeration bound in `primesInRange` excludes no member of the interval. +-/ +theorem mem_primesInRange {D p : ℕ} : + p ∈ primesInRange D ↔ p.Prime ∧ Real.sqrt D / 2 ≤ (p : ℝ) ∧ (p : ℝ) < Real.sqrt D := by + unfold primesInRange + rw [Finset.mem_filter, Finset.mem_range] + refine ⟨fun h => h.2, fun h => ⟨?_, h⟩⟩ + -- From `p < √D` we get `p ≤ p² < D`. + have hsq : p ^ 2 < D := by exact_mod_cast (Real.lt_sqrt (Nat.cast_nonneg p)).1 h.2.2 + exact (Nat.le_self_pow two_ne_zero p).trans_lt hsq + +/-- Characterize window membership using primality and integer-square inequalities, including the +closed lower and open upper endpoints. +-/ +theorem mem_primesInRange_iff_sq {D p : ℕ} : + p ∈ primesInRange D ↔ p.Prime ∧ D ≤ 4 * p ^ 2 ∧ p ^ 2 < D := by + rw [mem_primesInRange] + have hp0 : (0 : ℝ) ≤ p := Nat.cast_nonneg p + have hsqrt0 : 0 ≤ Real.sqrt (D : ℝ) := Real.sqrt_nonneg _ + have hsqrt : (Real.sqrt (D : ℝ)) ^ 2 = D := Real.sq_sqrt (Nat.cast_nonneg D) + constructor + · rintro ⟨hp, hlo, hhi⟩ + refine ⟨hp, ?_, ?_⟩ + · have h : (D : ℝ) ≤ 4 * (p : ℝ) ^ 2 := by nlinarith + exact_mod_cast h + · exact_mod_cast (Real.lt_sqrt hp0).1 hhi + · rintro ⟨hp, hlo, hhi⟩ + refine ⟨hp, ?_, (Real.lt_sqrt hp0).2 (by exact_mod_cast hhi)⟩ + have h : (D : ℝ) ≤ 4 * (p : ℝ) ^ 2 := by exact_mod_cast hlo + nlinarith + +/-- Enumerate the real prime window using a decidable filter of the integers below `D`. +-/ +theorem primesInRange_eq_filter (D : ℕ) : + primesInRange D = (Finset.range D).filter fun p => p.Prime ∧ D ≤ 4 * p ^ 2 ∧ p ^ 2 < D := by + ext p + rw [mem_primesInRange_iff_sq, Finset.mem_filter, Finset.mem_range] + exact ⟨fun h => ⟨(Nat.le_self_pow two_ne_zero p).trans_lt h.2.2, h⟩, fun h => h.2⟩ + +/-- A number `r < p` is the sum of the residues of `u` and `v` in `{0, …, p − 1}`, reduced modulo +`p`, exactly if `u + v ≡ r`. +-/ +private theorem eq_add_toNat_emod_iff {p r : ℕ} (hp : p ≠ 0) (hr : r < p) (u v : ℤ) : + r = ((u % (p : ℤ)).toNat + (v % (p : ℤ)).toNat) % p ↔ u + v ≡ (r : ℤ) [ZMOD (p : ℤ)] := by + rw [← Int.natCast_inj, Int.ModEq, Int.emod_eq_of_lt (Int.natCast_nonneg r) (by exact_mod_cast hr), + eq_comm] + push_cast + rw [natCast_toNat_emod (Nat.pos_of_ne_zero hp), + natCast_toNat_emod (Nat.pos_of_ne_zero hp), + ← Int.add_emod] + +/-! +### Counting the triples with `S(a,b,c) ≡ 0 (mod p)` -/ + +section Counting + +variable {n : ℕ} (wAB wBC wAC : Fin n → Fin n → ℤ) + +/-- A vertex triple has a nonzero integer weight sum that is congruent to zero modulo `p`. +-/ +abbrev IsFalsePositive (p : ℕ) (t : Fin n × Fin n × Fin n) : Prop := + weightSum wAB wBC wAC t.1 t.2.1 t.2.2 ≠ 0 ∧ (p : ℤ) ∣ weightSum wAB wBC wAC t.1 t.2.1 t.2.2 + +/-- Count vertex triples satisfying `IsFalsePositive` for the supplied three weight matrices and +modulus. +-/ +def falsePositiveCount (p : ℕ) : ℕ := + (Finset.univ.filter fun t : Fin n × Fin n × Fin n => IsFalsePositive wAB wBC wAC p t).card + +/-- Count vertex triples whose three supplied edge weights sum to zero as an integer. +-/ +def zeroCount : ℕ := + (Finset.univ.filter fun t : Fin n × Fin n × Fin n => weightSum wAB wBC wAC t.1 t.2.1 t.2.2 = + 0).card + +/-- The zero-triple count is positive exactly when the supplied matrices satisfy +`HasZeroTriangle`. +-/ +theorem zeroCount_pos_iff : 0 < zeroCount wAB wBC wAC ↔ HasZeroTriangle wAB wBC wAC := by + classical + simp only [zeroCount, Finset.card_pos, HasZeroTriangle] + constructor + · rintro ⟨⟨a, b, c⟩, h⟩ + exact ⟨a, b, c, (Finset.mem_filter.mp h).2⟩ + · rintro ⟨a, b, c, h⟩ + exact ⟨(a, b, c), Finset.mem_filter.mpr ⟨Finset.mem_univ _, h⟩⟩ + +/-- Partition the modular-zero triples into false positives and exact zero-sum triples. The +exact-zero count is independent of the modulus. +-/ +theorem countZeroMod_eq (p : ℕ) : (countZeroMod wAB wBC wAC) p = (falsePositiveCount wAB wBC + wAC) p + (zeroCount wAB wBC wAC) := by + classical + simp only [countZeroMod, falsePositiveCount, zeroCount, Finset.card_filter, ← + Finset.sum_add_distrib] + -- A triple with `p ∣ S(a,b,c)` is a zero triangle or a false positive, and not both. + refine Finset.sum_congr rfl fun t _ => ?_ + by_cases h0 : weightSum wAB wBC wAC t.1 t.2.1 t.2.2 = 0 <;> + simp [IsFalsePositive, Int.modEq_zero_iff_dvd, h0] + +/-- 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 matP (p : ℕ) : Matrix (Fin n) (Fin n) (CyclicIntRing p) := + Matrix.of fun a c => CyclicIntRing.x p ^ (wAC a c % (p : ℤ)).toNat + +/-- Encode the B–C weight at `(b,c)` in matrix position `(c,b)`. This orientation makes the +product sum over the middle index `c`. +-/ +noncomputable def matQ (p : ℕ) : Matrix (Fin n) (Fin n) (CyclicIntRing p) := + Matrix.of fun c b => CyclicIntRing.x p ^ (wBC b c % (p : ℤ)).toNat + +/-- 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 coeff_matP_mul_matQ {p : ℕ} (hp : p ≠ 0) (a b : Fin n) (r : ℕ) (hr : r < p) : + CyclicIntRing.coeff hp r ((matP wAC p * matQ wBC p) a b) = + ((Finset.univ.filter fun c : Fin n => + wAC a c + wBC b c ≡ (r : ℤ) [ZMOD (p : ℤ)]).card : ℤ) := by + classical + -- `(PQ)[a,b]` is the sum over `c` of `x^(w(a,c) mod p + w(b,c) mod p)`, and the coefficient of + -- `x^r` in each term is 1 or 0. + rw [Matrix.mul_apply] + simp only [matP, matQ, Matrix.of_apply, ← pow_add] + rw [map_sum] + simp only [CyclicIntRing.coeff_x_pow] + rw [Finset.card_filter] + push_cast + refine Finset.sum_congr rfl fun c _ => ?_ + simp only [eq_add_toNat_emod_iff hp hr] + +/-- 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`. +-/ +theorem falsePositiveCount_add_zeroCount_eq_sum_coeff {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) := by + classical + rw [← countZeroMod_eq] + unfold countZeroMod + rw [Finset.card_filter, Fintype.sum_prod_type] + push_cast + refine Finset.sum_congr rfl fun a _ => ?_ + rw [Fintype.sum_prod_type] + refine Finset.sum_congr rfl fun b _ => ?_ + have hcast := natCast_toNat_emod (Nat.pos_of_ne_zero hp) (-wAB a b) + rw [(coeff_matP_mul_matQ wBC wAC) hp a b _ (toNat_emod_lt (Nat.pos_of_ne_zero hp) _), + Finset.card_filter] + push_cast + refine Finset.sum_congr rfl fun c _ => ?_ + -- `S(a,b,c) ≡ 0` says the same as `w(a,c) + w(b,c) ≡ -w(a,b)`, and `-w(a,b)` is congruent to its + -- residue. + have hres : (-wAB a b) % (p : ℤ) ≡ -wAB a b [ZMOD (p : ℤ)] := Int.mod_modEq _ _ + have hiff : weightSum wAB wBC wAC a b c ≡ 0 [ZMOD (p : ℤ)] ↔ + wAC a c + wBC b c ≡ ((((-wAB a b) % (p : ℤ)).toNat : ℕ) : ℤ) [ZMOD (p : ℤ)] := by + rw [hcast, show wAC a c + wBC b c ≡ (-wAB a b) % (p : ℤ) [ZMOD (p : ℤ)] ↔ + wAC a c + wBC b c ≡ -wAB a b [ZMOD (p : ℤ)] from + ⟨fun h => h.trans hres, fun h => h.trans hres.symm⟩, + Int.modEq_iff_dvd, Int.modEq_iff_dvd, + show 0 - weightSum wAB wBC wAC a b c = -wAB a b - (wAC a c + wBC b c) by + simp only [weightSum]; ring] + simp only [hiff] + +end Counting + +/-- For `D ≥ 16`, the number of primes in `primesInRange D` is strictly less than `sqrt D`. +-/ +theorem card_primesInRange_lt (D : ℕ) (hD : 16 ≤ D) : + ((primesInRange D).card : ℝ) < Real.sqrt D := by + have hpos : 0 < Real.sqrt D := by linarith [four_le_sqrt hD] + -- The primes in the range are among the numbers `1, …, ⌈√D⌉ - 1`. + have hsub : primesInRange D ⊆ Finset.Ico 1 ⌈Real.sqrt D⌉₊ := by + intro p hp + obtain ⟨hprime, -, hlt⟩ := mem_primesInRange.1 hp + exact Finset.mem_Ico.2 ⟨hprime.one_lt.le, Nat.lt_ceil.2 hlt⟩ + have hcard : (primesInRange D).card + 1 ≤ ⌈Real.sqrt D⌉₊ := by + have hle := Finset.card_le_card hsub + have hone : 1 ≤ ⌈Real.sqrt D⌉₊ := Nat.one_le_ceil_iff.2 hpos + rw [Nat.card_Ico] at hle + omega + have hcast : ((primesInRange D).card : ℝ) + 1 ≤ (⌈Real.sqrt D⌉₊ : ℝ) := by exact_mod_cast hcard + linarith [Nat.ceil_lt_add_one hpos.le] + +/-! +### Selecting the prime -/ + +section Selection + +variable {n D p : ℕ} {κ : ℝ} (wAB wBC wAC : Fin n → Fin n → ℤ) + +/-- For every `D ≥ 16` and every three supplied weight matrices, the prime window contains a +minimum of the modular-zero count. +-/ +theorem exists_isSelectedPrime (D : ℕ) (hD : 16 ≤ D) : ∃ p, IsSelectedPrime wAB wBC wAC D p := by + obtain ⟨q, hq⟩ := + Nat.exists_prime_half_le_and_lt (Real.sqrt D) (four_le_sqrt hD) + exact Finset.exists_min_image (primesInRange D) (countZeroMod wAB wBC wAC) ⟨q, + mem_primesInRange.2 hq⟩ + +/-- A selected minimum of the modular-zero count also minimizes the false-positive count over the +same prime window. +-/ +theorem IsSelectedPrime.falsePositiveCount_le {wAB wBC wAC : Fin n → Fin n → ℤ} (hp : + IsSelectedPrime wAB wBC wAC D p) : + ∀ q ∈ primesInRange D, (falsePositiveCount wAB wBC wAC) p ≤ (falsePositiveCount wAB wBC wAC) + q := by + intro q hq + have h := hp.2 q hq + rw [countZeroMod_eq, countZeroMod_eq] at h + omega + +/-! +### The bound on the number of false positives of the selected prime -/ + +open Classical in +/-- 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 card_falsePositive_primes_le (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) : + (((primesInRange D).filter fun p => IsFalsePositive wAB wBC wAC p t).card : ℝ) + ≤ Real.logb (Real.sqrt D / 2) (3 * (n : ℝ) ^ κ) := by + have hsqrt := four_le_sqrt hD + set divisors := (primesInRange D).filter fun p => IsFalsePositive wAB wBC wAC p t + have hmem : ∀ p ∈ divisors, + p.Prime ∧ Real.sqrt D / 2 ≤ (p : ℝ) ∧ (p : ℤ) ∣ weightSum wAB wBC wAC t.1 t.2.1 t.2.2 := by + intro p hp + obtain ⟨hrange, -, hdvd⟩ := Finset.mem_filter.1 hp + obtain ⟨hprime, hge, -⟩ := mem_primesInRange.1 hrange + exact ⟨hprime, hge, hdvd⟩ + -- The product of these primes divides `S(a,b,c)`, so it is at most `|S(a,b,c)| ≤ 3n^κ`. + have hdvd : ∏ p ∈ divisors, p ∣ (weightSum wAB wBC wAC t.1 t.2.1 t.2.2).natAbs := + Finset.prod_primes_dvd _ (fun p hp => (hmem p hp).1.prime) + fun p hp => Int.natCast_dvd.1 (hmem p hp).2.2 + have hprod : ∏ p ∈ divisors, (p : ℝ) ≤ 3 * (n : ℝ) ^ κ := + calc ∏ p ∈ divisors, (p : ℝ) = ((∏ p ∈ divisors, p : ℕ) : ℝ) := (Nat.cast_prod _ _).symm + _ ≤ ((weightSum wAB wBC wAC t.1 t.2.1 t.2.2).natAbs : ℝ) := by + exact_mod_cast Nat.le_of_dvd (Int.natAbs_pos.2 ht) hdvd + _ = ((|weightSum wAB wBC wAC t.1 t.2.1 t.2.2| : ℤ) : ℝ) := Nat.cast_natAbs _ + _ ≤ 3 * (n : ℝ) ^ κ := (abs_weightSum_le wAB wBC wAC) hT _ _ _ + -- Each of these primes is at least `√D/2`. + have hpow : (Real.sqrt D / 2) ^ divisors.card ≤ ∏ p ∈ divisors, (p : ℝ) := by + rw [← Finset.prod_const] + exact Finset.prod_le_prod₀ (fun _ _ => by linarith) fun p hp => (hmem p hp).2.1 + have hY : 0 < 3 * (n : ℝ) ^ κ := lt_of_lt_of_le (by positivity) (hpow.trans hprod) + rw [Real.le_logb_iff_rpow_le (by linarith) hY, Real.rpow_natCast] + exact hpow.trans hprod + +/-- 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 sum_falsePositiveCount_le (hD : 16 ≤ D) (hκ : 1 ≤ κ) (hT : WeightsBoundedBy wAB wBC wAC + ((n : ℝ) ^ κ)) : + ((∑ p ∈ primesInRange D, (falsePositiveCount wAB wBC wAC) p : ℕ) : ℝ) + ≤ (n : ℝ) ^ 3 * Real.logb (Real.sqrt D / 2) (3 * (n : ℝ) ^ κ) := by + classical + have hsqrt := four_le_sqrt hD + -- Count the pairs (prime, false positive of that prime) triple by triple. + have hswap : ∑ p ∈ primesInRange D, (falsePositiveCount wAB wBC wAC) p = ∑ t : Fin n × Fin n × + Fin n, + ((primesInRange D).filter fun p => IsFalsePositive wAB wBC wAC p t).card := by + simp only [falsePositiveCount, Finset.card_filter] + exact Finset.sum_comm + have hterm : ∀ t : Fin n × Fin n × Fin n, + (((primesInRange D).filter fun p => IsFalsePositive wAB wBC wAC p t).card : ℝ) + ≤ Real.logb (Real.sqrt D / 2) (3 * (n : ℝ) ^ κ) := by + intro t + by_cases ht : weightSum wAB wBC wAC t.1 t.2.1 t.2.2 = 0 + · -- A zero triangle is a false positive of no prime. + rw [Finset.filter_eq_empty_iff.2 fun p _ h => h.1 ht, Finset.card_empty, Nat.cast_zero] + have hn : (1 : ℝ) ≤ n := by exact_mod_cast Fin.pos t.1 + have hpow : (1 : ℝ) ≤ (n : ℝ) ^ κ := Real.one_le_rpow hn (by linarith) + exact Real.logb_nonneg (by linarith) (by linarith) + · -- Otherwise this is the bound of `card_falsePositive_primes_le` for this triple. + convert (card_falsePositive_primes_le wAB wBC wAC) hD hT t ht + rw [hswap, Nat.cast_sum] + calc ∑ t : Fin n × Fin n × Fin n, + (((primesInRange D).filter fun p => IsFalsePositive wAB wBC wAC p t).card : ℝ) + ≤ ∑ _t : Fin n × Fin n × Fin n, Real.logb (Real.sqrt D / 2) (3 * (n : ℝ) ^ κ) := + Finset.sum_le_sum fun t _ => hterm t + _ = (n : ℝ) ^ 3 * Real.logb (Real.sqrt D / 2) (3 * (n : ℝ) ^ κ) := by + rw [Finset.sum_const, Finset.card_univ, Fintype.card_prod, Fintype.card_prod, + Fintype.card_fin, nsmul_eq_mul] + push_cast + ring + +end Selection + +/-- There is a universal positive `c` such that every window with `D ≥ 16` contains at least `c * +sqrt D / log D` primes. The proof uses the all-window counting form of Bertrand’s postulate from +`PrimeWindow`, with no prime-number-theorem assumption. +-/ +theorem exists_le_card_primesInRange : + ∃ c : ℝ, 0 < c ∧ ∀ D : ℕ, 16 ≤ D → + c * (Real.sqrt D / Real.log D) ≤ ((primesInRange D).card : ℝ) := by + obtain ⟨c, hc, hcount⟩ := Nat.exists_forall_mul_sqrt_div_log_le_card_primes + exact ⟨c, hc, fun D hD => hcount D hD _ + fun _ hp hge hlt => mem_primesInRange.2 ⟨hp, hge, hlt⟩⟩ + +/-- 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 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 * (primesInRange D).card ≤ ∑ q ∈ primesInRange D, + (falsePositiveCount wAB wBC wAC) q := by + rw [mul_comm, ← smul_eq_mul] + exact Finset.card_nsmul_le_sum _ _ _ hp.falsePositiveCount_le + +/-- For `D ≥ 16`, compare `log D` with four times `log (sqrt D / 2)`. +-/ +theorem log_le_four_mul_log_sqrt_div_two (D : ℕ) (hD : 16 ≤ D) : + Real.log D ≤ 4 * Real.log (Real.sqrt D / 2) := by + have hD16 : (16 : ℝ) ≤ D := by exact_mod_cast hD + have hsqrt : 0 < Real.sqrt D := by linarith [four_le_sqrt hD] + -- `log(√D/2) = (log D)/2 - log 2`, and `4 log 2 = log 16 ≤ log D`. + have hlog16 : 4 * Real.log 2 ≤ Real.log D := by + have h := Real.log_le_log (by norm_num) (show (2 : ℝ) ^ 4 ≤ D by linarith) + rw [Real.log_pow] at h + exact_mod_cast h + rw [Real.log_div hsqrt.ne' (by norm_num), Real.log_sqrt (by linarith)] + linarith [hlog16] + +/-- 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 falsePositiveCount_le_of_le_card_primesInRange {n D p : ℕ} {κ c : ℝ} + (wAB wBC wAC : Fin n → Fin n → ℤ) (hc : 0 < c) + (hcard : c * (Real.sqrt D / Real.log D) ≤ ((primesInRange D).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 : ℝ) ^ κ) + / Real.sqrt D) := by + -- The quantities of the paper's sentence: `r = √D`, `Y = 3n^κ`, and the number of primes in the + -- range. + set r := Real.sqrt D + set Y := 3 * (n : ℝ) ^ κ with hY + set numPrimes := (primesInRange D).card + have hr : 4 ≤ r := four_le_sqrt hD + have hn : (16 : ℝ) ≤ n := by exact_mod_cast hD.trans hDn + have hlogD_pos : 0 < Real.log D := Real.log_pos (by exact_mod_cast (by omega : 1 < D)) + have hlogr_pos : 0 < Real.log (r / 2) := Real.log_pos (by linarith) + have hlogY_nonneg : 0 ≤ Real.log Y := by + have : 1 ≤ (n : ℝ) ^ κ := Real.one_le_rpow (by linarith) (by linarith) + exact Real.log_nonneg (by rw [hY]; linarith) + -- The selected prime is at most average, after multiplying by the number of primes. + -- False positives of all primes in the + -- range add up to at most `n³ log_{r/2} Y`. + have average : ((falsePositiveCount wAB wBC wAC) p : ℝ) * numPrimes ≤ (n : ℝ) ^ 3 * Real.logb + (r / 2) Y := + le_trans (by exact_mod_cast hp.falsePositiveCount_mul_card_le_sum) + ((sum_falsePositiveCount_le wAB wBC wAC) hD hκ hT) + -- The base of the logarithm changes: `log_{r/2} Y ≤ 4 log Y / log D`. + have hlogD_le : Real.log D ≤ 4 * Real.log (r / 2) := log_le_four_mul_log_sqrt_div_two D hD + have changeBase : Real.logb (r / 2) Y ≤ 4 * Real.log Y / Real.log D := by + rw [Real.logb, div_le_div_iff₀ hlogr_pos hlogD_pos] + linarith [mul_le_mul_of_nonneg_left hlogD_le hlogY_nonneg] + rw [show 4 / c * ((n : ℝ) ^ 3 * Real.log Y / r) = 4 * (n : ℝ) ^ 3 * Real.log Y / (c * r) by + field_simp, le_div_iff₀ (by positivity)] + calc ((falsePositiveCount wAB wBC wAC) p : ℝ) * (c * r) = (falsePositiveCount wAB wBC wAC) p * + (c * (r / Real.log D)) * Real.log D := by field_simp + _ ≤ (falsePositiveCount wAB wBC wAC) p * numPrimes * Real.log D := by gcongr + _ ≤ (n : ℝ) ^ 3 * Real.logb (r / 2) Y * Real.log D := by gcongr + _ ≤ (n : ℝ) ^ 3 * (4 * Real.log Y / Real.log D) * Real.log D := by gcongr + _ = 4 * (n : ℝ) ^ 3 * Real.log Y := by field_simp + +/-- 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. +-/ +theorem 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 / Real.sqrt + D) := by + obtain ⟨c, hc, hcard⟩ := exists_le_card_primesInRange + refine ⟨max 1 (8 / c), le_max_left _ _, fun {n D p κ} hD hDn hκ wAB wBC wAC hT hp => ?_⟩ + have hn : (16 : ℝ) ≤ n := by exact_mod_cast hD.trans hDn + have hlogn : 0 ≤ Real.log n := Real.log_nonneg (by linarith) + -- `log(3n^κ) = log 3 + κ log n ≤ 2κ log n`, because `3 ≤ n` and `κ ≥ 1`. + have hlog : Real.log (3 * (n : ℝ) ^ κ) ≤ 2 * κ * Real.log n := by + have hlog3 : Real.log 3 ≤ κ * Real.log n := + (Real.log_le_log (by norm_num) (by linarith)).trans (le_mul_of_one_le_left hlogn hκ) + rw [Real.log_mul (by norm_num) (by positivity), Real.log_rpow (by linarith)] + linarith [hlog3] + calc ((falsePositiveCount wAB wBC wAC) p : ℝ) ≤ 4 / c * ((n : ℝ) ^ 3 * Real.log (3 * (n : ℝ) ^ + κ) / Real.sqrt D) := + (falsePositiveCount_le_of_le_card_primesInRange wAB wBC wAC) hc (hcard D hD) hD hDn hκ hT hp + _ ≤ 4 / c * ((n : ℝ) ^ 3 * (2 * κ * Real.log n) / Real.sqrt D) := by gcongr + _ = 8 / c * (κ * (n : ℝ) ^ 3 * Real.log n / Real.sqrt D) := by ring + _ ≤ max 1 (8 / c) * (κ * (n : ℝ) ^ 3 * Real.log n / Real.sqrt D) := by + gcongr + exact le_max_right _ _ + +/-- 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. +-/ +noncomputable def Hashing.falsePositiveConst : ℝ := Classical.choose exists_falsePositiveCount_le + +/-- The universal false-positive constant `Hashing.falsePositiveConst` is at least one. +-/ +theorem Hashing.one_le_falsePositiveConst : 1 ≤ Hashing.falsePositiveConst := + (Classical.choose_spec exists_falsePositiveCount_le).1 + +/-- For `16 ≤ D ≤ n`, `κ ≥ 1` and edge weights bounded by `n^κ`, bound every selected prime’s +false-positive count by `Hashing.falsePositiveConst * κ * n^3 * log n / sqrt D`. +-/ +theorem Hashing.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 : ℝ) ≤ Hashing.falsePositiveConst * (κ * (n : ℝ) ^ 3 * + Real.log n / Real.sqrt D) := + (Classical.choose_spec exists_falsePositiveCount_le).2 hD hDn hκ wAB wBC wAC hT hp + +end Cslib.Algorithms.ExactTriangle diff --git a/Complexity/Algorithms/ExactTriangle/Weights.lean b/Complexity/Algorithms/ExactTriangle/Weights.lean new file mode 100644 index 0000000000..d358d0cd80 --- /dev/null +++ b/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 diff --git a/Complexity/Foundations/NumberTheory/PrimeWindow.lean b/Complexity/Foundations/NumberTheory/PrimeWindow.lean new file mode 100644 index 0000000000..9693a53028 --- /dev/null +++ b/Complexity/Foundations/NumberTheory/PrimeWindow.lean @@ -0,0 +1,344 @@ +/- +Copyright (c) 2020 Patrick Stevens, 2026 Anthropic, PBC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Patrick Stevens, Bolton Bailey, Anthropic, PBC +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Analysis.SpecialFunctions.Log.Base +public import Mathlib.Analysis.SpecialFunctions.Pow.Real +public import Mathlib.NumberTheory.PrimeCounting +import Mathlib.Analysis.Complex.ExponentialBounds +import Mathlib.Data.Nat.Prime.Factorial +import Mathlib.NumberTheory.Bertrand +import Mathlib.NumberTheory.Primorial +import Mathlib.Analysis.Convex.SpecificFunctions.Deriv + +/-! +# Explicit prime counts in a window of ratio two + +For every real `x ≥ 4`, the half-open window `[x/2, x)` contains at least `c * x / log x` primes +for one universal positive constant `c`. The proof counts prime factors of a central binomial +coefficient, so no prime-number-theorem hypothesis is assumed. + +## Main results + +* `Nat.exists_prime_half_le_and_lt`: a prime exists in every such window. +* `Nat.exists_forall_mul_div_log_le_card_primes`: the uniform counting bound. +* `Nat.exists_forall_mul_sqrt_div_log_le_card_primes`: the bound at `x = sqrt D`, for all `D ≥ + 16`. + +## References + +Adapted from [Anthropic's +PrimesInWindow.lean](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Util/PrimesInWindow.lean). +Its central-binomial and concavity estimates adapt `Mathlib/NumberTheory/Bertrand.lean`, +originally by Patrick Stevens and Bolton Bailey; that source credit is retained. +-/ + +@[expose] public section + +open Finset + +namespace Nat + +private theorem one_le_log_of_three_le {x : ℝ} (hx : 3 ≤ x) : 1 ≤ Real.log x := + (Real.le_log_iff_exp_le (by linarith)).2 (Real.exp_one_lt_three.le.trans hx) + +/-- The primes `p` with `n < p ≤ 2n`: the primes that Bertrand's postulate is about. -/ +private def bertrandPrimes (n : ℕ) : Finset ℕ := (Ioc n (2 * n)).filter Nat.Prime + +/-- Membership in `bertrandPrimes`, spelled out. -/ +private theorem mem_bertrandPrimes {n p : ℕ} : + p ∈ bertrandPrimes n ↔ (n < p ∧ p ≤ 2 * n) ∧ p.Prime := by + simp only [bertrandPrimes, mem_filter, mem_Ioc] + +/-! +## 1. Erdős's upper bound for the central binomial coefficient -/ + +/-- Every prime power in `C(2n, n)` is at most `2n`, so `|s|` of them multiply to at most +`(2n)^|s|`. +-/ +private theorem prod_pow_factorization_le {n : ℕ} (hn : 0 < n) (s : Finset ℕ) : + ∏ p ∈ s, p ^ n.centralBinom.factorization p ≤ (2 * n) ^ s.card := + prod_le_pow_card _ _ _ fun _ _ => Nat.pow_factorization_choose_le (by omega) + +/-- The primes in `(√(2n), n]` contribute at most `4^(2n/3)` to `C(2n, n)`: their exponent is at +most 1, it is 0 above `2n/3`, and the product of the primes up to `2n/3` is at most `4^(2n/3)`. +Adapted from Mathlib, Mathlib/NumberTheory/Bertrand.lean, Apache 2.0. +-/ +private theorem prod_middle_le {n : ℕ} (hn : 2 < n) (s : Finset ℕ) + (hs : ∀ p ∈ s, p.Prime ∧ Nat.sqrt (2 * n) < p ∧ p ≤ n) : + ∏ p ∈ s, p ^ n.centralBinom.factorization p ≤ 4 ^ (2 * n / 3) := + calc ∏ p ∈ s, p ^ n.centralBinom.factorization p + ≤ ∏ p ∈ s, (if p ≤ 2 * n / 3 then p else 1) := by + refine prod_le_prod fun p hp => ?_ + obtain ⟨hprime, hsqrt, hpn⟩ := hs p hp + split_ifs with h3 + · exact (pow_right_mono₀ hprime.one_lt.le + (Nat.factorization_choose_le_one (Nat.sqrt_lt'.mp hsqrt))).trans (pow_one p).le + · rw [Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul hn hpn (by omega), + pow_zero] + _ = ∏ p ∈ s.filter (· ≤ 2 * n / 3), p := (prod_filter _ _).symm + _ ≤ primorial (2 * n / 3) := by + refine prod_le_prod_of_subset_of_one_le (fun p hp => ?_) + fun p hp _ => (mem_filter.1 hp).2.one_lt.le + obtain ⟨hps, hp3⟩ := mem_filter.1 hp + exact mem_filter.2 ⟨mem_range.2 (by omega), (hs p hps).1⟩ + _ ≤ 4 ^ (2 * n / 3) := primorial_le_four_pow _ + +/-- Erdős's bound, keeping the primes of `(n, 2n]`: `C(2n, n) ≤ (2n)^√(2n) · 4^(2n/3) · (2n)^k`, +where `k` is the number of primes in `(n, 2n]`. Mathlib proves the case `k = 0` on the way to +Bertrand's postulate (`centralBinom_le_of_no_bertrand_prime`). Adapted from Mathlib, +Mathlib/NumberTheory/Bertrand.lean, Apache 2.0. +-/ +private theorem centralBinom_le (n : ℕ) (hn : 2 < n) : + n.centralBinom ≤ + (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ (2 * n / 3) * (2 * n) ^ (bertrandPrimes n).card := by + -- `C(2n, n)` is the product of its prime powers over the set `T` of the primes up to `2n`. + set T := (range (2 * n + 1)).filter Nat.Prime with hT + have hprod : ∏ p ∈ T, p ^ n.centralBinom.factorization p = n.centralBinom := + (prod_filter_of_ne fun p _ h => by + contrapose h + rw [Nat.factorization_eq_zero_of_not_prime _ h, pow_zero]).trans + n.prod_pow_factorization_centralBinom + -- Split the primes at `n`, and those up to `n` at `√(2n)`. + rw [← hprod, ← prod_filter_mul_prod_filter_not T (· ≤ n), + ← prod_filter_mul_prod_filter_not (T.filter (· ≤ n)) (· ≤ Nat.sqrt (2 * n))] + refine mul_le_mul' (mul_le_mul' ?_ ?_) ?_ + · -- There are at most `√(2n)` primes up to `√(2n)`. + have hsub : (T.filter (· ≤ n)).filter (· ≤ Nat.sqrt (2 * n)) ⊆ Icc 1 (Nat.sqrt (2 * n)) := by + intro p hp + simp only [hT, mem_filter, mem_range] at hp + obtain ⟨⟨⟨-, hprime⟩, -⟩, hsqrt⟩ := hp + exact mem_Icc.mpr ⟨hprime.one_lt.le, hsqrt⟩ + exact (prod_pow_factorization_le (by omega) _).trans (pow_right_mono₀ (by omega) + ((card_le_card hsub).trans_eq (by rw [Nat.card_Icc, Nat.add_sub_cancel]))) + · -- The primes in `(√(2n), n]`. + refine prod_middle_le hn _ fun p hp => ?_ + simp only [hT, mem_filter, mem_range, not_le] at hp + obtain ⟨⟨⟨-, hprime⟩, hpn⟩, hsqrt⟩ := hp + exact ⟨hprime, hsqrt, hpn⟩ + · -- The primes above `n` are those of `(n, 2n]`. + refine (prod_pow_factorization_le (by omega) _).trans + (pow_right_mono₀ (by omega) (card_le_card fun p hp => ?_)) + simp only [hT, mem_filter, mem_range] at hp + obtain ⟨⟨hp2n, hprime⟩, hnp⟩ := hp + exact mem_bertrandPrimes.2 ⟨⟨by omega, by omega⟩, hprime⟩ + +/-! +## 2. The elementary estimate `n^6 · (2n)^(6√(2n)) ≤ 2^n` for `n ≥ 16562` -/ + +/-- For `a ≥ 0` the function `log x + √(2x) · log (2x) - a x` is concave for `x > 1/2`. Adapted from +Mathlib, Mathlib/NumberTheory/Bertrand.lean, Apache 2.0 (there inside +`Bertrand.real_main_inequality`, for `a = log 4 / 3`). +-/ +private theorem concaveOn_log_add_sqrt_mul_log_sub (a : ℝ) (ha : 0 ≤ a) : + ConcaveOn ℝ (Set.Ioi (1 / 2 : ℝ)) + (fun x : ℝ => Real.log x + √(2 * x) * Real.log (2 * x) - a * x) := by + apply ConcaveOn.sub + · apply ConcaveOn.add + · exact strictConcaveOn_log_Ioi.concaveOn.subset + (Set.Ioi_subset_Ioi (by norm_num)) (convex_Ioi _) + · have h := strictConcaveOn_sqrt_mul_log_Ioi.concaveOn.comp_linearMap + ((2 : ℝ) • (LinearMap.id : ℝ →ₗ[ℝ] ℝ)) + have hset : (⇑((2 : ℝ) • (LinearMap.id : ℝ →ₗ[ℝ] ℝ))) ⁻¹' Set.Ioi 1 = Set.Ioi (1 / 2) := by + ext x + simp only [Set.mem_Ioi, Set.mem_preimage, LinearMap.smul_apply, LinearMap.id_coe, id_eq, + smul_eq_mul] + constructor <;> intro h <;> linarith + rw [hset] at h + exact h + · exact ConvexOn.smul ha (convexOn_id (convex_Ioi _)) + +/-- `log x + √(2x) · log (2x) ≤ (log 2 / 6) · x` for `x ≥ 16562`. The difference of the two sides +is concave, it is nonnegative at `x = 2` and nonpositive at `x = 16562 = 2 · 91²` (where `√(2x) += 182`; the only numerical input is `91^13 ≤ 2^85`), so it is nonpositive from there on. Adapted +from Mathlib, Mathlib/NumberTheory/Bertrand.lean, Apache 2.0 (the same argument proves +`Bertrand.real_main_inequality` there, with other numbers). +-/ +private theorem log_add_sqrt_mul_log_le {x : ℝ} (hx : 16562 ≤ x) : + Real.log x + √(2 * x) * Real.log (2 * x) ≤ Real.log 2 / 6 * x := by + have hlog2 : 0 < Real.log 2 := Real.log_pos (by norm_num) + have hat2 : (0 : ℝ) ≤ + Real.log 2 + √(2 * 2) * Real.log (2 * 2) - Real.log 2 / 6 * 2 := by + rw [Real.sqrt_mul_self (by norm_num), Real.log_mul (by norm_num) (by norm_num)] + linarith + have hat16562 : Real.log 16562 + √(2 * 16562) * Real.log (2 * 16562) + - Real.log 2 / 6 * 16562 ≤ 0 := by + have hlog91 : 13 * Real.log 91 ≤ 85 * Real.log 2 := by + have h := Real.log_le_log (by positivity) (show (91 : ℝ) ^ 13 ≤ 2 ^ 85 by norm_num) + rw [Real.log_pow, Real.log_pow] at h + exact_mod_cast h + have hlogx : Real.log 16562 = Real.log 2 + 2 * Real.log 91 := by + rw [show (16562 : ℝ) = 2 * 91 ^ 2 by norm_num, Real.log_mul (by norm_num) (by norm_num), + Real.log_pow] + norm_num + have hlog2x : Real.log (182 * 182) = 2 * Real.log 2 + 2 * Real.log 91 := by + rw [show (182 * 182 : ℝ) = 2 ^ 2 * 91 ^ 2 by norm_num, + Real.log_mul (by norm_num) (by norm_num), Real.log_pow, Real.log_pow] + norm_num + rw [show (2 * 16562 : ℝ) = 182 * 182 by norm_num, Real.sqrt_mul_self (by norm_num), hlogx, + hlog2x] + -- `366 log 91 ≤ 366 · (85/13) log 2 < (16562/6 - 365) log 2` + linarith only [hlog91, hlog2] + have hconcave := concaveOn_log_add_sqrt_mul_log_sub (Real.log 2 / 6) (by positivity) + have hatx := hconcave.right_le_of_le_left'' + (x := 2) (y := 16562) (z := x) (by norm_num [Set.mem_Ioi]) (by rw [Set.mem_Ioi]; linarith) + (by norm_num) hx (hat16562.trans hat2) + linarith only [hatx, hat16562] + +/-- The same estimate for natural numbers, without logarithms. -/ +private theorem pow_mul_pow_sqrt_le_two_pow {n : ℕ} (hn : 16562 ≤ n) : + n ^ 6 * (2 * n) ^ (6 * Nat.sqrt (2 * n)) ≤ 2 ^ n := by + have hx : (16562 : ℝ) ≤ n := by exact_mod_cast hn + have hreal := log_add_sqrt_mul_log_le hx + have hsqrt : (Nat.sqrt (2 * n) : ℝ) ≤ √(2 * n) := by + exact_mod_cast Real.nat_sqrt_le_real_sqrt (a := 2 * n) + have hlog : 0 ≤ Real.log (2 * n) := Real.log_nonneg (by linarith) + have hpos : (0 : ℝ) < n := by linarith + rw [← Nat.cast_le (α := ℝ)] + push_cast + rw [← Real.log_le_log_iff (by positivity) (by positivity), + Real.log_mul (by positivity) (by positivity), Real.log_pow, Real.log_pow, Real.log_pow] + push_cast + -- `6 log n + 6 ⌊√(2n)⌋ log(2n) ≤ 6 (log n + √(2n) log(2n)) ≤ n log 2` + linarith [hreal, mul_le_mul_of_nonneg_right hsqrt hlog] + +/-! +## 3. The count for `n ≥ 16562` -/ + +/-- `2^n ≤ (2n)^(2k)` for `n ≥ 16562`. If it failed, the sixth power of `4^n < n · (2n)^√(2n) · +4^(2n/3) · (2n)^k` would give `2^(12n) < (n^6 (2n)^(6√(2n))) · 2^(8n) · 2^(3n) ≤ 2^(12n)`. +-/ +private theorem two_pow_le_of_large {n : ℕ} (hn : 16562 ≤ n) : + 2 ^ n ≤ (2 * n) ^ (2 * (bertrandPrimes n).card) := by + by_contra hcon + have hfew : (2 * n) ^ (2 * (bertrandPrimes n).card) ≤ 2 ^ n := (not_le.mp hcon).le + have herdos : 4 ^ n < n * ((2 * n) ^ Nat.sqrt (2 * n) * 4 ^ (2 * n / 3) + * (2 * n) ^ (bertrandPrimes n).card) := + (Nat.four_pow_lt_mul_centralBinom n (by omega)).trans_le + (Nat.mul_le_mul_left _ (centralBinom_le n (by omega))) + have hsmall := pow_mul_pow_sqrt_le_two_pow hn + have hmiddle : 4 ^ (6 * (2 * n / 3)) ≤ 4 ^ (4 * n) := + Nat.pow_le_pow_right (by norm_num) (by omega) + refine lt_irrefl ((4 ^ n) ^ 6) ?_ + calc (4 ^ n) ^ 6 + < (n * ((2 * n) ^ Nat.sqrt (2 * n) * 4 ^ (2 * n / 3) + * (2 * n) ^ (bertrandPrimes n).card)) ^ 6 := Nat.pow_lt_pow_left herdos (by norm_num) + _ = (n ^ 6 * (2 * n) ^ (6 * Nat.sqrt (2 * n))) * 4 ^ (6 * (2 * n / 3)) + * ((2 * n) ^ (2 * (bertrandPrimes n).card)) ^ 3 := by ring + _ ≤ 2 ^ n * 4 ^ (4 * n) * (2 ^ n) ^ 3 := by gcongr + _ = (4 ^ n) ^ 6 := by + rw [mul_comm 4 n, pow_mul 4 n 4, show (4 : ℕ) ^ n = 2 ^ n * 2 ^ n by rw [← mul_pow]; rfl] + ring + +/-- The count of step 3 with natural logarithms: `n log 2 ≤ 2 k log (2n)`. -/ +private theorem mul_log_two_le_card_bertrandPrimes_mul_log {n : ℕ} (hn : 16562 ≤ n) : + (n : ℝ) * Real.log 2 ≤ 2 * (bertrandPrimes n).card * Real.log (2 * n) := by + have hpow : (2 : ℝ) ^ n ≤ (2 * (n : ℝ)) ^ (2 * (bertrandPrimes n).card) := by + exact_mod_cast two_pow_le_of_large hn + have hlog := Real.log_le_log (by positivity) hpow + rw [Real.log_pow, Real.log_pow] at hlog + exact_mod_cast hlog + +/-! +## 4. Half-open windows `[x/2, x)` with real endpoints -/ + +/-- For a real `x ≥ 4` the natural number `n = ⌈x/2⌉ - 1`, written below as `(⌈x⌉ - 1) / 2`, +satisfies `n ≥ 1`, `n ≥ x/4` and `2n < x`, and every natural number in `(n, 2n]` lies in `[x/2, +x)`. +-/ +private theorem exists_nat_window {x : ℝ} (hx : 4 ≤ x) : + ∃ n : ℕ, 1 ≤ n ∧ x / 4 ≤ (n : ℝ) ∧ 2 * (n : ℝ) < x ∧ + ∀ p : ℕ, n < p → p ≤ 2 * n → x / 2 ≤ (p : ℝ) ∧ (p : ℝ) < x := by + have hle : x ≤ (⌈x⌉₊ : ℝ) := Nat.le_ceil x + have hlt : (⌈x⌉₊ : ℝ) < x + 1 := Nat.ceil_lt_add_one (by linarith) + have hceil : 4 ≤ ⌈x⌉₊ := by exact_mod_cast hx.trans hle + obtain ⟨n, hn⟩ : ∃ n, n = (⌈x⌉₊ - 1) / 2 := ⟨_, rfl⟩ + have hlow : (⌈x⌉₊ : ℝ) ≤ 2 * n + 2 := by exact_mod_cast (by omega : ⌈x⌉₊ ≤ 2 * n + 2) + have hhigh : (2 * n + 1 : ℝ) ≤ (⌈x⌉₊ : ℝ) := by exact_mod_cast (by omega : 2 * n + 1 ≤ ⌈x⌉₊) + refine ⟨n, by omega, by linarith, by linarith, fun p hnp hp2n => ?_⟩ + have hnp' : (n : ℝ) + 1 ≤ p := by exact_mod_cast hnp + have hp2n' : (p : ℝ) ≤ 2 * n := by exact_mod_cast hp2n + exact ⟨by linarith, by linarith⟩ + +/-- For every real `x ≥ 4` there is a prime `p` with `x/2 ≤ p < x`, by Bertrand's postulate. -/ +theorem exists_prime_half_le_and_lt (x : ℝ) (hx : 4 ≤ x) : + ∃ p : ℕ, p.Prime ∧ x / 2 ≤ (p : ℝ) ∧ (p : ℝ) < x := by + obtain ⟨n, hn1, -, -, hwindow⟩ := exists_nat_window hx + obtain ⟨p, hprime, hnp, hp2n⟩ := Nat.exists_prime_lt_and_le_two_mul n (by omega) + exact ⟨p, hprime, hwindow p hnp hp2n⟩ + +/-- If `(n, 2n]` lies in the window and `n ≥ x/4` is large, the window has at least `x / (12 log x)` +primes: `(x/4) log 2 ≤ n log 2 ≤ 2 k log (2n) ≤ 2 k log x`, and `log 2 ≥ 2/3`. +-/ +private theorem div_log_le_card_of_large {x : ℝ} {n : ℕ} {S : Finset ℕ} (hx : 4 ≤ x) + (hn : 16562 ≤ n) (hn4 : x / 4 ≤ (n : ℝ)) (h2n : 2 * (n : ℝ) < x) (hsub : bertrandPrimes n ⊆ S) : + x / (12 * Real.log x) ≤ (S.card : ℝ) := by + have hcard : ((bertrandPrimes n).card : ℝ) ≤ S.card := by exact_mod_cast card_le_card hsub + have hn1 : (1 : ℝ) ≤ n := by exact_mod_cast (by omega : 1 ≤ n) + have hlog : Real.log (2 * n) ≤ Real.log x := Real.log_le_log (by linarith) h2n.le + have hlog0 : 0 ≤ Real.log (2 * n) := Real.log_nonneg (by linarith) + have hlog2 : 2 / 3 ≤ Real.log 2 := by linarith [Real.log_two_gt_d9] + rw [div_le_iff₀ (mul_pos (by norm_num) (Real.log_pos (by linarith)))] + calc x = 6 * (x / 4 * (2 / 3)) := by ring + _ ≤ 6 * (n * Real.log 2) := by gcongr + _ ≤ 6 * (2 * (bertrandPrimes n).card * Real.log (2 * n)) := + mul_le_mul_of_nonneg_left (mul_log_two_le_card_bertrandPrimes_mul_log hn) (by norm_num) + _ ≤ 6 * (2 * S.card * Real.log x) := by gcongr + _ = S.card * (12 * Real.log x) := by ring + +/-- There is a `c > 0` such that, for every real `x ≥ 4`, every finite set of natural numbers that +contains all primes `p` with `x/2 ≤ p < x` has at least `c · x / log x` elements. (This form +applies to the set of those primes however it is written down.) +-/ +theorem exists_forall_mul_div_log_le_card_primes : + ∃ c : ℝ, 0 < c ∧ ∀ x : ℝ, 4 ≤ x → ∀ S : Finset ℕ, + (∀ p : ℕ, p.Prime → x / 2 ≤ (p : ℝ) → (p : ℝ) < x → p ∈ S) → + c * (x / Real.log x) ≤ (S.card : ℝ) := by + -- `66248 = 4 · 16562`: for `x` below it one prime is enough + refine ⟨1 / 66248, by norm_num, fun x hx S hS => ?_⟩ + obtain ⟨n, hn1, hn4, h2n, hwindow⟩ := exists_nat_window hx + have hlogx : 1 ≤ Real.log x := one_le_log_of_three_le (by linarith) + rcases le_or_gt 16562 n with hlarge | hsmall + · -- The primes of `(n, 2n]` lie in the window. + have hsub : bertrandPrimes n ⊆ S := fun p hp => by + obtain ⟨⟨hnp, hp2n⟩, hprime⟩ := mem_bertrandPrimes.1 hp + exact hS p hprime (hwindow p hnp hp2n).1 (hwindow p hnp hp2n).2 + calc 1 / 66248 * (x / Real.log x) ≤ 1 / 12 * (x / Real.log x) := by gcongr; norm_num + _ = x / (12 * Real.log x) := by field_simp + _ ≤ (S.card : ℝ) := div_log_le_card_of_large hx hlarge hn4 h2n hsub + · -- Here `x ≤ 4n < 66248`, and one prime is enough. + obtain ⟨p, hprime, hlow, hhigh⟩ := exists_prime_half_le_and_lt x hx + have hone : (1 : ℝ) ≤ S.card := by + exact_mod_cast Finset.card_pos.mpr ⟨p, hS p hprime hlow hhigh⟩ + have hn : (n : ℝ) ≤ 16562 := by exact_mod_cast hsmall.le + calc 1 / 66248 * (x / Real.log x) ≤ 1 / 66248 * (x / 1) := by gcongr + _ ≤ 1 := by linarith + _ ≤ (S.card : ℝ) := hone + +/-! +## 5. The window `[√D/2, √D)` used in the modular reduction -/ + +/-- There is a `c > 0` such that, for every natural number `D ≥ 16`, every finite set of natural +numbers that contains all primes `p` with `√D/2 ≤ p < √D` has at least `c · √D / log D` +elements. +-/ +theorem exists_forall_mul_sqrt_div_log_le_card_primes : + ∃ c : ℝ, 0 < c ∧ ∀ D : ℕ, 16 ≤ D → ∀ S : Finset ℕ, + (∀ p : ℕ, p.Prime → √D / 2 ≤ (p : ℝ) → (p : ℝ) < √D → p ∈ S) → + c * (√D / Real.log D) ≤ (S.card : ℝ) := by + obtain ⟨c, hc, hcount⟩ := exists_forall_mul_div_log_le_card_primes + refine ⟨c, hc, fun D hD S hS => ?_⟩ + have hlog : 0 < Real.log D := Real.log_pos (by exact_mod_cast (by omega : 1 < D)) + calc c * (√D / Real.log D) ≤ c * (√D / (Real.log D / 2)) := by + gcongr + linarith + _ = c * (√D / Real.log (√D)) := by rw [Real.log_sqrt (Nat.cast_nonneg D)] + _ ≤ (S.card : ℝ) := hcount _ ((Real.le_sqrt_of_sq_le (by norm_num; exact_mod_cast hD))) S hS + +end Nat diff --git a/Complexity/Foundations/RingTheory/CyclicIntRing.lean b/Complexity/Foundations/RingTheory/CyclicIntRing.lean new file mode 100644 index 0000000000..d15f95b193 --- /dev/null +++ b/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 diff --git a/ComplexityTests/ExactTriangleHashing.lean b/ComplexityTests/ExactTriangleHashing.lean new file mode 100644 index 0000000000..41df09a874 --- /dev/null +++ b/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 diff --git a/NOTICE b/NOTICE index 3ab01a2df3..95b9c8d57a 100644 --- a/NOTICE +++ b/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. diff --git a/ROADMAP.md b/ROADMAP.md index 5dd6e55845..37981f88a8 100644 --- a/ROADMAP.md +++ b/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 diff --git a/UPSTREAM.md b/UPSTREAM.md index 87d9cb5288..30a7a8947f 100644 --- a/UPSTREAM.md +++ b/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 diff --git a/references.bib b/references.bib index 93c134807f..8ce53070a9 100644 --- a/references.bib +++ b/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},