The C-layer

The C-layer.

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

theorem NLogN.KFW.clQ (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) (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)
    {σ : Fin HS → Option ℤ} (hC : CoreR σ K S r H P D ρ k q0 Bp) :
    SImplQ Isym tbl (fun s => Agree σ s) 0 H r (fun x : Fin D => KFH.stT K D S ρ x)
      (P * 2 ^ (K * D) * S) (Butterfly.tens Cm) (clC jT jW) (q0 + lowF ES k (D - q0))
      (2 * q0 + lowF DWl k (D - q0)) (cCL Kc K S r H P D k q0 Bp Z Zr Bz)

Context. The lemma belongs to the part KFW C-layer 9: the C-layer tens Cm on the whole layer: clC jT jW: the top kernels on the bits x < q₀ (level-0 calls, topC from i = 0), then, if q₀ < D, the low bits q₀ ≤ x < D by digit pieces (lowC from j = k, R = D', o = 0) on the layout padded from P 2^{K q₀} to B' blocks (padCU with the frame padL on 17, 18).

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.