Sparse elimination = dense elimination (round six, `geSolveS_eq`)
ProvedJ6Seg.geSolveS_eqSparse elimination = dense elimination (zero pattern closed under elimination, pivots positive by the near-identity hypotheses).
The following holds (Lean statement, in the scope of module Solutions.J6SegBand):
theorem J6Seg.geSolveS_eq (S : ℕ → ℕ → Prop) [DecidableRel S] : ∀ (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 →
∀ k, geSolveS P S L A b k = geSolve P L A b k
Context. Segmented inverse (S2): sparse (banded + border) elimination
geSolveS P S L A b is the elimination of geSolve restricted to a pattern S: the Schur
update of (i, k) is performed only when S i j ∧ S j k, the right-hand side update only when
S i j, and the back substitution sums only over S j k.
geSolveS_eq: if A vanishes off S on L × L, S is closed under elimination in the order of
L (PatOK: S i j → S j k → S i k for i, k after the pivot j), and the hypotheses of
geSolve_resid hold (row deviation η, η + |L|²/2^P ≤ 1/2, so every pivot is positive), then
geSolveS = geSolve. Hence the error theorems of geSolve hold verbatim for the sparse version.
bandS m c a b: |a - b| ≤ m or a ≥ c or b ≥ c (band plus a border at the end, the
cyclic block-tridiagonal shape); PatOK holds for it along any increasing list (bandS_patOK).
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*).
-- 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 : ℕ)
theorem J6Seg.geSolveS_eq (S : ℕ → ℕ → Prop) [DecidableRel S] : ∀ (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 →
∀ k, geSolveS P S L A b k = geSolve P L A b k := by sorry