Proposition 4.7 with the segmented inverse (round six, `prop_4_7_seg`)

Proposition 4.7 with the segmented inverse.

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

theorem J6Seg.prop_4_7_seg (p P R lam w s t α : ℕ) [NeZero s] [NeZero t] (hst : s < t)
    (hcop : Nat.Coprime s t) (hα : 2 ≤ α) (hαp : α ^ 2 ≤ p) (hx3 : 3 * s ≤ α ^ 2 * (t - s))
    (hl : 1 ≤ lam) (hw : w ≤ s) (hR : ddR (α : ℝ) ((t : ℝ) / s) (lam - 1) ≤ 2 ^ R)
    (hpP : p + 1 ≤ P) (hP : 1000 * fullG lam w s t α (1 / 2) ≤ 2 ^ P)
    (hE : 200 * segE p P lam w s t α ≤ 2 ^ p) :
    ∃ (A : (ZMod s → ℂ) →L[ℂ] (ZMod t → ℂ)) (B : (ZMod t → ℂ) →L[ℂ] (ZMod s → ℂ)),
      ‖A‖ ≤ 1 ∧ ‖B‖ ≤ 1 / 2 ∧
      (∀ u, (s : ℂ)⁻¹ • ZMod.dft u = (2 : ℂ) ^ (2 * α ^ 2) • B ((t : ℂ)⁻¹ • ZMod.dft (A u))) ∧
      (∀ U : ℕ → ℤ × ℤ, (∀ i, ‖toC (U i)‖ ≤ 2 ^ p) → ∀ k : ZMod t,
        ‖toC (Sapprox p s t α U k.val) - 2 ^ p * A (fun j => toC (U j.val) / 2 ^ p) k‖
          ≤ 6 * sWidth p α + 4) ∧
      (∀ V : ℕ → ℤ × ℤ, (∀ i, ‖toC (V i)‖ ≤ 2 ^ p) → ∀ j : ZMod s,
        ‖toC (Bseg p P R lam w s t α V j.val) - 2 ^ p * B (fun k => toC (V k.val) / 2 ^ p) j‖
          ≤ 2 * segE p P lam w s t α + 3)

Context. Segmented inverse (S2): Proposition 4.7 and Lemma 19 with the segmented J̃

The base Bapprox = P̃_s⁻¹ D̃' J̃' C̃ P̃_t (HvdH Proposition 4.7) solves the resampling system (I + E) w = y/2 by the Neumann iteration Japprox. Here the solver is the segmented inverse segInvFullS (sparse banded elimination, tables and blocks computed from the parameters):

• segJ p P R λ w s t α Y: scale Y (precision p) to precision P (exact shift by P - p - 1, which also halves), run segInvFullS, shift back by P - p (floor), and read 0 outside [0, s).
• Bseg = P̃_s⁻¹ D̃' segJ C̃ P̃_t and the permutation-free B0seg = D̃' segJ C̃ (B0segP: read mod s).
• prop_4_7_seg: the maps A, B of Proposition 4.7 (built exactly as in the base proof), with ‖toC (Bseg V)_j - 2^p (B v)_j‖ ≤ 2 segE + 3, where segE = 2^p (60 G/2^P + 18 e^{-πα² w(w+1)}) + 1, G = fullG λ w s t α (1/2). Hypotheses: α²θ ≥ 3 (3 s ≤ α² (t - s)), α² ≤ p, 1 ≤ λ, w ≤ s, D_{λ-1} ≤ 2^R, p + 1 ≤ P, 1000 G ≤ 2^P, 200 segE ≤ 2^p (no jIter hypothesis).
• lemma19_seg: the same in the B₀ = B0of s t B form with the permS/permT identity of AxisMaps6.hid / KFM.AxisMaps.hid.

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