The sparse algorithm equals the dense one (round six, `segInvS_eq`)

The sparse algorithm equals the dense one under the hypotheses of segInv_err.

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

theorem J6Seg.segInvS_eq {E Dm Bu : ℝ} (hs : 0 < s) (hst : s ≤ t) (hα : 2 ≤ α) (hx : 3 ≤ xθ s t α)
    (hB : BlocksOK s t B) (hlam : ∀ i < s, B.len i ≤ lam)
    (hT : TabOK P s t α B T E Dm) (hE : 0 ≤ E) (hBu : 0 ≤ Bu)
    (hP : 1000 * segG B lam E Dm Bu ≤ 2 ^ P) (U : ℕ → ℤ) :
    ∀ i, segInvS P lam T B U i = segInv P T B U i

Context. Segmented inverse (S2): the sparse algorithm

segInvS P lam T B U is segInv with the capacitance solved by geSolveS on the pattern bandS (λ + w) (s - λ - w): a band of half-width λ + w (blocks of length ≤ λ, coupling width w) plus the border of positions ≥ s - λ - w (the cyclic wrap). Per row of the capacitance at most 2(λ+w)+1 band entries plus the border are touched.

• capI_band: the capacitance vanishes off the pattern;
• segInvS_eq: under the hypotheses of segInv_err, segInvS = segInv;
• segInvFullS_err: the fully instantiated sparse algorithm satisfies the bound of segInvFull_err.

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