The `B₀` tensor pass with the segmented inverse (round six, `passBseg`)
ProvedJ6Seg.passBsegThe B₀ tensor pass with the segmented inverse.
The following holds (Lean statement, in the scope of module Solutions.J6SegLn11):
theorem J6Seg.passBseg (hp18 : 18 ≤ (2 : ℝ) ^ p) (hst : ∀ i, s i ≤ t i) (ys : List GI)
(y : ((i : Fin d) → ZMod (t i)) → ℂ) (hrep : RepFull p t ys y) (hy : ‖y‖ ≤ 1)
(Bm : (i : Fin d) → (ZMod (t i) → ℂ) →L[ℂ] (ZMod (s i) → ℂ))
(hBn : ∀ i, ‖Bm i‖ ≤ 1 / 2)
(hErr : ∀ i (W : ℕ → ℤ × ℤ), (∀ k, ‖IntMul.HvdH.P47.toC (W k)‖ ≤ 2 ^ p) →
∀ l : ZMod (s i), ‖IntMul.HvdH.P47.toC (B0seg p (Pf (s i)) R lam w (s i) (t i) α W l.val) -
2 ^ p * Bm i (fun k => IntMul.HvdH.P47.toC (W k.val) / 2 ^ p) l‖ ≤ 9)
(hZ : ∀ i, B0seg p (Pf (s i)) R lam w (s i) (t i) α (fun _ => (0, 0)) = fun _ => (0, 0)) :
RepPad p s t (tensorGo (mapsBs p R lam w α Pf s t) (List.ofFn t) ys)
(vOf p s t (tensorGo (mapsBs p R lam w α Pf s t) (List.ofFn t) ys)) ∧
DiscL p (tensorGo (mapsBs p R lam w α Pf s t) (List.ofFn t) ys) ∧
‖vOf p s t (tensorGo (mapsBs p R lam w α Pf s t) (List.ofFn t) ys) - tensCLM (kerB Bm) y‖ ≤
(9 * d) * hp p
Context. Segmented inverse (S2), machine side 11: the B₀ tensor pass
Axis by axis (tensorGo, as the frozen KFY.passB), every t_i-line X is replaced by the
t_i values B0seg … (X as a function) l (zero for l ≥ s_i): this is what lineB computes
(lineB_list, with n_c λ = t_i).
passBseg: for per-axis maps Bm i with ‖Bm i‖ ≤ 1/2, the per-axis bound 9 of
r6_axisMaps_fit and B0seg 0 = 0, from RepFull ys y, ‖y‖ ≤ 1:
RepPad of the result, every entry in the disc (GB (p+2)), and
‖vOf − tensCLM (kerB Bm) y‖ ≤ 9 d · 2^{-p}.
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 Complex
open IntMul IntMul.HvdH IntMul.HvdH.Ref IntMul.HvdH.RefPf NLogN.KFM NLogN.KFY IntMul.OpenAI.RT
open NLogN.KFB (GI gflat)
variable {d : ℕ} (p R lam w α : ℕ) (Pf : ℕ → ℕ) (s t : Fin d → ℕ) [∀ i, NeZero (s i)]
[∀ i, NeZero (t i)]
theorem J6Seg.passBseg (hp18 : 18 ≤ (2 : ℝ) ^ p) (hst : ∀ i, s i ≤ t i) (ys : List GI)
(y : ((i : Fin d) → ZMod (t i)) → ℂ) (hrep : RepFull p t ys y) (hy : ‖y‖ ≤ 1)
(Bm : (i : Fin d) → (ZMod (t i) → ℂ) →L[ℂ] (ZMod (s i) → ℂ))
(hBn : ∀ i, ‖Bm i‖ ≤ 1 / 2)
(hErr : ∀ i (W : ℕ → ℤ × ℤ), (∀ k, ‖IntMul.HvdH.P47.toC (W k)‖ ≤ 2 ^ p) →
∀ l : ZMod (s i), ‖IntMul.HvdH.P47.toC (B0seg p (Pf (s i)) R lam w (s i) (t i) α W l.val) -
2 ^ p * Bm i (fun k => IntMul.HvdH.P47.toC (W k.val) / 2 ^ p) l‖ ≤ 9)
(hZ : ∀ i, B0seg p (Pf (s i)) R lam w (s i) (t i) α (fun _ => (0, 0)) = fun _ => (0, 0)) :
RepPad p s t (tensorGo (mapsBs p R lam w α Pf s t) (List.ofFn t) ys)
(vOf p s t (tensorGo (mapsBs p R lam w α Pf s t) (List.ofFn t) ys)) ∧
DiscL p (tensorGo (mapsBs p R lam w α Pf s t) (List.ofFn t) ys) ∧
‖vOf p s t (tensorGo (mapsBs p R lam w α Pf s t) (List.ofFn t) ys) - tensCLM (kerB Bm) y‖ ≤
(9 * d) * hp p := by sorry