Round-six lemma `out_step`
ProvedJ6Seg.Src.out_stepAn auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.
The following holds (Lean statement, in the scope of module Solutions.J6SegILSrc8):
theorem J6Seg.Src.out_step (s0 : IState HS) (G : Fin HS → List ℤ) {iP iS iT iA : Fin HS} (fP : Free7 iP)
(fS : Free7 iS) (fT : Free7 iT) (fA : Free7 iA) {p s t α A : ℕ} {LP LS LT LA : List ℤ}
(hGP : G iP = (p : ℤ) :: LP) (hGS : G iS = (s : ℤ) :: LS) (hGT : G iT = (t : ℤ) :: LT)
(hGA : G iA = (α : ℤ) :: LA) (hs : 0 < s) (ha : 1 ≤ α) (hpA : p ≤ 2 ^ A) (hsA : s ≤ 2 ^ A)
(htA : t ≤ 2 ^ A) (haA : α ≤ 2 ^ A) (hA : 2 ≤ A)
(hdA : ∀ l < s, |dTilde p s t α l| ≤ 2 ^ A)
{n' j : ℕ} (hj : j < n') (hjA : j + 1 ≤ 2 ^ A) :
Sp (outB iP iS iT iA)
(encK s0 (tbS G [(j : ℤ) + 1] (tlT (fun l => some l) (argO p s t α) n' (j + 1) ++ G 44)))
(encK s0 (tbS G [(j : ℤ) + 1] (tlT (fun l => some l) (argO p s t α) n' j ++ G 44)))
(c7 A p α)
Context. B-line IL, source-table producers, part 8: pass 7 (argO, the d̃_l values)
outP iP iS iT iA iN: src = some, argOf = argO p s t α (d̃_l = dTilde p s t α l for
l < s, else 0), n' on iN; each entry with l < s calls the library program expPosP
(callB, which uses 16, 17, 18, 19, 27 and restores them) with inputs p, s²,
α² · kOf s t l (the rounding residue b = t l - s · rowSel l is first pushed on 13), and
2α² - 2.
Inputs: p on iP, s on iS, t on iT, α on iA, n' on iN, all Free7 (Free
and not 16, 17, 18, 19, 27); 0 < s, 1 ≤ α, all ≤ 2^A, 2 ≤ A, and
|d̃_l| ≤ 2^A for l < s. Output: 44 := srcTab some (argO p s t α) n' ++ F 44.
Theorem outP_sp, cost (n' + 1) * (c7 A p α + uC A DD).
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 IntMul.HvdH open J6Seg.Slab (srcTab argO)
theorem J6Seg.Src.out_step (s0 : IState HS) (G : Fin HS → List ℤ) {iP iS iT iA : Fin HS} (fP : Free7 iP)
(fS : Free7 iS) (fT : Free7 iT) (fA : Free7 iA) {p s t α A : ℕ} {LP LS LT LA : List ℤ}
(hGP : G iP = (p : ℤ) :: LP) (hGS : G iS = (s : ℤ) :: LS) (hGT : G iT = (t : ℤ) :: LT)
(hGA : G iA = (α : ℤ) :: LA) (hs : 0 < s) (ha : 1 ≤ α) (hpA : p ≤ 2 ^ A) (hsA : s ≤ 2 ^ A)
(htA : t ≤ 2 ^ A) (haA : α ≤ 2 ^ A) (hA : 2 ≤ A)
(hdA : ∀ l < s, |dTilde p s t α l| ≤ 2 ^ A)
{n' j : ℕ} (hj : j < n') (hjA : j + 1 ≤ 2 ^ A) :
Sp (outB iP iS iT iA)
(encK s0 (tbS G [(j : ℤ) + 1] (tlT (fun l => some l) (argO p s t α) n' (j + 1) ++ G 44)))
(encK s0 (tbS G [(j : ℤ) + 1] (tlT (fun l => some l) (argO p s t α) n' j ++ G 44)))
(c7 A p α) := by sorry