The layer body

The layer body.

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

theorem NLogN.KFW.bodyQ (jT jL jW : Fin Pp) (rowC : IStmt HS Pp) (hT : tbl jT = NLogN.KFW.topC jT jL)
    (hW : tbl jW = lowC jW jL) (hL : tbl jL = levC jL rowC)
    {K S r H P D ρ k q0 Bp Z Zr Mb Bz : ℕ} {Kc : ℝ}
    (LV : ∀ j, LvQ Isym tbl jL rowC K r Z Zr H j (cbW Kc K j))
    (hρ : ρ < K) (hS : 1 ≤ S) (hP : 1 ≤ P) (hr : 1 ≤ r) (hD : 1 ≤ D) (hq : q0 ≤ D)
    (hZ16 : zsz ((16 * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Z)
    (hV : zsz ((Vb K (K * D) S r H 0 P : ℕ) : ℤ) ≤ Zr)
    (hMb : zsz (Mb : ℤ) ≤ Bz) (hM : K * D + P + 10 ≤ Mb)
    (pre : q0 < D → LowPre K S r H P D ρ k q0 Bp Z Zr Mb Bz)
    (hEZ : zsz (((q0 + lowF ES k (D - q0) + (D / 2 + D % 2)) : ℕ) : ℤ) ≤ Z)
    {σ : Fin HS → Option ℤ} (hC : CoreR σ K S r H P D ρ k q0 Bp)
    (hE : σ 24 = some (((q0 + lowF ES k (D - q0) + (D / 2 + D % 2)) : ℕ) : ℤ))
    (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ) (xs : List (Fin r → ℂ)) (p w : ℕ)
    (hC0 : Clean0 f) (h0 : f 0 = gflat zs ++ l) (hx : RecRep r p zs xs)
    (hl : xs.length = vol (Butterfly.layerShape P K D S)) (hb : NLogN.KFB.GB w zs)
    (hH : w + (2 * q0 + lowF DWl k (D - q0) + 2) ≤ H)
    (hdisk : ∀ j (h : j < xs.length), ‖xs[j]‖ ≤ 1) :
    ∃ zs', RecRep r p zs' (Butterfly.prop14Proc (P := P) (S := S) hρ p
        (Butterfly.tens Butterfly.Cm : Butterfly.Op (Fin D)) xs) ∧
      NLogN.KFB.GB (p + 1) zs' ∧
      (∀ j (h : j < (Butterfly.prop14Proc (P := P) (S := S) hρ p
          (Butterfly.tens Butterfly.Cm : Butterfly.Op (Fin D)) xs).length)
        (h' : j < (Butterfly.layerH P K D S ρ hρ xs).length), ∀ c,
        ‖(Butterfly.prop14Proc (P := P) (S := S) hρ p
          (Butterfly.tens Butterfly.Cm : Butterfly.Op (Fin D)) xs)[j] c -
          (Butterfly.layerH P K D S ρ hρ xs)[j] c‖ < Real.sqrt 2 * 2⁻¹ ^ p) ∧
      RunQ Isym tbl σ (NLogN.KFW.bodyC jT jW) f (Function.update f 0 (gflat zs' ++ l))
        (NLogN.KFW.cBody Kc K S r H P D k q0 Bp Z Zr Bz w)

Context. The lemma belongs to the part KFW C-layer 10: the layer body S_D ; C ; S_D ; b^D ; Q_p: With the core registers and the total scale E = q₀ + lowF ES k D' + ⌊D/2⌋ + D mod 2 on register 24, the fixed code bodyC jT jW runs the uniform S_D (sdC), the C-layer (clC), S_D, the scalar b^D (mdC), and the truncation truncU 17 18 (frame 17 = 2^E, 18 = 2 N).

Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the uniform item-language machine (register programs over the NLogN multitape framework) assembling the Proposition 14 / Lemma 13 / Proposition 18 pieces, the resampling and chirp stages and the cost recurrences into one fixed machine, culminating in NLogN.KFTop.kappa_bound : IntMul.KappaBound (1 / 2 ^ 182) (the bound of Def_IntMul_MultitapeModel). All names refer to the definition bundles up to IntMul_Kappa_K_Defs33.