Block solve error (round six, `blkI_err`)

Proved

J6Seg.blkI_err

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

complexity-theoryinteger-multiplicationkappa-improvement

Block solve error.

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

theorem J6Seg.blkI_err {T : Tables} {a n : ℕ} {E B Dm : ℝ} (hα : 2 ≤ α) (hσ : 1 ≤ σ)
    (hx : 2 ≤ α ^ 2 * (σ - 1)) (hb : |b| ≤ 1 / 2) (hT : BlkTab P α σ b T a n E)
    (hE : 0 ≤ E) (hB : 0 ≤ B) (hDm : ∀ u < n, ddR α σ u ≤ Dm)
    (hP : 8 * (((n : ℝ) + 1) * E + 1) * (B + 1) ≤ 2 ^ P)
    (z : ℕ → ℤ) (hz : ∀ u < n, |(z u : ℝ) / 2 ^ P| ≤ B) :
    ∀ u < n, |(blkI P T a n z u : ℝ) / 2 ^ P - blkE α σ b n (fun k => (z k : ℝ) / 2 ^ P) u| ≤
      9 * Dm * (((n : ℝ) + 1) * E + 1) * (B + 1) / 2 ^ P

Context. Segmented inverse (S2): fixed-point error of one block solve and of single M⁻¹ entries

sum_stage: one rounded linear stage rs P (Σ c̃_k x̃_k) against the exact Σ c_k x_k.
blkI_err (report L7/L10 block part): with tables accurate to E ulps (dd to relative E ulps), input |z| ≤ 2^P B, Dm ≥ max_u D_u and 8 K (B+1) ≤ 2^P, K = (n+1)E + 1: |blkI z / 2^P - M_c⁻¹ (z/2^P)| ≤ 9 Dm K (B+1) / 2^P.
TinvI_err, MinvI_err: single entries of T⁻¹ (direct or persymmetric) and of M⁻¹.

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_Defs3

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg
open Finset Real
open J6QLU
variable (P : ℕ) (α σ b : ℝ)
variable {P α σ b}

Formal statement

theorem J6Seg.blkI_err {T : Tables} {a n : ℕ} {E B Dm : ℝ} (hα : 2 ≤ α) (hσ : 1 ≤ σ)
    (hx : 2 ≤ α ^ 2 * (σ - 1)) (hb : |b| ≤ 1 / 2) (hT : BlkTab P α σ b T a n E)
    (hE : 0 ≤ E) (hB : 0 ≤ B) (hDm : ∀ u < n, ddR α σ u ≤ Dm)
    (hP : 8 * (((n : ℝ) + 1) * E + 1) * (B + 1) ≤ 2 ^ P)
    (z : ℕ → ℤ) (hz : ∀ u < n, |(z u : ℝ) / 2 ^ P| ≤ B) :
    ∀ u < n, |(blkI P T a n z u : ℝ) / 2 ^ P - blkE α σ b n (fun k => (z k : ℝ) / 2 ^ P) u| ≤
      9 * Dm * (((n : ℝ) + 1) * E + 1) * (B + 1) / 2 ^ P := 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.blkI_err`, Solutions/J6SegBlk.lean (lines 142–334) of the round-six development.

View graph