The constructed tables are accurate (round six, `mkTables_ok`)
ProvedJ6Seg.mkTables_okThe constructed tables are accurate (TabOK with E = 3λ + 3, Dm = D_{λ-1}).
The following holds (Lean statement, in the scope of module Solutions.J6SegTab):
theorem J6Seg.mkTables_ok (hs : 0 < s) (hst : s ≤ t) (hα : 2 ≤ α) (hP : 1 ≤ P) {lam : ℕ}
(hl : 1 ≤ lam) (hPl : 200 * (3 * (lam : ℝ) + 1) ≤ 2 ^ P)
(hR : ddR (α : ℝ) ((t : ℝ) / s) (lam - 1) ≤ 2 ^ R) (B : Blocks)
(hlen : ∀ i < s, B.len i ≤ lam) :
TabOK P s t α B (mkTables P R s t α) (3 * lam + 3) (ddR (α : ℝ) ((t : ℝ) / s) (lam - 1))
Context. Segmented inverse (S2): construction of the constant tables
mkTables P R s t α (computable) fills the tables of J6SegAlg with
di u = expNeg P s (α²(t-s)u²)(≈ 2^P e^{-πα²θu²}),dd u = expPos (P+R) s (α²(t-s)u²) R(≈ 2^P e^{πα²θu²}, needse^{πα²θu²} ≤ 2^R),gam:(q;q)_uby the recurrenceΓ_{u+1} = Γ_u (1 - q^{u+1})(q^kbyexpNeg),gi u = 2^P / Γ_u(fdiv),ap/am c h = (-1)^h e^{-πα²(σ ± 2β_c)h} / Γ_h,cpl i h = expNeg P s² (α² K_{i,h})(the entries ofE, as inEapprox).
mkTables_ok: TabOK with E = 3λ + 3 and Dm = D_{λ-1}, for blocks of length ≤ λ, as soon as
200 (3λ+1) ≤ 2^P and D_{λ-1} ≤ 2^R.
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 Real
open IntMul.HvdH IntMul.HvdH.JPf J6QLU
variable {P R s t α : ℕ}
theorem J6Seg.mkTables_ok (hs : 0 < s) (hst : s ≤ t) (hα : 2 ≤ α) (hP : 1 ≤ P) {lam : ℕ}
(hl : 1 ≤ lam) (hPl : 200 * (3 * (lam : ℝ) + 1) ≤ 2 ^ P)
(hR : ddR (α : ℝ) ((t : ℝ) / s) (lam - 1) ≤ 2 ^ R) (B : Blocks)
(hlen : ∀ i < s, B.len i ≤ lam) :
TabOK P s t α B (mkTables P R s t α) (3 * lam + 3) (ddR (α : ℝ) ((t : ℝ) / s) (lam - 1)) := by sorry