Round-six lemma `MinvE_err`
ProvedJ6Seg.MinvE_errM⁻¹_{uv} = D_u T⁻¹_{uv} D_v⁻¹ as computed in fixed point.
The following holds (Lean statement, in the scope of module Solutions.J6SegEnt):
theorem J6Seg.MinvE_err {T : Tables} {a n w : ℕ} {E Dm : ℝ} (hα : 2 ≤ α) (hσ : 1 ≤ σ)
(hx : 2 ≤ α ^ 2 * (σ - 1)) (hb : |b| ≤ 1 / 2) (hT : BlkTab P α σ b T a n E) (hE : 0 ≤ E)
(hDm : ∀ u < n, ddR α σ u ≤ Dm)
(hP : 100 * (((n : ℝ) + 1) * E + 1) ≤ 2 ^ P) {u v : ℕ} (hu : u < n) (hv : v < n) :
|(fmul P (fmul P (T.dd u) (T.di v)) (TinvI P T w a n u v) : ℝ) / 2 ^ P -
MinvF α σ b n u v| ≤ 12 * Dm * (((n : ℝ) + 1) * E + 1) / 2 ^ P
Context. Segmented inverse (S2): single entries of the block inverse (capacitance corners)
TinvI evaluates T⁻¹_{uv} directly or through persymmetry (TinvF_persym), MinvI
evaluates M⁻¹_{uv} = D_u T⁻¹_{uv} D_v⁻¹. With K = (n+1)E + 1, 100 K ≤ 2^P:
|TinvI/2^P - T⁻¹_{uv}| ≤ 7K/2^P and |MinvI/2^P - M⁻¹_{uv}| ≤ 12 Dm K/2^P.
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 Real
open J6QLU
variable (P : ℕ)
variable {P} {α σ b : ℝ}
theorem J6Seg.MinvE_err {T : Tables} {a n w : ℕ} {E Dm : ℝ} (hα : 2 ≤ α) (hσ : 1 ≤ σ)
(hx : 2 ≤ α ^ 2 * (σ - 1)) (hb : |b| ≤ 1 / 2) (hT : BlkTab P α σ b T a n E) (hE : 0 ≤ E)
(hDm : ∀ u < n, ddR α σ u ≤ Dm)
(hP : 100 * (((n : ℝ) + 1) * E + 1) ≤ 2 ^ P) {u v : ℕ} (hu : u < n) (hv : v < n) :
|(fmul P (fmul P (T.dd u) (T.di v)) (TinvI P T w a n u v) : ℝ) / 2 ^ P -
MinvF α σ b n u v| ≤ 12 * Dm * (((n : ℝ) + 1) * E + 1) / 2 ^ P := by sorry