S_D on the layer

S_D on the layer.

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

theorem NLogN.KFW.sdQ {σ : Fin HS → Option ℤ} {K S r H P D ρ k q0 Bp Z : ℕ} (lo hi : ℕ)
    (hC : CoreR σ K S r H P D ρ k q0 Bp) (hρ : ρ < K) (hS : 1 ≤ S) (hP : 1 ≤ P) (hr : 1 ≤ r)
    (hD : 1 ≤ D) (hZ16 : zsz ((16 * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Z) :
    SImplQ Isym tbl (fun s => Agree σ s) lo hi r (fun x : Fin D => KFH.stT K D S ρ x)
      (P * 2 ^ (K * D) * S) (Butterfly.SD : Matrix (Fin D → Fin 2) (Fin D → Fin 2) ℂ) sdC 0 0
      (fun w => cSD K S r P D Z w)

Context. The lemma belongs to the part KFW C-layer 7: expression frames and the phase S_D of the layer.

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.