Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Faster lopsided triangle algorithms

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

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Corollary 16 solves counting and detection in O(∣W∣D0.437+N2/D0.063)O(|W|D^{0.437}+N^2/D^{0.063}) time for 1≤D1\leq D and D18≤ND^{18}\leq N. Corollary 15 records the earlier logarithmic bound for powers of four.

    Concept map
    6 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 corollary15 proven

    2 corollary16 proven

    Lean source view on GitHub

    1/-
    2Copyright (c) 2026 Anthropic, PBC. All rights reserved.
    3Released under Apache 2.0 license as described in the file LICENSE.
    4SPDX-License-Identifier: Apache-2.0
    5-/
    6/-
    7Modified for the independent Lax packaging by Édouard Bonnet, 2026.
    8Derived from 3sum-apsp/EndStatement.lean / PaperStatements.lean at upstream commit e1a4e6508154ea59f030480661590a9fe3018011.
    9Changes: Lax module/namespace layout, separated concepts and proofs, archive
    10annotations, and compatibility with the archive Lean/mathlib environment.
    11See NOTICE and README.md in the submission root for provenance and scope.
    12-/
    13
    14import Mathlib.Algebra.MvPolynomial.Basic
    15import Mathlib.Analysis.SpecialFunctions.Log.Base
    16import Mathlib.Analysis.SpecialFunctions.Log.Basic
    17import Mathlib.Analysis.SpecialFunctions.Pow.Real
    18import Mathlib.Combinatorics.SimpleGraph.Basic
    19import Mathlib.Data.Finset.Sort
    20import Mathlib.LinearAlgebra.Matrix.Notation
    21import Mathlib.MeasureTheory.Integral.Bochner.Basic
    22import Mathlib.NumberTheory.PrimeCounting
    23import Mathlib.Probability.Independence.Basic
    24import Mathlib.Tactic.DeriveFintype
    25import Lax350013.LopsidedTriangles
    26
    27/-!
    28---
    29title: Faster lopsided triangle algorithms
    30type: theorem
    31---
    32Corollary 16 solves counting and detection in O(∣W∣D0.437+N2/D0.063)O(|W|D^{0.437}+N^2/D^{0.063}) time for 1≤D1\leq D and D18≤ND^{18}\leq N. Corollary 15 records the earlier logarithmic bound for powers of four.
    33-/
    34
    35namespace Lax350013.LopsidedTriangleAlgorithms
    36
    37open Finset
    38open Lax350013.WordRAM
    39open Lax350013.RAMResources
    40open Lax350013.ThinMatrices
    41open Lax350013.LopsidedTriangles
    42
    43/-- **Corollary 15**: "Let D ≥ 4 be a power of four with n ≥ D^18, and consider an instance
    44of #Lop-AE-SparseTri(n,D) or of Lop-AE-SparseTri(n,D) with |W| query pairs. If |W| ≤ n²/√D, then
    45the instance can be solved deterministically in O(n² log² D/D^{1/18}) time. In general, [...] in
    46time O((n² + |W|√D) log² D/D^{1/18})." The general bound contains the first one, since
    47`|W|√D ≤ n²` there. (As a statement about the existence of programs, this follows from
    48`Corollary_16`, whose bound is smaller; see the remark at `Theorem_5`.) -/
    49def Corollary_15 : Prop :=
    50 ∃ (Pc Pd : List Instr) (b : ℕ) (C : ℝ),
    51 Solves lopCount Pc b
    52 (fun x => x.ZeroOne ∧ x.U = 1 ∧ (∃ k : ℕ, x.D = 4 ^ k) ∧ 4 ≤ x.D ∧ x.D ^ 18 ≤ x.N)
    53 (fun x => C * (((x.N : ℝ) ^ 2 + (x.W.length : ℝ) * Real.sqrt x.D) * Real.log x.D ^ 2 /
    54 (x.D : ℝ) ^ (1 / 18 : ℝ))) ∧
    55 Solves lopDetect Pd b
    56 (fun x => x.ZeroOne ∧ x.U = 1 ∧ (∃ k : ℕ, x.D = 4 ^ k) ∧ 4 ≤ x.D ∧ x.D ^ 18 ≤ x.N)
    57 (fun x => C * (((x.N : ℝ) ^ 2 + (x.W.length : ℝ) * Real.sqrt x.D) * Real.log x.D ^ 2 /
    58 (x.D : ℝ) ^ (1 / 18 : ℝ)))
    59
    60/-- **Corollary 16**: "Let n ≥ D^18, and consider an instance of #Lop-AE-SparseTri(n,D) or
    61of Lop-AE-SparseTri(n,D) with |W| query pairs. It can be solved deterministically in O(|W|
    62D^{0.437} + n²/D^{0.063}) time."
    63
    64NOTE. The paper states no lower bound on `D`; `D ≥ 1` is assumed, as in `Corollary_26` below. -/
    65def Corollary_16 : Prop :=
    66 ∃ (Pc Pd : List Instr) (b : ℕ) (C : ℝ),
    67 Solves lopCount Pc b (fun x => x.ZeroOne ∧ x.U = 1 ∧ 1 ≤ x.D ∧ x.D ^ 18 ≤ x.N)
    68 (fun x => C * ((x.W.length : ℝ) * (x.D : ℝ) ^ (0.437 : ℝ) +
    69 (x.N : ℝ) ^ 2 / (x.D : ℝ) ^ (0.063 : ℝ))) ∧
    70 Solves lopDetect Pd b (fun x => x.ZeroOne ∧ x.U = 1 ∧ 1 ≤ x.D ∧ x.D ^ 18 ≤ x.N)
    71 (fun x => C * ((x.W.length : ℝ) * (x.D : ℝ) ^ (0.437 : ℝ) +
    72 (x.N : ℝ) ^ 2 / (x.D : ℝ) ^ (0.063 : ℝ)))
    73
    74/-- Faster lopsided triangle algorithms: Corollary 15. -/
    75axiom corollary15 : Corollary_15
    76
    77
    78/-- Faster lopsided triangle algorithms: Corollary 16. -/
    79axiom corollary16 : Corollary_16
    80
    81end Lax350013.LopsidedTriangleAlgorithms
    82
    Show 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…