Trailing blocks stay near the identity (round six, `aseq_rows`)

Proved

J6Seg.aseq_rows

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

complexity-theoryinteger-multiplicationkappa-improvement

Trailing blocks stay near the identity.

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

theorem J6Seg.aseq_rows : ∀ (L : List ℕ) (A : ℕ → ℕ → ℤ)
    (b : ℕ → ℤ) (η : ℝ), L.Nodup → 0 ≤ η → η + (L.length : ℝ) ^ 2 / 2 ^ P ≤ 1 / 2 →
    (∀ i ∈ L, ∑ k ∈ L.toFinset, |(A i k : ℝ) / 2 ^ P - kd i k| ≤ η) →
    (∀ i ∈ L, ∀ k ∈ L, ¬ S i k → A i k = 0) → PatOK S L →
    ∀ r ≤ L.length, ∀ i ∈ L.drop r,
      ∑ k ∈ (L.drop r).toFinset, |(Aseq P S L A r i k : ℝ) / 2 ^ P - kd i k| ≤ 1 / 2

Context. B-line IL, J pre-table (B5-J), math part 1: the elimination in index form and its bounds

aseq_rows: under the near-identity hypotheses of pivPos_of (same induction), every trailing block of the pattern elimination Aseq stays within 1/2 of the identity in row sums; hence (aseq_entry, aseq_piv) its entries are ≤ (3/2) 2^P and its pivots ≥ 2^P/2;
Mseq: the elimination on line indices that only updates the trailing block (q < i, k); Mseq_eq: on the trailing block it is Aseq (Aseq_last: one more pivot is one more stepA); Mseq_frz: entry (i, k) is frozen from step min i k on. So the final matrix holds Aseq (min i k) (L i) (L k) at (i, k).

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 Real
open IntMul.HvdH IntMul.HvdH.JPf J6QLU
variable (P : ℕ) (S : ℕ → ℕ → Prop) [DecidableRel S]

Formal statement

theorem J6Seg.aseq_rows : ∀ (L : List ℕ) (A : ℕ → ℕ → ℤ)
    (b : ℕ → ℤ) (η : ℝ), L.Nodup → 0 ≤ η → η + (L.length : ℝ) ^ 2 / 2 ^ P ≤ 1 / 2 →
    (∀ i ∈ L, ∑ k ∈ L.toFinset, |(A i k : ℝ) / 2 ^ P - kd i k| ≤ η) →
    (∀ i ∈ L, ∀ k ∈ L, ¬ S i k → A i k = 0) → PatOK S L →
    ∀ r ≤ L.length, ∀ i ∈ L.drop r,
      ∑ k ∈ (L.drop r).toFinset, |(Aseq P S L A r i k : ℝ) / 2 ^ P - kd i k| ≤ 1 / 2 := 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.aseq_rows`, Solutions/J6SegILPreJM1.lean (lines 24–161) of the round-six development.

View graph