Split of `N` (truncation, report L8) (round six, `nsplit`)

Split of N (truncation, report L8): N x = M x + Δ x + drop, |drop| ≤ 4 e^{-πα² w(w+1)} ‖x‖.

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

theorem J6Seg.nsplit (hB : BlocksOK s t B) (hs : 0 < s) (hst : s ≤ t) (hα : 2 ≤ α)
    (hx1 : 1 ≤ xθ s t α) (x : ℕ → ℝ) (X : ℝ) (hX : ∀ k < s, |x k| ≤ X) {i : ℕ} (hi : i < s) :
    |NxR s t α x i - (Mv (blS B) (MxG s t α) x i + Dv (Hset B) (col B.s) (cfG s t α) x i)| ≤
      4 * exp (-(π * (α : ℝ) ^ 2 * (B.w * (B.w + 1)))) * X

Context. Segmented inverse (S2): the resampling system split into blocks, coupling and tail

For a valid block structure (BlocksOK: blocks are wrap-free runs [st i, st i + len i) that partition [0, s), coupling width w ≤ s):

• MxG (the block part of N, entries δ_{ik} + e_{i,k-i}) and MiG (its exact block inverse D T⁻¹ D⁻¹ from the q-LU) satisfy M M⁻¹ = I (hinvG, via eEx_recentre, MF_mul_MinvF);
• row sums: ‖M - I‖, ‖Δ‖ ≤ 2^{-α²θ} (rowM, rowD), hence ‖M⁻¹‖ ≤ 8/7 when α²θ ≥ 3;
• every coupling column lies in the capacitance set Jlist (col_mem);
• nsplit: (N x)_i = (M x)_i + (Δ x)_i + drop, |drop| ≤ 4 e^{-πα² w(w+1)} ‖x‖;
• nearN: ‖N d‖ ≤ ρ ⇒ ‖d‖ ≤ 8ρ/7 (‖N - I‖ ≤ 1/8).

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