Chunk bridge (round six, `chunk_bridge`)

Proved

GlueLayout.chunk_bridge

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

complexity-theoryinteger-multiplicationkappa-improvement

Chunk bridge. On a binary address of length n = A + DK + B, selected bits at the positions A + iK + (K-1-ρ) (bit ρ of the i-th K-bit chunk after a prefix of A bits) act exactly as layerSel (2^A) K D (2^B) ρ of §5 for every tensor kernel.

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

theorem GlueLayout.chunk_bridge (hρ : ρ < K) {n : ℕ} (hn : n = A + D * K + B) {ι : Type*} [Fintype ι]
    [DecidableEq ι] (P : PosData n ι) (e : ι ≃ Fin D)
    (hpos : ∀ i : Fin D, P.pos (e.symm i) = A + i * K + (K - 1 - ρ)) (M : M2)
    {X : Type*} [AddCommMonoid X] [Module ℂ X] (xs : List X) :
    selOp (posSel P) (tens M) xs = selOp (layerSel (2 ^ A) K D (2 ^ B) ρ hρ) (tens M) xs

Context. Glue 2a: the paper's layout as a CoordLayout, its selected bits, and the bridge to layerSel

§0 bit arithmetic: getBit_bitsum, bitsum_update (binary digit sums), getD_decode (a digit of decode), getD_decode_binSh (bits of a binary address).
§1 PosData/posSel: selected bits of a binary address given by bit positions; selOp_transport: two selected-bit structures related by an address map preserving the linear index give the same selOp for every tensor kernel.
§2 slotLayout: a slot arrangement arr (a list of slot names nm i h covering every slot h < a i exactly once) is a CoordLayout (binSh |arr|) a; slotSel (round h, axes P) is SelCompat with it (slot_compat).
§3 chunk_bridge: if the selected positions are A + iK + (K-1-ρ) in a binary address of length A + DK + B, the selected-bit operator is layerSel (2^A) K D (2^B) ρ of §5.
§4 the paper's layout tgtL (SynthLayoutPaper): paperLayout, paperSel, synth_forward_paper (§6.1 on the concrete layout: the rounds implement B F^-), and paper_round_layer (for every slot b ≤ h < b + qK the round's simultaneous layer is exactly Proposition 14's layerH (2^A) K D (2^B) ρ with ρ = (h-b) mod K, via tgt_slot).

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 GlueLayout
open Finset Butterfly AModel Synth
variable {n : ℕ} {ι : Type*} [Fintype ι] [DecidableEq ι]
variable {A K D B ρ : ℕ}

Formal statement

theorem GlueLayout.chunk_bridge (hρ : ρ < K) {n : ℕ} (hn : n = A + D * K + B) {ι : Type*} [Fintype ι]
    [DecidableEq ι] (P : PosData n ι) (e : ι ≃ Fin D)
    (hpos : ∀ i : Fin D, P.pos (e.symm i) = A + i * K + (K - 1 - ρ)) (M : M2)
    {X : Type*} [AddCommMonoid X] [Module ℂ X] (xs : List X) :
    selOp (posSel P) (tens M) xs = selOp (layerSel (2 ^ A) K D (2 ^ B) ρ hρ) (tens M) xs := 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 `GlueLayout.chunk_bridge`, Solutions/GlueLayout.lean (lines 542–637) of the round-six development.

View graph