The batched band-array procedure fills the right input array of a band

Proved

Light.Batch.bandArrayBR_entry

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

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

In every program $P$ whose procedure number pBandArray is bandArrayBBody, under the standard limits (Std lim), the procedure meets BandArrayBRSpec lim P cBandArray: as bandArrayBL_entry, for the right side, whose source is the transpose of a $D\times K_0N$ matrix $Y$ : the call writes the right input array of the band $\beta$ in the batched layout within the cost bound with constant cBandArray.

The batched layout (Batch/Tiling): the source of the left side is a $K_0N\times D$ matrix $X$ (row by row), that of the right side a $D\times K_0N$ matrix $Y$ (stored transposed); the slot $(g,h)$ of the band $\beta$ holds the row block number $(\beta K_0+g)K_0+h$ of the source, so one run of Theorem 30's data structure computes $K_0^2$ independent block products.

Meets lim P p d args μ T Q means: the call of procedure $p$ of $P$ at depth $d$ with the arguments args on memory $\mu$ returns within $T$ steps, under the limits lim, with a result $r$ and memory $\mu'$ satisfying $Q\,r\,\mu'$ .

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 ThreeSumApsp
open Light
open Light.Batch
open Light.Sec2 Light.Sec2.Band
variable {lim : Limits} {P : Program} {d : ℕ} {A : BandArgs} {μ₀ μ : ℕ → ℤ} {T : List ℤ}

Formal statement

theorem Light.Batch.bandArrayBR_entry (std : Std lim) (hP : P[pBandArray]? = some bandArrayBBody) :
    BandArrayBRSpec lim P cBandArray := 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/BandArrayB.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 (batched tensor slots).

View graph