The forward kernel computes the forward values (round six, `fwdK_eq`)

Proved

J6Seg.fwdK_eq

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

complexity-theoryinteger-multiplicationkappa-improvement

The forward kernel computes the forward values.

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

theorem J6Seg.fwdK_eq (cf : ℕ → ℕ) (hsupp : ∀ r < L.length, FwdSupp (S := S) (L := L) r (cf r)) :
    fwdK P ((List.range L.length).map fun r => fsW P S L A r (cf r))
      ((List.range L.length).map fun r => b (L.getD r 0)) [] =
      ((List.range L.length).map (btV P S L A b)).reverse

Context. Segmented inverse (S2), machine side 4: the capacitance solve as list kernels

The per-line work on the near-boundary positions L = Jlist B = [j₀ < j₁ < …] is done by two list kernels driven by precomputed (data-independent) coefficient streams:

fwdK fs Y []: for r = 0, 1, …: bt_r = Y_r − ∑_i fmul (fs_r)_i bt_{r-1-i} (the accumulator holds the previous values, most recent first); the result is [bt_{m-1}, …, bt_0];
bwdK bs bt [] []: for r = m-1, …, 0 with the record (cb, cz, pv, fl): z_r = fdiv (bt_r − ∑ fmul cb_i z_{r+1+i} − ∑ fmul cz_i ZB_i) pv, where ZB holds the z of the border indices computed so far (fl = 1 marks a border index); the result is [z₀, …, z_{m-1}].

fwdK_eq, bwdK_eq: with the coefficient streams fsOf, bsOf of the line (built from Aseq of the pattern-restricted elimination of capI), fwdK computes the forward values bseq r j_r and bwdK the solution geSolveS … j_r, given the support facts of the pattern (FwdSupp, BwdSupp).

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_Defs61

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg
open Finset
variable (P : ℕ) (S : ℕ → ℕ → Prop) [DecidableRel S] (L : List ℕ) (A : ℕ → ℕ → ℤ) (b : ℕ → ℤ)
variable {P S L A b}

Formal statement

theorem J6Seg.fwdK_eq (cf : ℕ → ℕ) (hsupp : ∀ r < L.length, FwdSupp (S := S) (L := L) r (cf r)) :
    fwdK P ((List.range L.length).map fun r => fsW P S L A r (cf r))
      ((List.range L.length).map fun r => b (L.getD r 0)) [] =
      ((List.range L.length).map (btV P S L A b)).reverse := 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.fwdK_eq`, Solutions/J6SegLn4.lean (lines 111–153) of the round-six development.

View graph