One backward step (round six, `bwd_step`)

Proved

J6Seg.Src.bwd_step

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

complexity-theoryinteger-multiplicationkappa-improvement

One backward step.

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

theorem J6Seg.Src.bwd_step (s0 : IState HS) (G : Fin HS → List ℤ) {iW : Fin HS} (fW : Free iW)
    {s t lam w A : ℕ} {LW : List ℤ} (hGW : G iW = (w : ℤ) :: LW) (hs : 0 < s) (hsA : s ≤ 2 ^ A)
    (hwA : w ≤ 2 ^ A) (hA : 2 ≤ A) {k : ℕ} (hk : k < s) :
    Sp (bwdB iW) (encK s0 (update (bwS G s t lam w k) 43 [(s : ℤ) - k]))
      (encK s0 (update (bwS G s t lam w (k + 1)) 43 [(s : ℤ) - k])) (80 * uC A DD)

Context. B-line IL, source-table producers, part 4: ljP, the backward pass

State after k backward steps (m = s - k positions left, the next one j = m - 1): 14 holds the forward starts of 0, …, m-1 (last first) over the sentinel, 15 the block end ncv m = eB (m-1), and 30, 31, 32, 33 the outputs on positions m, …, s-1.

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_Defs65

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.Src
set_option maxRecDepth 20000
open IntMul NLogN NLogN.KIL Function NLogN.RS J6Seg.PreT J6Seg

Formal statement

theorem J6Seg.Src.bwd_step (s0 : IState HS) (G : Fin HS → List ℤ) {iW : Fin HS} (fW : Free iW)
    {s t lam w A : ℕ} {LW : List ℤ} (hGW : G iW = (w : ℤ) :: LW) (hs : 0 < s) (hsA : s ≤ 2 ^ A)
    (hwA : w ≤ 2 ^ A) (hA : 2 ≤ A) {k : ℕ} (hk : k < s) :
    Sp (bwdB iW) (encK s0 (update (bwS G s t lam w k) 43 [(s : ℤ) - k]))
      (encK s0 (update (bwS G s t lam w (k + 1)) 43 [(s : ℤ) - k])) (80 * uC A DD) := 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.Src.bwd_step`, Solutions/J6SegILSrc4.lean (lines 251–394) of the round-six development.

View graph