The computed capacitance acts as `z ↦ z + (M⁻¹ Δ z)|_J` up to `λ(2w+1) δ Z` (`cap_apply`)

The computed capacitance acts as z ↦ z + (M⁻¹ Δ z)|_J up to λ(2w+1) δ Z.

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

theorem J6Seg.cap_apply (hB : BlocksOK s t B) (hs : 0 < s) (hst : s ≤ t) (hα : 2 ≤ α)
    (hx : 3 ≤ xθ s t α) (hT : TabOK P s t α B T E Dm) (hE : 0 ≤ E) {lam : ℕ}
    (hlam : ∀ i < s, B.len i ≤ lam) (hP : 100 * (((lam : ℝ) + 1) * E + 1) ≤ 2 ^ P)
    {a : ℕ} (ha : a ∈ (Jlist B).toFinset) (ha' : a < s) (zr : ℕ → ℝ) {Z : ℝ} (hZ0 : 0 ≤ Z)
    (hz : ∀ k ∈ (Jlist B).toFinset, |zr k| ≤ Z) :
    |∑ k ∈ (Jlist B).toFinset, (capI P T B a k : ℝ) / 2 ^ P * zr k -
      (zr a + Mv (blS B) (MiG s t α B) (Dv (Hset B) (col B.s) (cfG s t α) zr) a)| ≤
      lam * (2 * B.w + 1) * (15 * Dm * (((lam : ℝ) + 1) * E + 1) / 2 ^ P) * Z

Context. Segmented inverse (S2): accuracy of the global stages

With K = (λ+1)E + 1 (λ ≥ every block length, E the table accuracy in ulps) and Dm ≥ every D_u = e^{πα²θu²} used:

• applyMinv_err: |applyMinv V / 2^P - M⁻¹ (V/2^P)| ≤ 9 Dm K (B+1)/2^P (|V/2^P| ≤ B);
• coupleI_err: |coupleI z / 2^P - Δ (z/2^P)| ≤ (2w+1)(1/2 + E Z)/2^P (|z/2^P| ≤ Z on J);
• capI_row, capI_apply: the computed capacitance C = I + (M⁻¹Δ)|_J has row deviation ≤ 1/7 + λ(2w+1)δ and |C z - (z + M⁻¹ Δ z)| ≤ λ(2w+1) δ Z with δ = 15 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*).