The backward states (round six, `bwdS_eq`)

Proved

J6Seg.JK.bwdS_eq

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

complexity-theoryinteger-multiplicationkappa-improvement

The backward states.

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

theorem J6Seg.JK.bwdS_eq (hsort : L.Pairwise (· < ·)) (Y : ℕ → ℤ) : ∀ j ≤ L.length,
    bwdS P (bsOf P L mw c A) (accF (P := P) (S := bandS mw c) (L := L) (A := A) (b := Y)
      L.length) j =
      (accZ P (bandS mw c) L A Y (L.length - j),
        accB P (bandS mw c) L A Y (flOf L (c ≤ ·)) (L.length - j))

Context. J kernel precondition (JPre), part 4: the intermediates of the kernel in closed form

For the streams fsOf/bsOf of a sorted line L (pattern bandS mw c, border c ≤ ·) and an input v (|L| ≤ |v|), with the right-hand side bv L v (bv (L_r) = v_r):

fA_eq: the forward accumulator after r rows is accF r = [bt_{r-1}, …, bt_0];
bwdS_eq: the backward state after j records is (accZ (m-j), accB (m-j)) (the solution values z_{m-j}, …, z_{m-1} and their border part);
the shapes of the streams (fsOf_getElem_length, bsOf_getElem, WbOf_le, czOf_length, flOf_01).

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_R6_Defs66

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.JK
open Finset
variable {P : ℕ} {L : List ℕ} {mw c : ℕ} {A : ℕ → ℕ → ℤ}

Formal statement

theorem J6Seg.JK.bwdS_eq (hsort : L.Pairwise (· < ·)) (Y : ℕ → ℤ) : ∀ j ≤ L.length,
    bwdS P (bsOf P L mw c A) (accF (P := P) (S := bandS mw c) (L := L) (A := A) (b := Y)
      L.length) j =
      (accZ P (bandS mw c) L A Y (L.length - j),
        accB P (bandS mw c) L A Y (flOf L (c ≤ ·)) (L.length - j)) := 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.JK.bwdS_eq`, Solutions/J6SegJPre4.lean (lines 104–145) of the round-six development.

View graph