The selection chain
ProvedNLogN.KFW.mdTQThe selection chain.
The following holds (Lean statement, in the scope of module Solutions.KFWC8):
theorem NLogN.KFW.mdTQ {K S r H P D ρ k q0 Bp Z Mb Bz : ℕ} (lo hi : ℕ) (hρ : ρ < K) (hS : 1 ≤ S)
(hP : 1 ≤ P) (hr : 1 ≤ r) (hD : 1 ≤ D)
(hZ16 : zsz ((16 * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Z)
(hMb : zsz (Mb : ℤ) ≤ Bz) (hM : K * D + P + 10 ≤ Mb) :
∀ f j (σ : Fin HS → Option ℤ), CoreR σ K S r H P D ρ k q0 Bp → j ≤ D % 8 → D % 8 ≤ j + f →
j + f ≤ 7 →
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) (tensF (kerAt (⟨0, hD⟩ : Fin D) (Butterfly.cb ^ D • (1 : M2))))
(mdT j f) (D / 2 + D % 2) 2
(fun w => f * cMdT Bz + cMdK (P * 2 ^ (K * D) * S * r) Z Bz w)
Context. The lemma belongs to the part KFW C-layer 8: the scalar b^D by an 8-way selection: MD D = MD (D mod 8) (MD_mod8): the scalar kernel needs only D mod 8 in its code. The fixed
code mdC tests D mod 8 < j + 1 for j = 0 … 6 and runs the kernel qopU [MD j] on chunk 0
of the layer (level frame mdF).
Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below : 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.
-- OpenAI-preprint / κ-improvement development (integer-multiplication-kappa), generated by skeleton subtraction.
import Definitions.Def_IntMul_Kappa_K_Defs33
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unusedSectionVars false
open NLogN
open NLogN.KFW
open IntMul KIL KFD KFB KFG KFH KFN Complex Butterfly
variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}
theorem NLogN.KFW.mdTQ {K S r H P D ρ k q0 Bp Z Mb Bz : ℕ} (lo hi : ℕ) (hρ : ρ < K) (hS : 1 ≤ S)
(hP : 1 ≤ P) (hr : 1 ≤ r) (hD : 1 ≤ D)
(hZ16 : zsz ((16 * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Z)
(hMb : zsz (Mb : ℤ) ≤ Bz) (hM : K * D + P + 10 ≤ Mb) :
∀ f j (σ : Fin HS → Option ℤ), CoreR σ K S r H P D ρ k q0 Bp → j ≤ D % 8 → D % 8 ≤ j + f →
j + f ≤ 7 →
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) (tensF (kerAt (⟨0, hD⟩ : Fin D) (Butterfly.cb ^ D • (1 : M2))))
(mdT j f) (D / 2 + D % 2) 2
(fun w => f * cMdT Bz + cMdK (P * 2 ^ (K * D) * S * r) Z Bz w) := by sorry