#Lop-AE-SparseTri in time O(n² log²D / D^0.0703531 + w D^0.4296471 log D + nD + w) when D^1249 ≤ n^71

Proved

Light.Filter.claim_lopCountF

by xuanji · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

apsp-2996001apsp-exponentfine-grained-complexityword-ram

There are a constant $C$ and a time function $T(n,D,w)$ such that the counting version of Lop-AE-SparseTri (lopCountTask: given the $0/1$ biadjacency matrices of a lopsided graph with $n$ outer and $D$ inner vertices and $w$ query pairs $(a,b)$ , write for each pair the number of common neighbours) is solved in time $T$ (LopSolvedIn: by one program of the light language with a polynomially bounded need, with time at most $T(n,D,w')$ whenever $w\le w'$ ), and for all $n,D,w$ with $2\le D$ and $D^{1249}\le n^{71}$

T(n,D,w)\le C\Big(\frac{n^2\log^2D}{D^{0.0703531}}+wD^{0.4296471}\log D+nD+w+1\Big).

This is the thin product with pruned encodings at $c=21.2733$ , $\theta=0.111731$ (allInstancesF_programF), applied to the biadjacency matrices; $0.0703531<\Gamma$ and $0.4296471>q$ are the rounded exponents of Lemma 5.1.

Preamble

/-
Copyright (c) 2026 Anthropic, PBC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
SPDX-License-Identifier: Apache-2.0
-/
-- Generated by skeleton subtraction from the ThreeSumApsp library at commit 7c34437be804.

import Definitions.Def_APSP2996001_Defs2

set_option autoImplicit false
set_option relaxedAutoImplicit false

open ThreeSumApsp
open Light
open Light.Filter
open Light.Sec3 Light.Sec4

Formal statement

theorem Light.Filter.claim_lopCountF : ∃ (C : ℝ) (T : ℕ → ℕ → ℕ → ℝ), LopSolvedIn lopCountTask T ∧
    ∀ n D w : ℕ, 2 ≤ D → D ^ 1249 ≤ n ^ 71 →
      T n D w ≤ C * ((n : ℝ) ^ 2 * Real.log D ^ 2 / (D : ℝ) ^ (0.0703531 : ℝ)
        + (w : ℝ) * (D : ℝ) ^ (0.4296471 : ℝ) * Real.log D + (n : ℝ) * D + w + 1) := by sorry

Source

Developed for the prove2.me APSP exponent campaign (https://prove2.me/campaigns/apsp-exponent) on top of the Lean formalization anthropics/formal-math, folder 3sum-apsp, commit e1a4e65 (https://github.com/anthropics/formal-math/tree/e1a4e6508154ea59f030480661590a9fe3018011/3sum-apsp; Lean v4.33.1, Mathlib v4.33.1). The statement comes from the file 3sum-apsp/ThreeSumApsp/Filter/ThinLop.lean of the campaign's modified copy of that library, which is not published; the new definitions it uses are in the platform definition bundles APSP2996001_Defs1 and APSP2996001_Defs2 (and APSP299791_Defs1 to APSP299791_Defs5 of the 2.99791 entry). It follows the technical note "Deterministic APSP via thin products" (6 October 2026) refining J. Alman and V. Vassilevska Williams, "Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs", arXiv:2610.06783v1 (https://arxiv.org/abs/2610.06783v1), Lemma 5.1.

View graph