The in-place axis map on a box function (round six, `axisL_listOf`)

Proved

J6Seg.axisL_listOf

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

complexity-theoryinteger-multiplicationkappa-improvement

The in-place axis map on a box function.

The following holds (Lean statement, in the scope of module Solutions.J6SegSw1):

theorem J6Seg.axisL_listOf (dims : List ℕ) (hpos : ∀ u ∈ dims, 0 < u) (i : ℕ) (hi : i < dims.length)
    {n post pre : ℕ} (hn : dims.getD i 1 = n) (hp : (dims.drop (i + 1)).prod = post)
    (hpr : (dims.take i).prod = pre) (A : (ℕ → α) → ℕ → α)
    (hloc : ∀ U U' : ℕ → α, (∀ k < n, U k = U' k) → A U = A U') (g : (ℕ → ℕ) → α) :
    axisL n post (fun X => (List.range n).map (A fun k => X.getD k default)) (listOf dims g) =
      listOf dims (fun j => A (fun k => g (Function.update j i k)) (j i))

Context. B-line machine, sweep 1: in-place axis maps

The machine keeps the array in its row-major layout and applies the line map of axis i in place (no axis rotation). For a box dims and an axis i, the array is (pre, n, post) (pre = ∏_{j<i}, n = dims_i, post = ∏_{j>i}), and

axisL n post f L: every (n, post) block is transposed, f is applied to each of its post lines, and the block is transposed back;
axisL_getD: entry b (n·post) + a·post + c of axisL n post f L is entry a of f applied to the line k ↦ L[b (n·post) + k·post + c];
digL_split: the row-major digits of b (n·post) + a·post + c;
axisL_listOf: on listOf dims g, axisL is the slice map j ↦ A (k ↦ g (j[i ↦ k])) (j i).

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).

Preamble

-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_R6_Defs62

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg
open IntMul.HvdH IntMul.HvdH.Ref NLogN.KFM NLogN.KFY
variable {α : Type*} [Inhabited α]

Formal statement

theorem J6Seg.axisL_listOf (dims : List ℕ) (hpos : ∀ u ∈ dims, 0 < u) (i : ℕ) (hi : i < dims.length)
    {n post pre : ℕ} (hn : dims.getD i 1 = n) (hp : (dims.drop (i + 1)).prod = post)
    (hpr : (dims.take i).prod = pre) (A : (ℕ → α) → ℕ → α)
    (hloc : ∀ U U' : ℕ → α, (∀ k < n, U k = U' k) → A U = A U') (g : (ℕ → ℕ) → α) :
    axisL n post (fun X => (List.range n).map (A fun k => X.getD k default)) (listOf dims g) =
      listOf dims (fun j => A (fun k => g (Function.update j i k)) (j i)) := by sorry

Source

S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean declaration `J6Seg.axisL_listOf`, Solutions/J6SegSw1.lean (lines 244–303) of the round-six development.

View graph