Row deviation of the computed capacitance from `I` (`cap_row`)

Row deviation of the computed capacitance from I.

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

theorem J6Seg.cap_row (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 < s) :
    ∑ k ∈ (Jlist B).toFinset, |(capI P T B a k : ℝ) / 2 ^ P - kd a k| ≤
      1 / 7 + lam * (2 * B.w + 1) * (15 * Dm * (((lam : ℝ) + 1) * E + 1) / 2 ^ P)

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*).