claimroutineinferred_dep

Dimension choice makes errors small, savings large

Fixes

m,K,w_0,v_0

so errors are below

\varepsilon_0/3

and

cL>2

second third of budget; makes collision saving large

Claim·§4 Choice of parameters and proof of Theorem~thm:main·inside thmIrrationality exponent of pi is 2

Statement (paper)

For all sufficiently large integers

m

, the data

K=\lfloor C^m\rfloor

w_0=B^{-m}

v_0=2K\theta^m w_0

satisfy

K\theta^m\le(C\theta)^m<1

and

K\frac{w_0}{v_0}\theta^m=\frac12

, and the quantity

L=\frac{\eta^2K\theta^m}{(m+1)v_0A^m}=\frac{\eta^2(B/A)^m}{2(m+1)}

tends to

\infty

m\to\infty

, while

K/w_0\to0

v_0\to\infty

and

m/v_0\to0

. Consequently, with

\Lambda=4\log2

and

c=(\log2)/4

, one can fix

m

so large that

\frac{\Lambda F_0m+2\log2}{v_0}+\frac{100K}{w_0}<\frac{\varepsilon_0}{3}

and

cL>2

In plain English

For large

m

, setting

K=\lfloor C^m\rfloor

w_0=B^{-m}

and

v_0=2K\theta^m w_0

gives

K\theta^m\le(C\theta)^m<1

K\frac{w_0}{v_0}\theta^m=\frac12

, and

L=\frac{\eta^2(B/A)^m}{2(m+1)}\to\infty

, while

K/w_0\to0

v_0\to\infty

and

m/v_0\to0

. Hence one can fix

m

so large that

\frac{\Lambda F_0m+2\log2}{v_0}+\frac{100K}{w_0}<\frac{\varepsilon_0}{3}

and

cL>2

, with

\Lambda=4\log2

and

c=(\log2)/4

Why it's here

This fixes the dimension-type parameters

m

K

w_0

v_0

after

F_0

is chosen, so that the error terms depending on them take up only a third of the margin

\varepsilon_0

while the collision saving

cL

exceeds the threshold needed in the determinant comparison. The growth of

(B/A)^m

beats the factor

m+1

, which makes

L

large, and the later claims on weights and the combined error budget rely on this choice of

m

to apply the determinant comparison.

Classified routine:

This is a direct calculation from the parameter definitions and their growth inequalities: exponential growth makes the required limits and error bounds hold for sufficiently large m. The choice is bookkeeping to meet the earlier determinant-comparison conditions, rather than a new technique.

Uses

propDeterminant comparison with two savingsclaimChoose F_0 so nu/F_0 is small

Used by

claimApproximants chosen with center-independent weight thresholdsclaimCombined error margins contradict determinant comparison

Sources

PaperOpen

Section: §4 Choice of parameters and proof of Theorem~thm:main
Page: —
Label: —
Line: sections/conclusion.tex:66

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Dimension separates errors from collision savings" rests on claim-thm-main-1