The uniform prog_il (the KIL4_WIP target prog_il_uniform, in the form proved here): one fixed procedure…

The uniform prog_il (the KIL4_WIP target prog_il_uniform, in the form proved here): one fixed procedure table and constants, independent of q, k, P, L, A, B, Cs, the bit size Bb and the input.

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

theorem NLogN.KIL.prog_il_uniform5 (hm : 1 ≤ m) :
    ∃ (iprog : Fin 1 → IStmt HS 1) (K Kd S : ℕ), iprog = progU C tpl ∧
      ∀ (q : ℕ), 2 ≤ q → ∀ (Bb k : ℕ), (∀ j < k, LvOK C tpl (q ^ m ^ j) Bb) →
      zsz (k : ℤ) ≤ Bb →
      ∀ (P L : ℕ) (A B Cs : Shape), 1 ≤ P → W ^ k ∣ L → 1 ≤ L →
      (∀ a ∈ A, 1 ≤ a) → (∀ a ∈ B, 1 ≤ a) → (∀ a ∈ Cs, 1 ≤ a) →
      zsz ((vol (P :: L :: swShape A B Cs (q ^ m ^ k)) : ℕ) : ℤ) ≤ Bb →
      ∀ (I : List Sym) (t : IState HS) (R : List Item) (xs : List (ZMod 2)),
        DescIn t q m k P L A B Cs →
        xs.length = vol (P :: L :: swShape A B Cs (q ^ m ^ k)) →
        IRuns I iprog (iprog 0) (t.upd 0 (ints (enc2 xs) ++ R))
          (t.upd 0 (ints (enc2 (AModel.prog C q k P L A B Cs xs)) ++ R))
          (ilCostU5 W K Kd S q Bb k (vol (P :: L :: swShape A B Cs (q ^ m ^ k))))

Context. The lemma belongs to the part KIL5: the uniform prog_il: progU_run: the single fixed procedure progU C tpl (KIL5Prog; it depends only on the circuit C and the template function tpl) computes prog C q k P L A B Cs at every level k, for every q, P, L, A, B, Cs and input, from any state carrying the descriptor (DescIn), with cost ilCostU5 (constants Klev C tpl + 10⁹, Kd m, SWn C tpl, independent of q, k and the sizes).

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.