Round-six lemma `digL_split`

Proved

J6Seg.digL_split

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

complexity-theoryinteger-multiplicationkappa-improvement

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

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

theorem J6Seg.digL_split : ∀ (i : ℕ) (dims : List ℕ), (∀ u ∈ dims, 0 < u) → i < dims.length →
    ∀ b a c, b < (dims.take i).prod → a < dims.getD i 1 → c < (dims.drop (i + 1)).prod →
    ∀ m, digL dims (b * (dims.getD i 1 * (dims.drop (i + 1)).prod) +
        a * (dims.drop (i + 1)).prod + c) m =
      if m < i then digL (dims.take i) b m else if m = i then a
      else digL (dims.drop (i + 1)) c (m - i - 1)

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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_HvdH_Numeric
import Definitions.Def_IntMul_HvdH_ExpApprox
import Definitions.Def_IntMul_HvdH_RealExp
import Definitions.Def_IntMul_HvdH_Twiddle
import Definitions.Def_IntMul_HvdH_SApprox
import Definitions.Def_IntMul_HvdH_DiagApprox
import Definitions.Def_IntMul_HvdH_EApprox
import Definitions.Def_IntMul_HvdH_JApprox
import Definitions.Def_IntMul_HvdH_BApprox
import Definitions.Def_IntMul_HvdH_FPApprox
import Definitions.Def_IntMul_HvdH_MachineRef

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul.HvdH IntMul.HvdH.Ref NLogN.KFM NLogN.KFY

Formal statement

theorem J6Seg.digL_split : ∀ (i : ℕ) (dims : List ℕ), (∀ u ∈ dims, 0 < u) → i < dims.length →
    ∀ b a c, b < (dims.take i).prod → a < dims.getD i 1 → c < (dims.drop (i + 1)).prod →
    ∀ m, digL dims (b * (dims.getD i 1 * (dims.drop (i + 1)).prod) +
        a * (dims.drop (i + 1)).prod + c) m =
      if m < i then digL (dims.take i) b m else if m = i then a
      else digL (dims.drop (i + 1)) c (m - i - 1) := 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.digL_split`, Solutions/J6SegSw1.lean (lines 35–105) of the round-six development.

View graph