lemmaroutine

Rows reduce to entire-function rows

Writes each row as ≤

Q_H

scaled entire-function rows with explicit scalars

reduces the determinant to entire-function test rows

Lemma·det:translation·§3.2 Translation to entire functions

Statement (paper)

Every row

\rho=(j,s,\beta)

of is a sum of at most

Q_H=(\lfloor H\rfloor+1)^{2m} (\lfloor H/v_0\rfloor+1)

scalar multiples of row vectors of the form

\bigl([t^\ell]f_{a,P}(j\omega+\log(1+t))\bigr)_P, \qquad a\ge\beta,\quad wa\le H,\quad0\le\ell\le s.

Each scalar

\xi

occurring with index

a

satisfies

\begin{aligned} |\xi|&\le\exp\{-\nu w(a-\beta)+H E_{\rm tr}\},\\ E_{\rm tr} &=\frac{\nu}{F_0}+\frac{\log2}{v_0} +\frac{\log4+\log(2K)+\nu}{w_*}. \end{aligned}

In plain English

Each row

\rho=(j,s,\beta)

of the matrix is a sum of at most

Q_H=(\lfloor H\rfloor+1)^{2m}(\lfloor H/v_0\rfloor+1)

scalar multiples of row vectors

([t^\ell]f_{a,P}(j\omega+\log(1+t)))_P

with

a\ge\beta

wa\le H

0\le\ell\le s

. The scalar attached to index

a

has absolute value at most

\exp\{-\nu w(a-\beta)+HE_{\rm tr}\}

, with

E_{\rm tr}=\frac{\nu}{F_0}+\frac{\log2}{v_0}+\frac{\log4+\log(2K)+\nu}{w_*}

Why it's here

This lemma moves the determinant problem from the original rows to rows of the entire functions

f_{a,P}

evaluated at translated points. The expansion about exact periods is controlled by the tail-weight bound, which gives explicit coefficient sizes and a term count. The collision estimate, determinant comparison and main theorem can then expand the determinant into simpler test rows with controlled scalar factors and a bounded number of terms per row.

Classified routine:

This is a paper-specific expansion of the determinant rows using Taylor or binomial series about exact periods. The term count and coefficient bound are bookkeeping consequences of that expansion and the stated tail-weight bound.

Uses

Nothing else in the paper

Used by

thmIrrationality exponent of pi is 2lemRepeated Taylor degrees force determinant decaypropDeterminant comparison with two savingsclaimCombined error margins contradict determinant comparisonclaimSimplex counts calibrate expanded determinantclaimMany heavy indices force approximation saving

Inside the proof

claimRows expand around exact periodsclaimTruncation tails consume limited weightclaimCoefficient bound and term count

Sources

PaperOpen

Section: §3.2 Translation to entire functions
Page: —
Label: det:translation
Line: sections/determinant.tex:172

Leannot aligned

Phase 2 aligns this node to a Lean declaration.