claimroutineinferred_dep

Fixed exponents satisfy all parameter conditions

Chosen rational exponents satisfy all layer and dimension inequalities
admissible parameters for the layer and cost table
Claim·§9.1 A fixed rational choice·inside thmInteger multiplication in O(n (lg n)^{1-κ}) time

Statement (paper)

For the fixed rational numbers in , the layer conditions hold: max⁡{τ,σ}<λ<1\max\{\tau,\sigma\}<\lambda<1, τ(1+c/β)<1−31⋅2−55<λ\tau(1+c/\beta)<1-31\cdot2^{-55}<\lambda, and σ+β(1−σ)=1−2−51<λ<λ′<1\sigma+\beta(1-\sigma)=1-2^{-51}<\lambda<\lambda'<1. The dimension-exponent conditions also hold: ϵ<112\epsilon<\frac1{12}, ϵC1<1\epsilon C_1<1, ϵ(2−τ)<1−τ\epsilon(2-\tau)<1-\tau, 34+δ+32ϵ<1\frac34+\delta+\frac32\epsilon<1, ϵ(1+c)<1\epsilon(1+c)<1, and ϵ+δ<1\epsilon+\delta<1.

In plain English

With the specific rational parameter values fixed in the paper, every required inequality holds: the layer conditions (such as max⁡{τ,σ}<λ<1\max\{\tau,\sigma\}<\lambda<1 and σ+β(1−σ)=1−2−51<λ<λ′<1\sigma+\beta(1-\sigma)=1-2^{-51}<\lambda<\lambda'<1) and the dimension-exponent conditions (such as ϵ<112\epsilon<\frac1{12}, ϵC1<1\epsilon C_1<1, and ϵ+δ<1\epsilon+\delta<1).

Why it's here

This is a finite arithmetic check that the chosen rational constants are admissible, so the simultaneous Hadamard layer proposition and later band-bound and cost-table claims can be applied with these parameters. It separates the bookkeeping of exponent inequalities from the main argument, and in particular confirms ϵC1<1\epsilon C_1<1, which makes the guard width o(p)o(p).
Classified routine:
A finite arithmetic verification that the paper's chosen rational constants satisfy the inequalities required by the simultaneous Hadamard layer proposition and the later dimension-exponent conditions. It is pure bookkeeping with no new idea.

Uses

propSimultaneous Hadamard layer in near-linear time

Used by

claimTransform sizes and precision satisfy band boundsclaimCost table yields the final time bound

Sources

PaperOpen
Section
§9.1 A fixed rational choice
Page
—
Label
—
Line
sections/08-assembly.tex:16
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Fixed rational exponents satisfy all conditions" rests on prop:simultaneous-layer