One Prop. 11 level as IL code, any fixed unit coefficients (bit data)

One Prop. 11 level as IL code, any fixed unit coefficients (bit data). For a fixed circuit over ZMod 2 whose frame changes have 0/1 permutation parts and whose Lemma 10 shifts have coefficients ±k·d⁻¹ with k, d ≤ D prime to N, there is a constant K (depending on the circuit and D) such that for all sizes the level is an IL statement calling the child procedures, computing levelR, with cost K · (V + 1) · (Bb + 2)² + rankSum C · (c₀ + 2).

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

theorem NLogN.KIL.levelR_il_frac (D : ℕ) (hN : 1 < N)
    (hfr : FramesOK (FrOK C N (ShFrac N D)) C.gates C.Min C.Mout) :
    ∃ K : ℕ, ∀ (P L' : ℕ), (∀ a ∈ P :: L' :: hdShape A B Cs m N, 1 ≤ a) →
      ∀ {Pp : ℕ} (I : List Sym) (iprog : Fin Pp → IStmt HS Pp)
      (jOf : Fin (m + m) → Fin (m + m) → Fin Pp)
      (child : Fin (m + m) → Fin (m + m) → List (ZMod 2) → List (ZMod 2)) (c0 Bb : ℕ),
      (∀ (i j : Fin m) (t : IState HS) (R : List Item) (ys : List (ZMod 2)),
        ys.length = vol (P :: L' :: hdShape A B Cs m N) →
        IRuns I iprog (iprog (jOf (Fin.castAdd m i) (Fin.natAdd m j)))
          (t.upd 0 (ints (enc2 ys) ++ R))
          (t.upd 0 (ints (enc2 (child (Fin.castAdd m i) (Fin.natAdd m j) ys)) ++ R)) c0 ∧
        (child (Fin.castAdd m i) (Fin.natAdd m j) ys).length =
          vol (P :: L' :: hdShape A B Cs m N)) →
      zsz ((vol (P :: W * L' :: hdShape A B Cs m N) : ℕ) : ℤ) ≤ Bb →
      zsz ((2 * N : ℕ) : ℤ) ≤ Bb →
      ∃ code : IStmt HS Pp, ∀ (t : IState HS) (R : List Item) (xs : List (ZMod 2)),
        xs.length = vol (P :: W * L' :: hdShape A B Cs m N) →
        IRuns I iprog code (t.upd 0 (ints (enc2 xs) ++ R))
          (t.upd 0 (ints (enc2 (levelR C N P L' A B Cs child xs)) ++ R))
          (K * ((vol (P :: W * L' :: hdShape A B Cs m N) + 1) * (Bb + 2) ^ 2) +
            rankSum C * (c0 + 2))

Context. The lemma belongs to the part KIL3: one Prop. 11 level with arbitrary fixed unit coefficients: The level code of KIL3Level with the shift code scodeF: a shift step with coefficient u = ±k·d⁻¹ runs shFrac (KIL3Unit). Every unit of ZMod N that is (the image of) a fixed fraction ±k/d with k, d ≤ D prime to N is handled (FracUnit D N u), so the constant K depends only on the circuit and D.

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.