`segLineC` computes the sparse segmented inverse (round six, `segLineC_eq`)
ProvedJ6Seg.segLineC_eqsegLineC computes the sparse segmented inverse (real part, one line).
The following holds (Lean statement, in the scope of module Solutions.J6SegLn8):
theorem J6Seg.segLineC_eq (hl : 1 ≤ lam) (hs : 0 < s) (hws : 2 * w < s) (hwK : w ≤ K)
(hKm : 2 * K + 1 ≤ (LJ s t lam w).length) {nc : ℕ} (hsN : s ≤ nc * lam) {x : List ℤ}
(hx : nc * lam ≤ x.length) {u : ℕ} (hu : u < nc * lam) :
(segLineC P R s t lam w α K nc x).getD u 0 =
if u < s then segInvS P lam (TT P R s t α) (BB s t lam w) (fun v => x.getD v 0) u else 0
Context. Segmented inverse (S2), machine side 8: one real line of segInvS by list kernels
The real part of the segmented inverse on one line, as the machine computes it, on a padded
line x of N = n_c λ positions (s ≤ N):
Y = applyL x: the chunk kernel on eachλ-chunk (M⁻¹);- the values of
Yon the lineL = Jlist B, the two capacitance kernels (jsolve_eq); - the coupling window kernel on the cyclic extension (
couple_window), scattered back to the positions (zero offL); Y₂ = applyLof the scattered coupling; the output isY - Y₂.
segLineC_eq: entry u < N of the result is segInvS … u for u < s and 0 beyond.
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 R s t lam w α K : ℕ)
variable {P R s t lam w α K}
theorem J6Seg.segLineC_eq (hl : 1 ≤ lam) (hs : 0 < s) (hws : 2 * w < s) (hwK : w ≤ K)
(hKm : 2 * K + 1 ≤ (LJ s t lam w).length) {nc : ℕ} (hsN : s ≤ nc * lam) {x : List ℤ}
(hx : nc * lam ≤ x.length) {u : ℕ} (hu : u < nc * lam) :
(segLineC P R s t lam w α K nc x).getD u 0 =
if u < s then segInvS P lam (TT P R s t α) (BB s t lam w) (fun v => x.getD v 0) u else 0 := by sorry