The merged digits of the standard layout (round six, `enc_layA`)

Proved

NLogN.KFU.enc_layA

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

complexity-theoryinteger-multiplicationkappa-improvement

The merged digits of the standard layout.

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

theorem NLogN.KFU.enc_layA : ∀ (ax : List ℕ), ax.Nodup → (∀ j ∈ ax, 1 ≤ mz j) → ∀ b : List ℕ,
    Valid ((layA bg ax).map (asz mz)) b →
    Valid (ax.map (tz mz bg)) (ax.map (dig bg (layA bg ax) b)) ∧
      encode (ax.map (tz mz bg)) (ax.map (dig bg (layA bg ax) b)) =
        encode ((layA bg ax).map (asz mz)) b

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
variable (mz : ℕ → ℕ) (bg : ℕ → Bool)

Formal statement

theorem NLogN.KFU.enc_layA : ∀ (ax : List ℕ), ax.Nodup → (∀ j ∈ ax, 1 ≤ mz j) → ∀ b : List ℕ,
    Valid ((layA bg ax).map (asz mz)) b →
    Valid (ax.map (tz mz bg)) (ax.map (dig bg (layA bg ax) b)) ∧
      encode (ax.map (tz mz bg)) (ax.map (dig bg (layA bg ax) b)) =
        encode ((layA bg ax).map (asz mz)) b := 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.enc_layA`, Solutions/KFURevBase.lean (lines 262–354) of the round-six development.

View graph