Callable reductions between the algorithmic problems
Lax350013.AlgorithmReductions · concepts/Lax350013/AlgorithmReductions.lean · lax-350013
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Theorem 17 reduces Exact Triangle to lopsided triangle detection at the two parameter choices used in the paper. Theorem 21 transfers an Exact Triangle solver to 3SUM, min-plus products and APSP. Additional reductions turn selected matrix entries into triangle counts and detection, and split large query sets. All are proved transformations of callable programs. The callable versions also preserve memory and resource guarantees needed when these algorithms are used as subroutines.
Concept map
Evidence
This concept declares 8 statements. Each proof establishes one of them relative to its assumptions.
1 apspFromExactTriangle proven
2 exactTriangleViaCorollary26 proven
3 exactTriangleViaTheorem5 proven
4 minPlusFromExactTriangle proven
5 splitTriangleQueries proven
6 threeSumFromExactTriangle proven
7 triangleCountsFromMatrixProduct proven
8 triangleDetectionFromCounts proven
Lean source view on GitHub
| 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.CallableAlgorithms |
| 26 | |
| 27 | /-! |
| 28 | --- |
| 29 | title: Callable reductions between the algorithmic problems |
| 30 | type: theorem |
| 31 | --- |
| 32 | Theorem 17 reduces Exact Triangle to lopsided triangle detection at the two parameter choices used in the paper. Theorem 21 transfers an Exact Triangle solver to 3SUM, min-plus products and APSP. Additional reductions turn selected matrix entries into triangle counts and detection, and split large query sets. All are proved transformations of callable programs. The callable versions also preserve memory and resource guarantees needed when these algorithms are used as subroutines. |
| 33 | -/ |
| 34 | |
| 35 | namespace Lax350013.AlgorithmReductions |
| 36 | |
| 37 | open Finset |
| 38 | |
| 39 | /-- Callable contract proved by upstream `Light.Sec3.claim_theorem_17₅`. -/ |
| 40 | axiom exactTriangleViaTheorem5 : Lax350013.CallableAlgorithms.Claim.Theorem_17 Lax350013.CallableAlgorithms.lightModel Lax350013.CallableAlgorithms.strassen Lax350013.CallableAlgorithms.paramD₅ Lax350013.CallableAlgorithms.paramG₅ |
| 41 | |
| 42 | |
| 43 | /-- Callable contract proved by upstream `Light.Sec3.claim_theorem_17₂₆`. -/ |
| 44 | axiom exactTriangleViaCorollary26 : Lax350013.CallableAlgorithms.Claim.Theorem_17 Lax350013.CallableAlgorithms.lightModel Lax350013.CallableAlgorithms.strassen Lax350013.CallableAlgorithms.paramD₂₆ Lax350013.CallableAlgorithms.paramG₂₆ |
| 45 | |
| 46 | |
| 47 | /-- Callable contract proved by upstream `Light.Sec3.claim_theorem_21a`. -/ |
| 48 | axiom threeSumFromExactTriangle : Lax350013.CallableAlgorithms.Claim.Theorem_21a Lax350013.CallableAlgorithms.lightModel |
| 49 | |
| 50 | |
| 51 | /-- Callable contract proved by upstream `Light.Sec3.claim_theorem_21b_minPlus`. -/ |
| 52 | axiom minPlusFromExactTriangle : Lax350013.CallableAlgorithms.Claim.Theorem_21b_minPlus Lax350013.CallableAlgorithms.lightModel |
| 53 | |
| 54 | |
| 55 | /-- Callable contract proved by upstream `Light.Sec3.claim_theorem_21b_apsp`. -/ |
| 56 | axiom apspFromExactTriangle : Lax350013.CallableAlgorithms.Claim.Theorem_21b_apsp Lax350013.CallableAlgorithms.lightModel |
| 57 | |
| 58 | |
| 59 | /-- Callable contract proved by upstream `Light.Sec3.claim_lopCountFromThinProduct`. -/ |
| 60 | axiom triangleCountsFromMatrixProduct : Lax350013.CallableAlgorithms.Claim.LopCountFromThinProduct Lax350013.CallableAlgorithms.lightModel |
| 61 | |
| 62 | |
| 63 | /-- Callable contract proved by upstream `Light.Sec3.claim_lopDetectFromCount`. -/ |
| 64 | axiom triangleDetectionFromCounts : Lax350013.CallableAlgorithms.Claim.LopDetectFromCount Lax350013.CallableAlgorithms.lightModel |
| 65 | |
| 66 | |
| 67 | /-- Callable contract proved by upstream `Light.Sec3.claim_lopSplit`. -/ |
| 68 | axiom splitTriangleQueries : Lax350013.CallableAlgorithms.Claim.LopSplit Lax350013.CallableAlgorithms.lightModel |
| 69 | |
| 70 | end Lax350013.AlgorithmReductions |
| 71 |
Builds on
Used by
none
From Mathlib
Mathlib.Algebra.MvPolynomial.BasicMathlib.Analysis.SpecialFunctions.Log.BaseMathlib.Analysis.SpecialFunctions.Log.BasicMathlib.Analysis.SpecialFunctions.Pow.RealMathlib.Combinatorics.SimpleGraph.BasicMathlib.Data.Finset.SortMathlib.LinearAlgebra.Matrix.NotationMathlib.MeasureTheory.Integral.Bochner.BasicMathlib.NumberTheory.PrimeCountingMathlib.Probability.Independence.BasicMathlib.Tactic.DeriveFintype
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments