claimroutineinferred_dep

Cost table yields the final time bound

Cost table has every dominant power of pp at most 1−2κ1-2\kappa
gives the final p1−κp^{1-\kappa} time bound
Claim·§9.8 The complete time bound·inside thmInteger multiplication in O(n (lg n)^{1-κ}) time

Statement (paper)

Each of the seven dominant powers of pp in Table costs is at most 1−2κ1-2\kappa, with min⁡igi=2−181=2κ\min_i g_i=2^{-181}=2\kappa, and all remaining costs (setup, exceptional streams, input, padding, carries, output) are absorbed or are o(Tp)o(Tp). Consequently, for all sufficiently large nn the total running time is O(Tp p1−κ)=O(n(log⁡n)1−κ)O(Tp\,p^{1-\kappa})=O(n(\log n)^{1-\kappa}), and using schoolbook multiplication below a fixed cutoff gives TA(n)=O(n(lg⁡n)1−κ)T_A(n)=O(n(\lg n)^{1-\kappa}) for every n≥1n\ge1.

In plain English

Each of the seven dominant powers of pp in the cost table is at most 1−2κ1-2\kappa, with minimum exponent 2−181=2κ2^{-181}=2\kappa, and the other costs are absorbed or are o(Tp)o(Tp). So the total time is O(n(lg⁡n)1−κ)O(n(\lg n)^{1-\kappa}) for large nn, and with schoolbook multiplication below a fixed cutoff, TA(n)=O(n(lg⁡n)1−κ)T_A(n)=O(n(\lg n)^{1-\kappa}) for every n≥1n\ge1.

Why it's here

This is the closing step of the main theorem: it takes the per-stage costs from the transform, layer, chunk-swap, resampling and CRT address-map results, evaluated at the admissible parameters, and shows each has a saving of at least 2κ2\kappa in the exponent of pp. That saving gives the p1−κp^{1-\kappa} factor, with slack to absorb the smaller terms, and the small-nn cutoff extends the bound to all nn.
Classified routine:
This is bookkeeping that closes the main theorem. It checks the exponents in the cost table at the fixed parameters, absorbs the lower-order terms, and handles small n with a schoolbook cutoff, all as direct consequences of the earlier cost lemmas and the parameter claim.

Uses

claimFixed exponents satisfy all parameter conditionslemCost and accuracy of synthetic transformpropSimultaneous Hadamard layer in near-linear timelemSwapping binary address chunks in O(Vu^τ)propPower-width chunk interchange in O(Ve^τ)lemPacked XOR of selected address bitslemTensor resampling across d dimensionsclaimCRT address map via controlled shiftsclaimFinal error below 1/2; rounding and carries exact

Used by

Nothing in the paper

Sources

PaperOpen
Section
§9.8 The complete time bound
Page
—
Label
—
Line
sections/08-assembly.tex:820
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Cost table gives O(n(lg n)^{1-κ})" rests on claim-thm-main-1
  • info
    inferred_dep
    outline: "Cost table gives O(n(lg n)^{1-κ})" rests on lem:synthetic-transform-cost
  • info
    inferred_dep
    outline: "Cost table gives O(n(lg n)^{1-κ})" rests on prop:simultaneous-layer
  • info
    inferred_dep
    outline: "Cost table gives O(n(lg n)^{1-κ})" rests on lem:chunk-swap
  • info
    inferred_dep
    outline: "Cost table gives O(n(lg n)^{1-κ})" rests on prop:power-interchange
  • info
    inferred_dep
    outline: "Cost table gives O(n(lg n)^{1-κ})" rests on lem:packed-selected-bit-rectangle
  • info
    inferred_dep
    outline: "Cost table gives O(n(lg n)^{1-κ})" rests on lem:tensor-resampling
  • info
    inferred_dep
    outline: "Cost table gives O(n(lg n)^{1-κ})" rests on claim-thm-main-4
  • info
    inferred_dep
    outline: "Cost table gives O(n(lg n)^{1-κ})" rests on claim-thm-main-9