lemmaroutine

Arithmetic lower bound on minor determinant

Bounds a nonzero minor below:

\log|\Delta_H|/(MH)\ge-(1-\bar b)-E_{\rm ar}

arithmetic lower bound opposing the analytic upper bound

Lemma·det:arithmetic·§3.1 A full-row-rank minor and its arithmetic size

Statement (paper)

Let

\Lambda=4\log2

, and define

E_{\rm ar} =\frac{\Lambda F_0m}{v_0} +\Lambda\sum_{i=1}^m\frac1{w_i}+\frac{\theta}{w_*}.

Then every minor just chosen satisfies

\frac{\log|\Delta_H|}{MH} \ge -(1-\bar b)-E_{\rm ar}.

For every chosen full-rank minor

\Delta_H

\frac{\log|\Delta_H|}{MH}\ge-(1-\bar b)-E_{\rm ar}

, where

E_{\rm ar}=\frac{\Lambda F_0 m}{v_0}+\Lambda\sum_{i=1}^m \frac1{w_i}+\frac{\theta}{w_*}

and

\Lambda=4\log 2

This supplies the arithmetic side of the determinant comparison: a nonzero minor cannot be too small, with the loss controlled by the explicit error

E_{\rm ar}

. The main theorem and the comparison proposition combine it with an analytic upper bound on

|\Delta_H|

and show the two are incompatible when the exponent is too large, which gives the contradiction.

Classified routine:

This is the standard arithmetic side of a determinant argument: a nonzero minor has a lower bound after denominators are cleared. The explicit term

E_{\rm ar}

records the paper-specific denominator bookkeeping.

Nothing else in the paper

PaperOpen

Leannot aligned

Phase 2 aligns this node to a Lean declaration.