claimroutineinferred_dep

Combined error margins contradict determinant comparison

Total error

E_{\rm ar}+E_{\rm an}<\varepsilon_0

, so determinant comparison gives a contradiction

finishes the upper bound by contradiction

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

Statement (paper)

With the dimension, weights and centers chosen as above, the total error satisfies

E_{\rm ar}+E_{\rm an}=\frac{\nu}{F_0}+\frac{\Lambda F_0m+2\log2}{v_0}+\frac{100K}{w_0}+\Lambda\sum_i\frac1{w_i}+\frac{\theta+\log4+\log(2K)+\nu+\log(200K)}{w_*}<\varepsilon_0

. In particular

E_{\rm ar}+E_{\rm an}<g

and

cL>2>1+E_{\rm ar}+E_{\rm an}

, so all hypotheses of Proposition hold, which yields a contradiction.

In plain English

With the chosen

F_0

m

K

w_0

v_0

and approximants

p_i/q_i

, the total error

E_{\rm ar}+E_{\rm an}

is less than

\varepsilon_0

. Hence

E_{\rm ar}+E_{\rm an}<g

and

cL>2>1+E_{\rm ar}+E_{\rm an}

, so the determinant comparison hypotheses all hold and give a contradiction.

Why it's here

The total error splits into three pieces, each bounded by a third of

\varepsilon_0

by the earlier parameter choices: the

\nu/F_0

term, the

m

K

w_0

v_0

terms, and the weight terms. Since

\varepsilon_0=\min(g/2,1/2)

, the sum is below

g

and below

1/2

, so

1+E_{\rm ar}+E_{\rm an}<2<cL

. This meets the budget conditions of the determinant comparison proposition, which rules out the assumed approximations and so finishes the proof by contradiction.

Classified routine:

This is the final bookkeeping step: the earlier parameter choices bound the error terms, and the resulting inequalities meet the hypotheses of the determinant comparison proposition, yielding the contradiction.

Uses

propDeterminant comparison with two savingsclaimChoose F_0 so nu/F_0 is smallclaimDimension choice makes errors small, savings largeclaimApproximants chosen with center-independent weight thresholdslemArithmetic lower bound on minor determinantlemRows reduce to entire-function rowslemRepeated Taylor degrees force determinant decay

Used by

claimPi is irrationalclaimDirichlet pigeonhole gives lower bound exponent 2

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Combined error margins contradict determinant comparison" rests on claim-thm-main-1
info
inferred_dep
outline: "Combined error margins contradict determinant comparison" rests on claim-thm-main-2
info
inferred_dep
outline: "Combined error margins contradict determinant comparison" rests on claim-thm-main-3
info
inferred_dep
outline: "Combined error margins contradict determinant comparison" rests on det:arithmetic
info
inferred_dep
outline: "Combined error margins contradict determinant comparison" rests on det:translation
info
inferred_dep
outline: "Combined error margins contradict determinant comparison" rests on det:collision