One layout step (round six, `Dl_step`)

Proved

NLogN.KFU.Dl_step

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

complexity-theoryinteger-multiplicationkappa-improvement

One layout step.

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

theorem NLogN.KFU.Dl_step (mz : ℕ → ℕ) (bg : ℕ → Bool) {g : List ℕ → List ℕ} {σ : ℕ → ℕ} {n : ℕ}
    (hP : POp g σ n) (ax0 lay' : List ℕ) (hl : lay'.length = n) (hnd : (g lay').Nodup)
    (hF : Full bg ax0 (g lay')) {α : Type*} (xs : List α) (d : α) :
    pull ((g lay').map (asz mz)) (lay'.map (asz mz)) g d (Dl mz bg ax0 (g lay') xs d) =
      Dl mz bg ax0 lay' xs d

Context. KFU §3: labelled layouts for the axis reversal

Addresses of the working array are tracked through layouts: lists of atom labels (2j is the main part of axis j, of size mz j; 2j+1 is its extra bit, of size 2, present when bg j). An axis of size tz j = mz j · (2 if bg j) is the pair [mz j, 2] in row-major order.

Dl ax0 lay xs: the array xs (shape ax0.map tz) viewed in the layout lay.
POp g σ n: an address map g = permIdx σ on n digits, σ onto [0, n).
Dl_step: a program realizing pull (g lay').map asz → lay'.map asz by g turns Dl ax0 (g lay') into Dl ax0 lay'. swapPos and KIL.swapMid are POps.
Dl_layA: for the standard layout layA ax of an axis order ax, Dl is an ordinary pull onto ax.map tz.

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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFU
open AModel AModelL12

Formal statement

theorem NLogN.KFU.Dl_step (mz : ℕ → ℕ) (bg : ℕ → Bool) {g : List ℕ → List ℕ} {σ : ℕ → ℕ} {n : ℕ}
    (hP : POp g σ n) (ax0 lay' : List ℕ) (hl : lay'.length = n) (hnd : (g lay').Nodup)
    (hF : Full bg ax0 (g lay')) {α : Type*} (xs : List α) (d : α) :
    pull ((g lay').map (asz mz)) (lay'.map (asz mz)) g d (Dl mz bg ax0 (g lay') xs d) =
      Dl mz bg ax0 lay' xs d := 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 `NLogN.KFU.Dl_step`, Solutions/KFURevBase.lean (lines 161–201) of the round-six development.

View graph