Integer algorithms before rounding the exponents

Lax350013.IntegerAlgorithmBounds · concepts/Lax350013/IntegerAlgorithmBounds.lean · lax-350013

proven

Loading review…

Natural Language Statement

Theorem

Theorem 19 gives Exact Triangle bounds from both constructions. Theorem 22 carries these improvements to 3SUM, min-plus product and APSP, retaining the logarithmic and $o(1)$ factors before rounding. These statements are deterministic integer word-RAM bounds; they do not assert the paper’s real-RAM or randomized bounds.

Concept map

8 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

This concept declares 5 statements. Each proof establishes one of them relative to its assumptions.

Lean source view on GitHub

Show types on hover

1	/-
2	Copyright (c) 2026 Anthropic, PBC. All rights reserved.
3	Released under Apache 2.0 license as described in the file LICENSE.
4	SPDX-License-Identifier: Apache-2.0
5	-/
6	/-
7	Modified for the independent Lax packaging by Édouard Bonnet, 2026.
8	Derived from 3sum-apsp/EndStatement.lean / PaperStatements.lean at upstream commit e1a4e6508154ea59f030480661590a9fe3018011.
9	Changes: Lax module/namespace layout, separated concepts and proofs, archive
10	annotations, and compatibility with the archive Lean/mathlib environment.
11	See NOTICE and README.md in the submission root for provenance and scope.
12	-/
13
14	import Mathlib.Algebra.MvPolynomial.Basic
15	import Mathlib.Analysis.SpecialFunctions.Log.Base
16	import Mathlib.Analysis.SpecialFunctions.Log.Basic
17	import Mathlib.Analysis.SpecialFunctions.Pow.Real
18	import Mathlib.Combinatorics.SimpleGraph.Basic
19	import Mathlib.Data.Finset.Sort
20	import Mathlib.LinearAlgebra.Matrix.Notation
21	import Mathlib.MeasureTheory.Integral.Bochner.Basic
22	import Mathlib.NumberTheory.PrimeCounting
23	import Mathlib.Probability.Independence.Basic
24	import Mathlib.Tactic.DeriveFintype
25	import Lax350013.ExactTriangle
26	import Lax350013.ThreeSUM
27	import Lax350013.MinPlusProduct
28	import Lax350013.APSP
29	import Lax350013.RAMResources
30
31	/-!
32	---
33	title: Integer algorithms before rounding the exponents
34	type: theorem
35	---
36	Theorem 19 gives Exact Triangle bounds from both constructions. Theorem 22 carries these improvements to 3SUM, min-plus product and APSP, retaining the logarithmic and $o(1)$ factors before rounding. These statements are deterministic integer word-RAM bounds; they do not assert the paper’s real-RAM or randomized bounds.
37	-/
38
39	namespace Lax350013.IntegerAlgorithmBounds
40
41	open Finset
42	open Lax350013.WordRAM
43	open Lax350013.RAMResources
44
45	/-- Theorem 19: "For every constant ν ≥ 1, Exact Triangle on n vertices per part with
46	integer weights of absolute value at most n^ν can be solved by a deterministic algorithm in
47	O(n^{3−1/648} log² n) time [...], and in O(n^{3−ε'} log n) ≤ O(n^{3−ε_T}) time", with `ε' = 0.00175`
48	and `ε_T = 0.0017`. (The paper reaches the first bound using Theorem 5 and the second using
49	Corollary 26. This cannot be said by "there is a program": as statements about the existence of
50	programs, the first and the third bound follow from the second, which is smaller.) -/
51	def Theorem_19 : Prop :=
52	SolvedInTime Lax350013.ExactTriangle.ExactTriangle (3 - 1 / 648) 2 ∧
53	SolvedInTime Lax350013.ExactTriangle.ExactTriangle (3 - 0.00175) 1 ∧
54	SolvedInTime Lax350013.ExactTriangle.ExactTriangle (3 - 0.0017) 0
55
56	/-- Theorem 22, the bounds "Using Theorem 5": 3SUM in `O(n^{1.99923})` time, "and the
57	(min,+)-product [...] as well as APSP [...] in Õ(n^{3−1/1944}) ≤ O(n^{2.99949}) time". (The
58	intermediate form `n^{2−1/1296+o(1)}` for 3SUM is `Theorem_22_threeSum` below. "Using Theorem 5"
59	cannot be said by "there is a program": as statements about the existence of programs, all five
60	bounds follow from those of `Theorem_22_second`, which are smaller.) -/
61	def Theorem_22_first : Prop :=
62	SolvedInTime Lax350013.ThreeSUM.ThreeSum 1.99923 0 ∧
63	SolvedInPolylogTime Lax350013.MinPlusProduct.MinPlusProduct (3 - 1 / 1944) ∧
64	SolvedInPolylogTime Lax350013.APSP.APSP (3 - 1 / 1944) ∧
65	SolvedInTime Lax350013.MinPlusProduct.MinPlusProduct 2.99949 0 ∧
66	SolvedInTime Lax350013.APSP.APSP 2.99949 0
67
68	/-- Theorem 22, the bounds "Using Corollary 26 instead": 3SUM in `O(n^{1.9992})` time,
69	the (min,+)-product and APSP in "Õ(n^{3−ε'/3}) ≤ O(n^{2.99942})" time, with
70	`ε' = 0.00175`. (The intermediate form `n^{2−ε'/2+o(1)}` for 3SUM is `Theorem_22_threeSum`
71	below.) -/
72	def Theorem_22_second : Prop :=
73	SolvedInTime Lax350013.ThreeSUM.ThreeSum 1.9992 0 ∧
74	SolvedInPolylogTime Lax350013.MinPlusProduct.MinPlusProduct (3 - 0.00175 / 3) ∧
75	SolvedInPolylogTime Lax350013.APSP.APSP (3 - 0.00175 / 3) ∧
76	SolvedInTime Lax350013.MinPlusProduct.MinPlusProduct 2.99942 0 ∧
77	SolvedInTime Lax350013.APSP.APSP 2.99942 0
78
79	/-- Theorem 22, the two bounds for 3SUM before rounding: "Using Theorem 5 (through
80	Theorem 19), deterministic algorithms solve 3SUM on n integers of absolute value at most n^ν in
81	n^{2−1/1296+o(1)} ≤ O(n^{1.99923}) time [...]. Using Corollary 26 instead, the times are
82	n^{2−ε'/2+o(1)} ≤ O(n^{1.9992}) [...]", with `ε' = 0.00175`. The rounded bounds are in
83	`Theorem_22_first` and `Theorem_22_second`. (As a statement about the existence of programs, the
84	first bound follows from the second, which is smaller.) -/
85	def Theorem_22_threeSum : Prop :=
86	SolvedInLittleOTime Lax350013.ThreeSUM.ThreeSum (2 - 1 / 1296) ∧
87	SolvedInLittleOTime Lax350013.ThreeSUM.ThreeSum (2 - 0.00175 / 2)
88
89	/-- Theorem 2, the deterministic half: "On a word RAM with O(log n)-bit words,
90	deterministic algorithms solve the following problems, where all numbers in the input are integers
91	of absolute value n^{O(1)}: Exact Triangle on n-vertex graphs in O(n^{2.9983}) time, APSP on
92	directed n-vertex graphs with no negative cycles in O(n^{2.9995}) time, the (min,+)-product of two
93	n × n matrices in O(n^{2.9995}) time, and 3SUM on n numbers in O(n^{1.9992}) time." (For APSP and
94	the (min,+)-product, Theorem 22 prints the smaller exponent 2.99942: `Theorem_22_second`.)
95
96	NOTE. Here Exact Triangle has the tripartite form of Section 3.2, with `n` vertices per part; for
97	`n`-vertex graphs see `Theorem_2_graphs`. -/
98	def Theorem_2 : Prop :=
99	SolvedInTime Lax350013.ExactTriangle.ExactTriangle 2.9983 0 ∧
100	SolvedInTime Lax350013.APSP.APSP 2.9995 0 ∧
101	SolvedInTime Lax350013.MinPlusProduct.MinPlusProduct 2.9995 0 ∧
102	SolvedInTime Lax350013.ThreeSUM.ThreeSum 1.9992 0
103
104	/-- Integer algorithms before rounding the exponents: Theorem 19. -/
105	axiom theorem19 : Theorem_19
106
107
108	/-- Integer algorithms before rounding the exponents: Theorem 22 first. -/
109	axiom theorem22_first : Theorem_22_first
110
111
112	/-- Integer algorithms before rounding the exponents: Theorem 22 second. -/
113	axiom theorem22_second : Theorem_22_second
114
115
116	/-- Integer algorithms before rounding the exponents: Theorem 22 threeSum. -/
117	axiom theorem22_threeSum : Theorem_22_threeSum
118
119
120	/-- Integer algorithms before rounding the exponents: Theorem 2. -/
121	axiom theorem2 : Theorem_2
122
123	end Lax350013.IntegerAlgorithmBounds
124

Show ProofShow ProofShow ProofShow ProofShow Proof

Builds on

Used by

none

From Mathlib

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Integer algorithms before rounding the exponents

Flags

Flag this concept

Natural Language Statement

Theorem

1 `theorem19` proven

2 `theorem2` proven

3 `theorem22_first` proven

4 `theorem22_second` proven

5 `theorem22_threeSum` proven

Lean source view on GitHub

Discussion

Settings