preA_sp (KIL6: the run-time descriptor)

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

theorem NLogN.KIL.preA_sp (s : IState HS) (F : Fin HS → List ℤ) {M B : ℕ} (hM : zsz (M : ℤ) ≤ B)
    {q m W u P g sv : ℕ} (hq : 2 ≤ q) (hm : 2 ≤ m)
    (FP : ∃ L, F kP = (P : ℤ) :: L) (FG : ∃ L, F kG = (g : ℤ) :: L)
    (FS : ∃ L, F NLogN.KIL.kS = (sv : ℤ) :: L) (FU : ∃ L, F aU = (u : ℤ) :: L) (hg : 1 ≤ g)
    (F23 : F 23 = [])
    (hM1 : 2 ^ u + q ≤ M) (hM4 : Nat.clog q (2 ^ u) + m ≤ M) (hM6 : W * Nat.clog q (2 ^ u) ≤ M)
    (hM6' : W ≤ M) (hM7 : g * q ^ Nat.clog q (2 ^ u) ≤ M) :
    ∃ v : Fin HS → ℕ, (∀ i ∈ regD, v i ≤ M) ∧ v kP = P ∧ v kG = g ∧ v NLogN.KIL.kS = sv ∧ v aU = u ∧
      v aT2 = 2 ^ u ∧ v NLogN.KIL.aE = Nat.clog q (2 ^ u) ∧ v aQE = q ^ Nat.clog q (2 ^ u) ∧
      v aK = Nat.clog m (Nat.clog q (2 ^ u)) ∧
      v kR = min (W * Nat.clog m (Nat.clog q (2 ^ u))) (Nat.clog q (2 ^ u)) ∧
      v aN = Nat.clog q (2 ^ u) - min (W * Nat.clog m (Nat.clog q (2 ^ u))) (Nat.clog q (2 ^ u)) ∧
      v aQR = q ^ min (W * Nat.clog m (Nat.clog q (2 ^ u))) (Nat.clog q (2 ^ u)) ∧
      v aQN = q ^ (Nat.clog q (2 ^ u) -
        min (W * Nat.clog m (Nat.clog q (2 ^ u))) (Nat.clog q (2 ^ u))) ∧
      v aGR = g * q ^ min (W * Nat.clog m (Nat.clog q (2 ^ u))) (Nat.clog q (2 ^ u)) ∧
      v kQt = q ^ 0 ∧ v kQr = q ^ (Nat.clog q (2 ^ u) - 0) / q ∧
      Sp (preA q m W) (encK s F) (encK s (regState F v regD)) (cPreA u (Nat.clog q (2 ^ u)) B)

Context. The lemma belongs to the part KIL6: the run-time descriptor: preA q m W: create the register file and compute 2^u, e = ⌈log_q 2^u⌉, q^e, Kp = ⌈log_m e⌉, r = min (W·Kp) e, n = e - r, q^r, q^n, vol G · q^r and the swap registers.

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.