Residual of the segmented inverse (round six, `res_bound`)
ProvedJ6Seg.res_boundResidual of the segmented inverse (exact Woodbury, all four stages perturbed).
The following holds (Lean statement, in the scope of module Solutions.J6SegRes):
theorem J6Seg.res_bound (Mi : ℕ → ℕ → ℝ) {I J : Finset ℕ} {u W y y₂ x z : ℕ → ℝ}
{ε₁ ε₂ ε₃ ε₄ A d μ : ℝ} (hJI : J ⊆ I) (hblI : ∀ i ∈ I, bl i ⊆ I)
(hcl : ∀ i ∈ I, ∀ h ∈ Hs i, cl i h ∈ J)
(hMM : ∀ i ∈ I, ∀ f : ℕ → ℝ, Mv bl Mx (Mv bl Mi f) i = f i)
(hMi : ∀ (f : ℕ → ℝ) (F : ℝ), (∀ k ∈ I, |f k| ≤ F) → ∀ i ∈ I, |Mv bl Mi f i| ≤ μ * F)
(hA : ∀ i ∈ I, ∑ k ∈ bl i, |Mx i k| ≤ A) (hd : ∀ i ∈ I, ∑ h ∈ Hs i, |cf i h| ≤ d)
(hd0 : 0 ≤ d) (hμ : 0 ≤ μ) (hε₂ : 0 ≤ ε₂) (hε₃ : 0 ≤ ε₃) (hε₄ : 0 ≤ ε₄)
(hx : ∀ i, x i = y i - y₂ i)
(h1 : ∀ i ∈ I, |y i - Mv bl Mi u i| ≤ ε₁)
(h2 : ∀ i ∈ I, |y₂ i - Mv bl Mi W i| ≤ ε₂)
(h3 : ∀ i ∈ I, |W i - Dv Hs cl cf z i| ≤ ε₃)
(h4 : ∀ a ∈ J, |z a + Mv bl Mi (Dv Hs cl cf z) a - y a| ≤ ε₄) :
∀ i ∈ I, |Mv bl Mx x i + Dv Hs cl cf x i - u i| ≤
A * (ε₁ + ε₂) + ε₃ + d * (ε₄ + μ * ε₃ + ε₂)
Context. Segmented inverse (S2): the exact Woodbury residual identity (abstract form)
Abstract setting on positions ℕ (a position set I): a block-diagonal matrix M given by its
blocks bl i and entries Mx, its block inverse Mi, and a sparse coupling Δ given row-wise
by offsets Hs i, columns cl i h and coefficients cf i h, with every coupling column in the
capacitance index set J.
res_bound (report L8 + L10, residual form): if the four fixed-point stages of the segmented
inverse are accurate,
y ≈ M⁻¹ u(ε₁),W ≈ Δ z(ε₃),y₂ ≈ M⁻¹ W(ε₂),z + (M⁻¹ Δ z)|_J ≈ y|_J(ε₄, the capacitance solve),
then x = y - y₂ satisfies |((M + Δ) x - u)_i| ≤ A(ε₁+ε₂) + ε₃ + d(ε₄ + μ ε₃ + ε₂)
(A, d, μ bound ‖M‖, ‖Δ‖, ‖M⁻¹‖ row-wise). No exact intermediate solution is needed.
Miv_bound: ‖M⁻¹‖ ≤ 1/(1-m) from M M⁻¹ = I and ‖M - I‖ ≤ m < 1 (via near_id).
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_Defs3 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg open Finset variable (bl : ℕ → Finset ℕ) (Mx : ℕ → ℕ → ℝ) (Hs : ℕ → Finset ℤ) (cl : ℕ → ℤ → ℕ) (cf : ℕ → ℤ → ℝ)
theorem J6Seg.res_bound (Mi : ℕ → ℕ → ℝ) {I J : Finset ℕ} {u W y y₂ x z : ℕ → ℝ}
{ε₁ ε₂ ε₃ ε₄ A d μ : ℝ} (hJI : J ⊆ I) (hblI : ∀ i ∈ I, bl i ⊆ I)
(hcl : ∀ i ∈ I, ∀ h ∈ Hs i, cl i h ∈ J)
(hMM : ∀ i ∈ I, ∀ f : ℕ → ℝ, Mv bl Mx (Mv bl Mi f) i = f i)
(hMi : ∀ (f : ℕ → ℝ) (F : ℝ), (∀ k ∈ I, |f k| ≤ F) → ∀ i ∈ I, |Mv bl Mi f i| ≤ μ * F)
(hA : ∀ i ∈ I, ∑ k ∈ bl i, |Mx i k| ≤ A) (hd : ∀ i ∈ I, ∑ h ∈ Hs i, |cf i h| ≤ d)
(hd0 : 0 ≤ d) (hμ : 0 ≤ μ) (hε₂ : 0 ≤ ε₂) (hε₃ : 0 ≤ ε₃) (hε₄ : 0 ≤ ε₄)
(hx : ∀ i, x i = y i - y₂ i)
(h1 : ∀ i ∈ I, |y i - Mv bl Mi u i| ≤ ε₁)
(h2 : ∀ i ∈ I, |y₂ i - Mv bl Mi W i| ≤ ε₂)
(h3 : ∀ i ∈ I, |W i - Dv Hs cl cf z i| ≤ ε₃)
(h4 : ∀ a ∈ J, |z a + Mv bl Mi (Dv Hs cl cf z) a - y a| ≤ ε₄) :
∀ i ∈ I, |Mv bl Mx x i + Dv Hs cl cf x i - u i| ≤
A * (ε₁ + ε₂) + ε₃ + d * (ε₄ + μ * ε₃ + ε₂) := by sorry