The inner body (round six, `tsB`)
ProvedJ6Seg.PJ.Rn.tsBThe inner body.
The following holds (Lean statement, in the scope of module Solutions.J6SegILPreJK2):
theorem J6Seg.PJ.Rn.tsB (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hu : BV W u)
(h1 : u 1 = c) (h2 : u 2 = n) (h3 : u 3 = uu) (h4 : u 4 = k) (h7 : u 7 = a) (h24 : u 24 = lam)
(h26 : u 26 = w) (h9 : u 9 = 2 ^ Q) (h10 : u 10 = 2 ^ (Q + 1))
(hca : c ≤ a) (hua : a - c < n) (huu : uu < n) (hk : k < n) (hnl : n ≤ lam) (hlN : lam ≤ N)
(hAP : D SAP = ((List.range n).map (T.ap c)).reverse)
(hAM : D SAM = ((List.range n).map (T.am c)).reverse)
(hGM : D SGM = ((List.range lam).map T.gam).reverse)
(bAP : ∀ i < n, |T.ap c i| ≤ 2 ^ W) (bAM : ∀ i < n, |T.am c i| ≤ 2 ^ W)
(bGM : ∀ i < lam, |T.gam i| ≤ 2 ^ W)
(bS : |u 8 + tsT Q T c (tU w n (a - c) uu) (tV w n (a - c) uu) k| ≤ 2 ^ W) :
Rn (progL PJ.tsB) u D (fun v' =>
v' 8 = u 8 + tsT Q T c (tU w n (a - c) uu) (tV w n (a - c) uu) k ∧
(∀ j ∉ ([5, 8, 11, 12, 29] : List (Fin HS)), v' j = u j) ∧ BV W v') D (costL W N PJ.tsB)
Context. B5 J side, part K2: the TsumI inner loop
Stacks: SAP = 38, SAM = 39 (the block's a⁺, a⁻ lists, reversed), SGM = 36 (Γ,
reversed, length λ). Body PJ.tsB (step k on 4): read a⁺_{k-tU}, a⁻_{k-tV}, Γ_k and
add the TsumI summand to 8 (Rn.tsB); the loop PJ.tsL = forL 51 2 4 PJ.tsB sums it over
k < n (Rn.tsL).
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_Defs70
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6Seg J6Seg.PJ
open IntMul NLogN NLogN.KIL NLogN.RS Function J6Seg.PJ.E
variable {Q W N : ℕ} {T : Tables} {u : Vr} {D : Cs} {c n a uu k lam w : ℕ}
theorem J6Seg.PJ.Rn.tsB (hN : N ≤ 2 ^ W) (hW2 : 2 ≤ W) (hu : BV W u)
(h1 : u 1 = c) (h2 : u 2 = n) (h3 : u 3 = uu) (h4 : u 4 = k) (h7 : u 7 = a) (h24 : u 24 = lam)
(h26 : u 26 = w) (h9 : u 9 = 2 ^ Q) (h10 : u 10 = 2 ^ (Q + 1))
(hca : c ≤ a) (hua : a - c < n) (huu : uu < n) (hk : k < n) (hnl : n ≤ lam) (hlN : lam ≤ N)
(hAP : D SAP = ((List.range n).map (T.ap c)).reverse)
(hAM : D SAM = ((List.range n).map (T.am c)).reverse)
(hGM : D SGM = ((List.range lam).map T.gam).reverse)
(bAP : ∀ i < n, |T.ap c i| ≤ 2 ^ W) (bAM : ∀ i < n, |T.am c i| ≤ 2 ^ W)
(bGM : ∀ i < lam, |T.gam i| ≤ 2 ^ W)
(bS : |u 8 + tsT Q T c (tU w n (a - c) uu) (tV w n (a - c) uu) k| ≤ 2 ^ W) :
Rn (progL PJ.tsB) u D (fun v' =>
v' 8 = u 8 + tsT Q T c (tU w n (a - c) uu) (tV w n (a - c) uu) k ∧
(∀ j ∉ ([5, 8, 11, 12, 29] : List (Fin HS)), v' j = u j) ∧ BV W v') D (costL W N PJ.tsB) := by sorry