Lemma 12 as a uniform item-language program, correctness: if the oracle denotation is correct (OracleSpec,…

Lemma 12 as a uniform item-language program, correctness: if the oracle denotation is correct (OracleSpec, the conclusion of Prop. 11), the program interchanges the two [2^u] fields of the bit array.

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

theorem NLogN.KIL.l12_il_rat_correct (Qc : QCircuit (ZMod 2) m W) (hm : 2 ≤ m)
    (q : ℕ) (hq : q.Prime) (Bb u : ℕ) (Pre G Suf : Shape) (hu : 1 ≤ u)
    (hPre : ∀ a ∈ Pre, 1 ≤ a) (hG : ∀ a ∈ G, 1 ≤ a) (hS : ∀ a ∈ Suf, 1 ≤ a)
    (e Kp : ℕ) (he : e = Nat.clog q (2 ^ u)) (hKp : Kp = Nat.clog m e)
    (hspec : OracleSpec (AModel.prog (Qc.toCircuit (q ^ m ^ Kp)) q) 0 W m q Kp)
    (hfr : ∀ 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)
    (hsb : ∀ j < Kp, SubBnd (q ^ m ^ j) Bb)
    (hBb : zsz (((2 * vol (qShape Pre G Suf q e) + m + W * e : ℕ)) : ℤ) ≤ Bb) (hB1 : 1 ≤ Bb)
    (I : List Sym) (s : IState HS) (F : Fin HS → List ℤ) (xs : List (ZMod 2))
    (LP LG LS LU : List ℤ)
    (FP : F kP = (vol Pre : ℤ) :: LP) (FG : F kG = (vol G : ℤ) :: LG)
    (FS : F NLogN.KIL.kS = (vol Suf : ℤ) :: LS) (FU : F aU = (u : ℤ) :: LU) (F0 : F 0 = enc2 xs)
    (F8 : F 8 = []) (F9 : F 9 = []) (F10 : F 10 = []) (F11 : F 11 = []) (F15 : F 15 = [])
    (F20 : F 20 = []) (F21 : F 21 = []) (F23 : F 23 = []) (F24 : F 24 = [])
    (hxs : 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 (AModel.pull (binShape Pre G Suf (2 ^ u))
        (binShape Pre G Suf (2 ^ u)) (swapPos Pre.length (Pre.length + 1 + G.length)) 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.