The coupling at a line position is the window sum (round six, `couple_window`)
ProvedJ6Seg.couple_windowThe coupling at a line position is the window sum.
The following holds (Lean statement, in the scope of module Solutions.J6SegLn6):
theorem J6Seg.couple_window (hsort : L.Pairwise (· < ·)) (hL : ∀ x ∈ L, x < B.s) (hwK : B.w ≤ K)
(hKm : 2 * K + 1 ≤ L.length) (hws : 2 * B.w < B.s) (zf : ℕ → ℤ)
(hz : ∀ k, k ∉ L → zf k = 0) {r : ℕ} (hr : r < L.length) :
coupleI P T B zf (L.getD r 0) = ∑ i ∈ range (2 * K + 1),
fmul P (ccOf T B L K r i) ((zext K (zlOf L zf)).getD (r + i) 0)
Context. Segmented inverse (S2), machine side 6: the coupling as a cyclic window
On a sorted line L = [j₀ < … < j_{m-1}] of positions < s (the near-boundary positions), with
z vanishing off L, the coupling W = U z at j_r only reads z at the line indices
q within cyclic index distance K ≥ w of r (positions within cyclic distance w, and the
line is strictly increasing). With the cyclically extended list
zext = (last K of zl) ++ zl ++ (first K of zl), zl = [z_{j_0}, …, z_{j_{m-1}}]:
couple_window:W_{j_r} = ∑_{i ≤ 2K} fmul (cc_r)_i zext_{r+i}(2K+1 ≤ m,2w < s);couple_off:W_i = 0at positions that are not near a block boundary.
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*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.
import Definitions.Def_IntMul_Kappa_R6_Defs61
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6Seg
open Finset
variable (P : ℕ) (T : Tables) (B : Blocks) (L : List ℕ) (K : ℕ)
variable {P T B L K}
theorem J6Seg.couple_window (hsort : L.Pairwise (· < ·)) (hL : ∀ x ∈ L, x < B.s) (hwK : B.w ≤ K)
(hKm : 2 * K + 1 ≤ L.length) (hws : 2 * B.w < B.s) (zf : ℕ → ℤ)
(hz : ∀ k, k ∉ L → zf k = 0) {r : ℕ} (hr : r < L.length) :
coupleI P T B zf (L.getD r 0) = ∑ i ∈ range (2 * K + 1),
fmul P (ccOf T B L K r i) ((zext K (zlOf L zf)).getD (r + i) 0) := by sorry