Round six: final reduction from a machine with the round-six cost to KappaBound

Let $P$ satisfy Prm.Ok and let $\kappa < \mathrm{gap}(P)$. Let $M$ be a multitape Turing machine that multiplies correctly on every input length $n \ge 1$, and suppose there are $n_1, A \in \mathbb N$ and $C_0 \ge 0$ such that for every $n \ge n_1$ the machine multiplies $n$-bit numbers within time

where $V$ is the round-six bit volume and $N$ the per-bit cost. Then the platform bound KappaBound $\kappa$ holds, i.e. integer multiplication is possible in time $O(n \log n \cdot \text{(saving } \lg^{-\kappa}))$ in the sense of Def_IntMul_MultitapeModel.

This is the glue between the round-six machine (still to be built) and the campaign's exponent bookkeeping.

In Lean:

theorem IntMul.Kappa.R6.kappaBound_of_machine6 (P : Prm) (hP : P.Ok) (κ : ℝ) (hκ : κ < P.gap)
    (M : IntMul.MultitapeTM) (hcorr : ∀ n, 1 ≤ n → ∃ T : ℝ, IntMul.MultipliesAt M n T)
    (n₁ A : ℕ) (C₀ : ℝ) (hC₀ : 0 ≤ C₀)
    (htime : ∀ n, n₁ ≤ n → IntMul.MultipliesAt M n
      (C₀ * (VP6 P n * Ncost6 P n * (Real.log (IntMul.lg n) + 1) ^ A + n))) :
    IntMul.KappaBound κ

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).