The segmented `B₀` lines in the round-six regime at the fitted (cost-row) parameters (round six, `r6_axisMaps_fit`)
ProvedJ6Seg.r6_axisMaps_fitThe segmented B₀ lines in the round-six regime at the fitted (cost-row) parameters
λ = lamP d (the power of two in (dk/2, dk]), w = 7k (k = ⌊√d⌋ + 1), R = ⌊p/7⌋,
P = segPF p d s; moreover ‖B_i‖ ≤ 1/2 and B₀ sends the zero line to zero.
The following holds (Lean statement, in the scope of module Solutions.J6SegLine):
theorem J6Seg.r6_axisMaps_fit (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ,
SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 →
∀ [∀ i, NeZero (sD6 src D i)] [∀ i, NeZero (tD6 P n D i)],
∃ M : AxisMaps6 (αN6 P n) (sD6 src D) (tD6 P n D), ∀ i : Fin (D + 1), ‖M.B i‖ ≤ 1 / 2 ∧
(∀ U : ℕ → ℤ × ℤ, (∀ k, ‖toC (U k)‖ ≤ 2 ^ pP6 P n) → ∀ k : ZMod (tD6 P n D i),
‖toC (Sapprox (pP6 P n) (sD6 src D i) (tD6 P n D i) (αN6 P n) U k.val) -
2 ^ pP6 P n * M.A i (fun j => toC (U j.val) / 2 ^ pP6 P n) k‖
≤ 6 * sWidth (pP6 P n) (αN6 P n) + 4) ∧
(∀ W : ℕ → ℤ × ℤ, (∀ k, ‖toC (W k)‖ ≤ 2 ^ pP6 P n) → ∀ l : ZMod (sD6 src D i),
‖toC (B0seg (pP6 P n) (segPF (pP6 P n) (dP6 P n) (sD6 src D i)) (pP6 P n / 7)
(lamP (dP6 P n)) (wF (dP6 P n))
(sD6 src D i) (tD6 P n D i) (αN6 P n) W l.val) -
2 ^ pP6 P n * M.B i (fun k => toC (W k.val) / 2 ^ pP6 P n) l‖ ≤ 9) ∧
B0seg (pP6 P n) (segPF (pP6 P n) (dP6 P n) (sD6 src D i)) (pP6 P n / 7)
(lamP (dP6 P n)) (wF (dP6 P n)) (sD6 src D i) (tD6 P n D i) (αN6 P n)
(fun _ => (0, 0)) = fun _ => (0, 0)
Context. Segmented inverse (S2): the B₀ line maps of LineNeed6 (math side)
r6_axisMaps_seg: in the round-six regime (n ≥ n₁, every SrcOK6 source list, d = D + 1)
there are per-axis exact maps M : AxisMaps6 (αN6 P n) (sD6 src D) (tD6 P n D) (the structure
of R6Ifaces, unchanged) such that on every axis i the segmented fixed-point procedure
B0seg p (segP p d s_i) 0 1 (6d) s_i t_i α (λ = 1, R = 0, w = 6d)
approximates 2^p M.B i within 9 units of 2^{-p} (p = pP6 P n), and Sapprox
approximates 2^p M.A i within the base bound 6 sWidth p α + 4. The 9 is far inside the
interface budget errW6 P n · 2^{-p} = 2^{⌊p/2⌋ - p}.
The machine side (IRuns of the B₀ line procedure, RepFull/RepPad, the tensor layout, the
cost row) is not addressed here.
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 import Definitions.Def_IntMul_KappaFramework import Definitions.Def_IntMul_KappaJainData set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg open Complex Real open IntMul.HvdH IntMul.HvdH.P47 IntMul.Kappa.R6
theorem J6Seg.r6_axisMaps_fit (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ,
SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 →
∀ [∀ i, NeZero (sD6 src D i)] [∀ i, NeZero (tD6 P n D i)],
∃ M : AxisMaps6 (αN6 P n) (sD6 src D) (tD6 P n D), ∀ i : Fin (D + 1), ‖M.B i‖ ≤ 1 / 2 ∧
(∀ U : ℕ → ℤ × ℤ, (∀ k, ‖toC (U k)‖ ≤ 2 ^ pP6 P n) → ∀ k : ZMod (tD6 P n D i),
‖toC (Sapprox (pP6 P n) (sD6 src D i) (tD6 P n D i) (αN6 P n) U k.val) -
2 ^ pP6 P n * M.A i (fun j => toC (U j.val) / 2 ^ pP6 P n) k‖
≤ 6 * sWidth (pP6 P n) (αN6 P n) + 4) ∧
(∀ W : ℕ → ℤ × ℤ, (∀ k, ‖toC (W k)‖ ≤ 2 ^ pP6 P n) → ∀ l : ZMod (sD6 src D i),
‖toC (B0seg (pP6 P n) (segPF (pP6 P n) (dP6 P n) (sD6 src D i)) (pP6 P n / 7)
(lamP (dP6 P n)) (wF (dP6 P n))
(sD6 src D i) (tD6 P n D i) (αN6 P n) W l.val) -
2 ^ pP6 P n * M.B i (fun k => toC (W k.val) / 2 ^ pP6 P n) l‖ ≤ 9) ∧
B0seg (pP6 P n) (segPF (pP6 P n) (dP6 P n) (sD6 src D i)) (pP6 P n / 7)
(lamP (dP6 P n)) (wF (dP6 P n)) (sD6 src D i) (tD6 P n D i) (αN6 P n)
(fun _ => (0, 0)) = fun _ => (0, 0) := by sorry