Lemma 12 as a uniform item-language program (oracle: the uniform Prop. 11 code)

Lemma 12 as a uniform item-language program (oracle: the uniform Prop. 11 code).

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

theorem NLogN.KIL.l12_il_uniform_rat (Qc : QCircuit (ZMod 2) m W) (hm : 2 ≤ m) :
      ∀ (q : ℕ), q.Prime → ∀ (Bb u : ℕ) (Pre G Suf : Shape), 1 ≤ u →
      (∀ a ∈ Pre, 1 ≤ a) → (∀ a ∈ G, 1 ≤ a) → (∀ a ∈ Suf, 1 ≤ a) →
      ∀ e Kp : ℕ, e = Nat.clog q (2 ^ u) → Kp = Nat.clog m e →
      (∀ j < Kp, FramesOK (fun X => GoodAtQ q ((Qc.den : ℚ)⁻¹ • ratM X) ∧
        ∀ T, TStep.sh T ∈ edgeTplQ Qc X → TOK T (q ^ m ^ j) Bb)
        (Qc.toCircuit (q ^ m ^ Kp)).gates (Qc.toCircuit (q ^ m ^ Kp)).Min
        (Qc.toCircuit (q ^ m ^ Kp)).Mout) →
      (∀ j < Kp, SubBnd (q ^ m ^ j) Bb) →
      zsz (((2 * vol (qShape Pre G Suf q e) + m + W * e : ℕ)) : ℤ) ≤ Bb → 1 ≤ Bb →
      ∀ (I : List Sym) (s : IState HS) (F : Fin HS → List ℤ) (xs : List (ZMod 2))
        (LP LG LS LU : List ℤ),
      F kP = (vol Pre : ℤ) :: LP → F kG = (vol G : ℤ) :: LG → F NLogN.KIL.kS = (vol Suf : ℤ) :: LS →
      F aU = (u : ℤ) :: LU → F 0 = enc2 xs →
      F 8 = [] → F 9 = [] → F 10 = [] → F 11 = [] → F 15 = [] → F 20 = [] → F 21 = [] →
      F 23 = [] → F 24 = [] →
      xs.length = vol (binShape Pre G Suf (2 ^ u)) →
      IRuns I (progU (Qc.toCircuit 1) (edgeTplQ Qc)) (l12I q m W) (encK s F)
        (encK s (Function.update F 0 (enc2 (l12v (normO (AModel.prog (Qc.toCircuit (q ^ m ^ Kp)) q))
          W m q Kp (W * Kp) e u Pre G Suf 0 xs))))
        (cL12 u e (min (W * Kp) e) Kp (e - min (W * Kp) e) (vol (qShape Pre G Suf q e))
          (vol (rowShape (vol Pre) (padRows W Kp (q ^ min (W * Kp) e))
            (G ++ List.replicate (min (W * Kp) e) q) Suf q (e - min (W * Kp) e))) m q
          (fun j => ilCostU5 W (Klev (Qc.toCircuit 1) (edgeTplQ Qc) + 10 ^ 9) (Kd m)
            (SWn (Qc.toCircuit 1) (edgeTplQ Qc)) q Bb j
            (vol (rowShape (vol Pre) (padRows W Kp (q ^ min (W * Kp) e))
              (G ++ List.replicate (min (W * Kp) e) q) Suf q (e - min (W * Kp) e)))) Bb)

Context. The lemma belongs to the part KIL6: the Lemma 12 program with the Prop. 11 code as oracle: The oracle code is the uniform Prop. 11 program of KIL5 (prog_il_uniform_rat, i.e. progU (Qc.toCircuit 1) (edgeTplQ Qc)). Its denotation at the levels used is prog (Qc.toCircuit (q ^ m ^ Kp)) q. The variant denotation l12v is taken with the length-normalised oracle normO (equal to the oracle on every call of the procedure, see normO_eq; it only serves to state the uniform length invariant).

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.