Explicit bound on the time of the batched counting oracle: oTimeF ≤ K · n^2.99556085

Proved

Light.Batch.oTimeF_le_of

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

apsp-2995561apsp-exponentfine-grained-complexityword-ram

Let $C_1,C_2,C_q,a_0,\kappa'\ge0$ be such that the preprocessing and query times of Theorem 30 (with pruned encodings) satisfy tPreCoreP cShared30 P t $\le C_1\,$ cost8p and tQueryAt $\le C_2\,$ costQuery under Hyp30, and the query cost at the parameters $c=20$ , $\theta=56569/500000$ is at most $C_q D(m)^{q}\log D(m)$ . Then for all $n,U,s,p$ with $1\le s\le n$ , $p\ge1$ , $\log n\ge20000$ , $|\log s-0.0336175\log n|\le\log 2$ , $\log p\le\log s+10^{-9}\log n$ and $\lfloor\log_2(U+1)\rfloor\le a_0+\kappa'\log n$ ,

\mathrm{oTimeF}(A,n,U,s,p)\le K_t(A,C_1,C_2,C_q,a_0,\kappa')\,e^{2.99556085\log n},

with the explicit constant Kt.

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 3b45b374640a.

import Definitions.Def_APSP2995561_Defs2

set_option autoImplicit false
set_option relaxedAutoImplicit false

open Filter
open Light
open Light.Batch
open ThreeSumApsp Light.Sec4
set_option maxHeartbeats 400000

Formal statement

theorem Light.Batch.oTimeF_le_of {A n U s p : ℕ} {C1 C2 Cq a0 κ' : ℝ} (hC1 : 0 ≤ C1) (hC2 : 0 ≤ C2)
    (hCq : 0 ≤ Cq) (ha0 : 0 ≤ a0) (hκ : 0 ≤ κ')
    (hpre : ∀ (P : Sec2.Par) (t : ℕ), Hyp30 P t →
      (tPreCoreP cShared30 P t : ℝ) ≤ C1 * cost8p P.L P.m t P.N)
    (hq : ∀ (P : Sec2.Par) (t : ℕ), Hyp30 P t →
      (tQueryAt P.L P.m t : ℝ) ≤ C2 * costQuery P.L P.m t)
    (hcq : ∀ m : ℕ, 1 ≤ m → costQuery (levelsOf 20 m) m (switchOf (56569 / 500000) m)
      ≤ Cq * ((ThreeSumApsp.D m : ℝ) ^ qOf (56569 / 500000) * Real.log (ThreeSumApsp.D m)))
    (hn : 1 ≤ n) (hs : 1 ≤ s) (hsn : s ≤ n) (hp : 1 ≤ p)
    (hν : 20000 ≤ Real.log n) (hx1 : 0.0336175 * Real.log n ≤ Real.log 2 + Real.log s)
    (hx2 : Real.log s ≤ Real.log 2 + 0.0336175 * Real.log n)
    (hy : Real.log p ≤ Real.log s + 0.000000001 * Real.log n)
    (hG : (Nat.log 2 (U + 1) : ℝ) ≤ a0 + κ' * Real.log n) :
    (oTimeF A n U s p : ℝ) ≤ Kt A C1 C2 Cq a0 κ' * Real.exp (2.99556085 * Real.log n) := 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/Batch/OBound.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 APSP2995561_Defs1 and APSP2995561_Defs2 (and APSP2996001_Defs1-2, APSP299791_Defs1-5 of the earlier entries). It follows the technical note "Deterministic APSP via thin products" (revised 7 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), Proposition 2.1 and Lemma 5.1 (the cost of a batched oracle call).

View graph