The top-level reduction

The top-level reduction. A merged table F with the multiplier at pM and a large-n procedure bigE meeting BigSpec with a cost Tb inside the budget gives KappaBound.

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

theorem NLogN.KFM.kappa_of_big {P : ℕ} (F : Fin P → IStmt HS P) (pM bigE : Fin P) (N₁ : ℕ) (Tb : ℕ → ℕ)
    (hM : ∀ I, MulOK I F pM ⟨fun a b => mulCostH (zsz a + zsz b), fun _ _ => True⟩)
    (hB : BigSpec F bigE N₁ Tb) (C₀ : ℝ) (hC₀ : 0 ≤ C₀) (A : ℕ)
    (hT : ∀ n, IntMul.OpenAI.Glue.n0 ≤ n → N₁ ≤ n → (2 * ((Tb n + topOvh n N₁ : ℕ) : ℝ) + 1 : ℝ) ≤
      C₀ * (VP n * Ncost (6 * (IntMul.lg n : ℝ)) (IntMul.OpenAI.Glue.dP n) (KP n) (ℓP n) (αP n) *
        (Real.log (6 * (IntMul.lg n : ℝ)) + 1) ^ A + n)) :
    IntMul.KappaBound (1 / 2 ^ 182)

Context. The lemma belongs to the part KFM K1: the top level — reading, the small-n branch, compilation.

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.