Correctness of the variant (round six, `l12v_correct`)

Proved

NLogN.KIL.l12v_correct

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

complexity-theoryinteger-multiplicationkappa-improvement

Correctness of the variant: it is the interchange of the two [2^u] fields.

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

theorem NLogN.KIL.l12v_correct {child : Oracle α} {d : α} {W m q Kp : ℕ}
    (hspec : OracleSpec child d W m q Kp) (hm : 2 ≤ m) (hW : 1 ≤ W) (ρ : ℕ)
    (Pre G Suf : Shape) {e u : ℕ} (he : e ≤ m ^ Kp) (hu : 2 ^ u ≤ q ^ e) (xs : List α) :
    l12v child W m q Kp ρ e u Pre G Suf d xs =
      pull (binShape Pre G Suf (2 ^ u)) (binShape Pre G Suf (2 ^ u))
        (swapPos Pre.length (Pre.length + 1 + G.length)) d xs

Context. KIL6: Lemma 12 as a uniform IL program — the list denotations

The IL program of KIL6 realises the Lemma 12 interchange with the following data flow (array model, AModelL12):

binary padding binShape … (2^u) → binShape … (q^e): two one-field paddings (padL, embed_binShape);
high swaps: r = min ρ e single-digit interchanges (highSwaps);
if n = e - r > 0, the middle part l12mid: the row field is the prefix Pre ++ [q]^r (volume vol Pre · q^r), padded to padRows W Kp (q^r) rows (padL); the Prop. 11 oracle runs on the pieces (runPieces … pieceLevels), with the gap G ++ [q]^r (the already interchanged high digits of the second chunk belong to the gap); the padding is scanned away (unpadL);
binary extraction (two unpadL).

Compared with AModelL12.l12q this variant needs no joining rotation: the interchanged high digits d⁺ simply stay inside the gap. l12v_correct proves that it is the interchange swapPos of the two [2^u] fields, from the same oracle specification OracleSpec.

The list functions padL / unpadL are the one-field embeddings / extractions in the chunk form the IL loops produce (embed_eq_padL, extract_eq_unpadL).

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.KIL
open AModel AModelL12
variable {α : Type*}

Formal statement

theorem NLogN.KIL.l12v_correct {child : Oracle α} {d : α} {W m q Kp : ℕ}
    (hspec : OracleSpec child d W m q Kp) (hm : 2 ≤ m) (hW : 1 ≤ W) (ρ : ℕ)
    (Pre G Suf : Shape) {e u : ℕ} (he : e ≤ m ^ Kp) (hu : 2 ^ u ≤ q ^ e) (xs : List α) :
    l12v child W m q Kp ρ e u Pre G Suf d xs =
      pull (binShape Pre G Suf (2 ^ u)) (binShape Pre G Suf (2 ^ u))
        (swapPos Pre.length (Pre.length + 1 + G.length)) d 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 `NLogN.KIL.l12v_correct`, Solutions/KIL6Den.lean (lines 401–448) of the round-six development.

View graph