The call wrapper

The call wrapper. If the procedure j0 maps every state carrying the child descriptor (level k, P, L', the child shapes, the tower towerL q m k) to the state with the child's array, then swC m j0 a b does so on the level's state.

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

theorem NLogN.KIL.swC_runs {q m k P L' N : ℕ} {A B Cs : Shape} (a b : ℕ) (ha : a < m) (hb : m ≤ b)
    (hb' : b < m + m) (j0 : Fin Pp) (ch : List (ZMod 2) → List (ZMod 2)) (c0 : ℕ)
    (hrec : ∀ (t' : IState HS) (R' : List Item) (ys : List (ZMod 2)),
      DescIn t' q m k P L' (A ++ List.replicate a N)
        (List.replicate (m - 1 - a) N ++ (B ++ List.replicate (b - m) N))
        (List.replicate (m + m - 1 - b) N ++ Cs) →
      ys.length = vol (P :: L' :: hdShape A B Cs m N) →
      IRuns I iprog (iprog j0) (t'.upd 0 (ints (enc2 ys) ++ R'))
        (t'.upd 0 (ints (enc2 (ch ys)) ++ R')) c0)
    (Bb : ℕ) (hN : 1 ≤ N) (hpos : ∀ x ∈ P :: L' :: hdShape A B Cs m N, 1 ≤ x)
    (hV : zsz ((vol (P :: L' :: hdShape A B Cs m N) : ℕ) : ℤ) ≤ Bb) (hk : zsz (k : ℤ) ≤ Bb)
    (t : IState HS) {L1 L2 L3 L4 L5 L6 L7 L8 : List Item}
    (hJ1 : t.G rJ1 = .int (k : ℤ) :: L1) (hLp : t.G rLp = .int (L' : ℤ) :: L2)
    (hVA : t.G rVA = .int ((vol A : ℕ) : ℤ) :: L3) (hVB : t.G rVB = .int ((vol B : ℕ) : ℤ) :: L4)
    (hVC : t.G rVC = .int ((vol Cs : ℕ) : ℤ) :: L5) (hQQ : t.G sQQ = .int (N : ℤ) :: L6)
    (hP : t.G NLogN.KIL.dP = .int (P : ℤ) :: L7) (hT : t.G dT = ints (towerL q m k) ++ L8)
    (R : List Item) (ys : List (ZMod 2)) (hys : ys.length = vol (P :: L' :: hdShape A B Cs m N)) :
    IRuns I iprog (NLogN.KIL.swC m j0 a b) (t.upd 0 (ints (enc2 ys) ++ R))
      (t.upd 0 (ints (enc2 (ch ys)) ++ R)) (cSwC m a b Bb c0)

Context. The lemma belongs to the part KIL5: the uniform frame change (template lists, child calls through the descriptor).

Formalization Note. This lemma belongs to the item-language (IL) layer of the integer-multiplication-kappa campaign: tape-level programs (register programs over 64 item stacks of the NLogN multitape framework, definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8) that implement the data-movement primitives of the OpenAI preprint Integer multiplication below $n\log n$ (field moves, row split/merge, shifts, the uniform Proposition 11 interchange, Lemma 12 with fine $O(1)$-per-element costs, Gaussian record primitives, Proposition 14 pieces) with exact list denotations from the array-model bundles IntMul_Kappa_K_Defs* and explicit cost bounds. All names refer to the definition bundles up to IntMul_Kappa_K_Defs18.