The line tables (round six, `tabP`)
ProvedJ6Seg.PJ.Rn.tabPThe line tables di, dd, Γ, Γ⁻¹, reversed, on SDI, SDD, SGM, SGI.
The following holds (Lean statement, in the scope of module Solutions.J6SegILPreJK12):
theorem J6Seg.PJ.Rn.tabP (hc : c PreT.Cu = []) (hi : PreT.StIn2 v Q R s t lam α W) (hQW : Q ≤ W)
(hDI : c SDI = []) (hDD : c SDD = []) (hGM : c SGM = []) (hGI : c SGI = [])
(bdi : ∀ k < lam, |(mkTables Q R s t α).di k| ≤ 2 ^ W)
(bdd : ∀ k < lam, |(mkTables Q R s t α).dd k| ≤ 2 ^ W)
(bq : ∀ k < lam, |HvdH.expNeg Q s (2 * α ^ 2 * t * (k + 1))| ≤ 2 ^ W)
(bG : ∀ k ≤ lam, |gamI Q s t α k| ≤ 2 ^ W)
(bI : ∀ k < lam, |giI Q s t α k| ≤ 2 ^ W) :
Rn J6Seg.PJ.tabP v c (fun v' => Fxk [4, 5, 11, 12] v v' ∧ BV W v')
(update (update (update (update c SDI (diL Q R s t lam α).reverse) SDD
(ddL Q R s t lam α).reverse) SGM (gamL Q R s t lam α).reverse) SGI
(giL Q R s t lam α).reverse) (cTabP W Q R lam)
Context. B5 J side, part K12: the line tables as Rn steps
stG_spX: stG_sp (J6SegILPre8) with the final registers explicit (stGV); the table stage
tabP = stDI SDI; stDD SDD; stGam SGM; stGi SGI (Rn.tabP).
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_Defs71
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6Seg J6Seg.PJ
open IntMul NLogN NLogN.KIL NLogN.RS Function
variable {W Q R s t lam α : ℕ} {v : Vr} {c : Cs}
theorem J6Seg.PJ.Rn.tabP (hc : c PreT.Cu = []) (hi : PreT.StIn2 v Q R s t lam α W) (hQW : Q ≤ W)
(hDI : c SDI = []) (hDD : c SDD = []) (hGM : c SGM = []) (hGI : c SGI = [])
(bdi : ∀ k < lam, |(mkTables Q R s t α).di k| ≤ 2 ^ W)
(bdd : ∀ k < lam, |(mkTables Q R s t α).dd k| ≤ 2 ^ W)
(bq : ∀ k < lam, |HvdH.expNeg Q s (2 * α ^ 2 * t * (k + 1))| ≤ 2 ^ W)
(bG : ∀ k ≤ lam, |gamI Q s t α k| ≤ 2 ^ W)
(bI : ∀ k < lam, |giI Q s t α k| ≤ 2 ^ W) :
Rn J6Seg.PJ.tabP v c (fun v' => Fxk [4, 5, 11, 12] v v' ∧ BV W v')
(update (update (update (update c SDI (diL Q R s t lam α).reverse) SDD
(ddL Q R s t lam α).reverse) SGM (gamL Q R s t lam α).reverse) SGI
(giL Q R s t lam α).reverse) (cTabP W Q R lam) := by sorry