claimroutineinferred_dep

Distinct primes meet resampling hypotheses

Distinct odd primes si≈(1−η)tis_i\approx(1-\eta)t_i with S∈(T/2,T)S\in(T/2,T) meet resampling
chooses the prime side lengths for the CRT step
Claim·§9.2.2 Prime source lengths·inside thmInteger multiplication in O(n (lg n)^{1-κ}) time

Statement (paper)

For all sufficiently large nn, one can choose pairwise distinct odd primes s1,…,sds_1,\ldots,s_d with (1−2η)ti<si≤(1−η)ti(1-2\eta)t_i<s_i\leq(1-\eta)t_i and gcd⁡(si,ti)=1\gcd(s_i,t_i)=1 for every ii, such that S=∏isiS=\prod_i s_i satisfies T/2<S<TT/2<S<T, and, with θi=ti/si−1\theta_i=t_i/s_i-1, one has α4θi>p\alpha^4\theta_i>p, 2≤α<p2\le\alpha<\sqrt p, and ti<2pt_i<2^p. Thus every hypothesis of Lemma  holds, and the setup condition of Lemma  holds; moreover the machine finds these primes deterministically in time no(1)=o(n)n^{o(1)}=o(n).

In plain English

For large nn, one can deterministically choose distinct odd primes sis_i with (1−2η)ti<si≤(1−η)ti(1-2\eta)t_i<s_i\le(1-\eta)t_i and gcd⁡(si,ti)=1\gcd(s_i,t_i)=1, whose product SS lies in (T/2,T)(T/2,T). With θi=ti/si−1\theta_i=t_i/s_i-1 they satisfy α4θi>p\alpha^4\theta_i>p, 2≤α<p2\le\alpha<\sqrt p and ti<2pt_i<2^p, so the one-dimensional and tensor resampling lemmas apply, and the search takes time no(1)n^{o(1)}.

Why it's here

This turns the abstract resampling lemmas into a concrete setup by supplying prime lengths sis_i slightly below the power-of-two-sized tit_i. The conditions α4θi>p\alpha^4\theta_i>p follow from the gap η\eta and the parameter bounds of the previous claim, and S∈(T/2,T)S\in(T/2,T) ensures the prime-length transform still covers the needed size. The later CRT address-map step uses these primes, and the sub-linear search time keeps the construction within the overall time budget.
Classified routine:
This parameter-selection step adapts the Harvey–van der Hoeven (2019/2021) choice of distinct primes slightly below power-of-two lengths, using prime number theorem / Bertrand-type density in short intervals and deterministic trial-division search. The inequalities follow from the bounds of the previous claim by direct calculation.

Uses

claimTransform sizes and precision satisfy band boundslemOne-dimensional resampling without sortinglemTensor resampling across d dimensions

Used by

claimCRT address map via controlled shifts

Sources

PaperOpen
Section
§9.2.2 Prime source lengths
Page
—
Label
—
Line
sections/08-assembly.tex:115
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Distinct prime source lengths meet resampling hypotheses" rests on claim-thm-main-2
  • info
    inferred_dep
    outline: "Distinct prime source lengths meet resampling hypotheses" rests on lem:no-sort-resampling
  • info
    inferred_dep
    outline: "Distinct prime source lengths meet resampling hypotheses" rests on lem:tensor-resampling