The Toeplitz stage in IL (round six, `tsI_runs`)

The Toeplitz stage in IL.

The following holds (Lean statement, in the scope of module Solutions.J6SegKr4):

theorem J6Seg.KR.tsI_runs {M : MulSpec} {pM : Fin Pp} (hM : MulOK I iprog pM M) (hdom : ∀ x y, M.dom x y)
    {b n pk φ : ℕ} (hΦ : ∀ x y : ℤ, zsz x ≤ b * (2 * n) + 2 → zsz y ≤ b * (2 * n) + 2 → M.Φ x y ≤ φ)
    (hb : 1 ≤ b) (hn1 : 1 ≤ n) (hbig : 2 * (2 * n) * 2 ^ (2 * pk) < 2 ^ (b - 1))
    {IN OUTS : Fin HS} (hIO : (IN = W1 ∧ OUTS = J6Seg.KR.W2) ∨ (IN = J6Seg.KR.W2 ∧ OUTS = W1))
    (P : ℕ) (s : IState HS) (F : Fin HS → List ℤ) (t : List GI) (am lin ldt l1 l2 ln ln2 : List ℤ)
    (hIN : F IN = gflat t.reverse ++ lin) (ht : t.length = n)
    (hdT : F J6Seg.KR.dT = am ++ ldt) (ham : am.length = n)
    (hbN : F bN = (n : ℤ) :: ln) (hbN2 : F bN2 = ((2 * n : ℕ) : ℤ) :: ln2)
    (hX : F vX = []) (hY : F vY = []) (hO : F vO = []) (hT : Tmp F)
    (hpc : F kc = [2 ^ pk]) (hpr : F kr = [((2 * n : ℕ) : ℤ)]) (hpK : F kK = [NLogN.KFV.kG b (2 * n) (2 ^ pk)])
    (hpB : F kB = [2 ^ b]) (hpJ : F kJ = [(2 ^ b) ^ (2 * (2 * n))]) (hpD : F kD = [1])
    (hP : F J6Seg.KR.rP = 2 ^ P :: l1) (hQ : F rP1 = 2 ^ (P + 1) :: l2)
    (htb : ∀ z ∈ t, |z.1| ≤ 2 ^ pk ∧ |z.2| ≤ 2 ^ pk) (hab : ∀ a ∈ am, |a| ≤ 2 ^ pk)
    (B : ℕ) (hBb : b + 4 ≤ B) (hBp : pk + 2 ≤ B) (hPB : P + 3 ≤ B)
    (hBn : zsz ((2 * n : ℕ) : ℤ) ≤ B) :
    IRuns I iprog (tsI pM IN OUTS) (encK s F)
      (encK s (Function.update (Function.update (Function.update (Function.update F IN lin) OUTS
        (gflat (lwG P (2 * n) am t) ++ F OUTS)) J6Seg.KR.dT ldt) DU (am.reverse ++ F DU)))
      (cTS n pk b φ B)

Context. B3 (chunk kernel), part 4: the Toeplitz stage

tsI pM IN OUTS: with n on bN, 2n on bN2, a Gaussian block t (reversed, gflat t.reverse) on IN, the real table am (length n) on top of the table stack dT, and the record-product parameters for records of length r = 2n on the parameter stacks 50 … 55 (managed), it leaves gflat (lwG P (2n) am t) on OUTS, consumes am from dT onto the stack DU of consumed descriptors, and uses one uniform Kronecker record product (recU, Δ = 0).

The parameter stacks are managed lists here; around recU they are moved into the base state (encK_split).

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*).