Round-six lemma `ljP_sp0`
ProvedJ6Seg.Src.ljP_sp0ljP on a state whose 43 is empty.
The following holds (Lean statement, in the scope of module Solutions.J6SegILSrc5):
theorem J6Seg.Src.ljP_sp0 (s0 : IState HS) (G : Fin HS → List ℤ) {iS iT iL iW : Fin HS} (fS : Free iS)
(fT : Free iT) (fL : Free iL) (fW : Free iW) {s t lam w A : ℕ} {LS LT LL LW : List ℤ}
(hGS : G iS = (s : ℤ) :: LS) (hGT : G iT = (t : ℤ) :: LT) (hGL : G iL = (lam : ℤ) :: LL)
(hGW : G iW = (w : ℤ) :: LW) (h43 : G 43 = []) (hs : 0 < s) (hl : 0 < lam)
(hsA : s ≤ 2 ^ A) (htA : t ≤ 2 ^ A) (hlA : lam ≤ 2 ^ A) (hwA : w ≤ 2 ^ A) (hA : 2 ≤ A) :
Sp (ljP iS iT iL iW) (encK s0 G) (encK s0 (J6Seg.Src.bS G (G 13) (G 14) (G 15)
(ljD s t lam w 0 ++ G 30) (((ljL s t lam w 0).length : ℤ) :: G 31) (J6Seg.Src.stD s t lam 0 ++ G 32)
(lnD s t lam 0 ++ G 33) [] (G 44))) (ljCost s A)
Context. B-line IL, source-table producers, part 5: ljP assembled
ljP iS iT iL iW is a plain RS program (no mulC calls).
Inputs (tops of the named stacks, which must be Free, i.e. < 56 and not one of
13, 14, 15, 30, 31, 32, 33, 43, 44): s on iS, t on iT, λ on iL, w on iW;
0 < s, 0 < λ, and s, t, λ, w ≤ 2^A with 2 ≤ A.
Outputs (prepended, head = index 0):
30:LJ = Jlist (mkBlocks s t λ w)(= J6Seg.LJ s t λ w), increasing;31:|LJ|;32:STL = (range s).map (stF s t λ);33:LNL = (range s).map (fun i => 1 + enF s t λ (stF s t λ i)).
Scratch 14, 15, 43 is pushed and popped; every other stack is unchanged; nothing ≥ 56
other than expression scratch is touched. Theorem ljP_sp, cost ljCost s A.
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_Defs65 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg J6Seg.Src set_option maxRecDepth 20000 open IntMul NLogN NLogN.KIL Function NLogN.RS J6Seg.PreT J6Seg
theorem J6Seg.Src.ljP_sp0 (s0 : IState HS) (G : Fin HS → List ℤ) {iS iT iL iW : Fin HS} (fS : Free iS)
(fT : Free iT) (fL : Free iL) (fW : Free iW) {s t lam w A : ℕ} {LS LT LL LW : List ℤ}
(hGS : G iS = (s : ℤ) :: LS) (hGT : G iT = (t : ℤ) :: LT) (hGL : G iL = (lam : ℤ) :: LL)
(hGW : G iW = (w : ℤ) :: LW) (h43 : G 43 = []) (hs : 0 < s) (hl : 0 < lam)
(hsA : s ≤ 2 ^ A) (htA : t ≤ 2 ^ A) (hlA : lam ≤ 2 ^ A) (hwA : w ≤ 2 ^ A) (hA : 2 ≤ A) :
Sp (ljP iS iT iL iW) (encK s0 G) (encK s0 (J6Seg.Src.bS G (G 13) (G 14) (G 15)
(ljD s t lam w 0 ++ G 30) (((ljL s t lam w 0).length : ℤ) :: G 31) (J6Seg.Src.stD s t lam 0 ++ G 32)
(lnD s t lam 0 ++ G 33) [] (G 44))) (ljCost s A) := by sorry