propositionroutineunresolved_ref

Determinant comparison with two savings

Gives a contradiction if

g>0

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

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

contradiction engine; only budget conditions remain to check

Proposition·det:comparison·§3.4 A comparison with two alternatives

Statement (paper)

Let

0<A<1

and

0<\eta<1

, and define

g=\nu\bigl(A(1-\eta)-\theta\bigr)-(1-\theta), \qquad L=\frac{\eta^2K\theta^m}{(m+1)v_0A^m}.

The approximations and the interpolation hypotheses cannot hold simultaneously if

g>0,\qquad E_{\rm ar}+E_{\rm an}<g, \qquad cL>1+E_{\rm ar}+E_{\rm an}.

In plain English

For

0<A<1

and

0<\eta<1

, set

g=\nu(A(1-\eta)-\theta)-(1-\theta)

and

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

. If

g>0

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

and

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

, then the approximations and the interpolation hypotheses cannot hold simultaneously.

Why it's here

This is the contradiction engine used by the main theorem. Row terms split into many light indices, which give a collision saving of

cL

, or many heavy indices, which give an approximation saving governed by

g

. Either saving pushes the upper bound on

\log|\Delta_H|/(MH)

below the arithmetic lower bound, so the budget conditions on

g

and

L

are all that must be checked downstream.

Classified routine:

This is the final budget comparison: it combines the preceding row-translation and collision bounds with the arithmetic lower bound, then applies a light-versus-heavy row split. The proposition packages those earlier estimates rather than introducing a separate new method.

Uses

lemRows reduce to entire-function rowslemRepeated Taylor degrees force determinant decaylemArithmetic lower bound on minor determinant

Used by

thmIrrationality exponent of pi is 2claimDimension choice makes errors small, savings largeclaimCombined error margins contradict determinant comparison

Inside the proof

claimSimplex counts calibrate expanded determinantclaimMany light indices force collisionsclaimMany heavy indices force approximation savingclaimEither saving defeats arithmetic lower bound

Sources

PaperOpen

Section: §3.4 A comparison with two alternatives
Page: —
Label: det:comparison
Line: sections/determinant.tex:353

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

warn
unresolved_ref
The collision-scale limit uses the unlabeled simplex row count at determinant.tex:69–81.