Round-six lemma `sum_stage`

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

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

theorem J6Seg.sum_stage {I : Finset ℕ} {ct xt : ℕ → ℤ} {c x : ℕ → ℝ} {ec δ X C : ℝ}
    (hc : ∀ k ∈ I, |(ct k : ℝ) / 2 ^ P - c k| ≤ ec) (hC : ∑ k ∈ I, |c k| ≤ C)
    (hx : ∀ k ∈ I, |(xt k : ℝ) / 2 ^ P - x k| ≤ δ) (hX : ∀ k ∈ I, |(xt k : ℝ) / 2 ^ P| ≤ X)
    (hec : 0 ≤ ec) (hδ : 0 ≤ δ) :
    |(rs P (∑ k ∈ I, ct k * xt k) : ℝ) / 2 ^ P - ∑ k ∈ I, c k * x k| ≤
      1 / (2 * 2 ^ P) + I.card * ec * X + C * δ

Context. Segmented inverse (S2): fixed-point error of one block solve and of single M⁻¹ entries

• sum_stage: one rounded linear stage rs P (Σ c̃_k x̃_k) against the exact Σ c_k x_k.
• blkI_err (report L7/L10 block part): with tables accurate to E ulps (dd to relative E ulps), input |z| ≤ 2^P B, Dm ≥ max_u D_u and 8 K (B+1) ≤ 2^P, K = (n+1)E + 1: |blkI z / 2^P - M_c⁻¹ (z/2^P)| ≤ 9 Dm K (B+1) / 2^P.
• TinvI_err, MinvI_err: single entries of T⁻¹ (direct or persymmetric) and of M⁻¹.

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