claimroutineinferred_dep

Either saving defeats arithmetic lower bound

Both savings fall below −(1−bˉ)−Ear-(1-\bar b)-E_{\rm ar}, contradicting the arithmetic bound
closes the comparison proposition
Claim·§3.4 A comparison with two alternatives·inside propDeterminant comparison with two savings

Statement (paper)

Under , for all sufficiently large HH, both quantities −cLH-cL_H and −ν(A(1−η)−bˉ)-\nu(A(1-\eta)-\bar b) inside the maximum in , after adding Ean+εHE_{\rm an}+\varepsilon_H, are strictly less than −(1−bˉ)−Ear-(1-\bar b)-E_{\rm ar}; consequently the upper bound for log⁡∣ΔH∣/(MH)\log|\Delta_H|/(MH) in contradicts the arithmetic lower bound of Lemma .

In plain English

Under the contradiction conditions g>0g>0, Ear+Ean<gE_{\rm ar}+E_{\rm an}<g and cL>1+Ear+EancL>1+E_{\rm ar}+E_{\rm an}, for all large HH both terms −cLH-cL_H and −ν(A(1−η)−bˉ)-\nu(A(1-\eta)-\bar b) in the upper bound (after adding Ean+εHE_{\rm an}+\varepsilon_H) fall strictly below −(1−bˉ)−Ear-(1-\bar b)-E_{\rm ar}. The analytic upper bound on log⁡∣ΔH∣/(MH)\log|\Delta_H|/(MH) therefore contradicts the arithmetic lower bound.

Why it's here

This closes the proof of the comparison proposition. The upper bound is the maximum of a light-index saving and a heavy-index saving, and the hypotheses on LL and gg make each one beat the arithmetic lower bound with its error EarE_{\rm ar}. Since εH→0\varepsilon_H\to0 and bˉ\bar b is controlled, the strict inequalities persist for large HH, so the maximum falls below the lower bound and no such ΔH\Delta_H can exist.
Classified routine:
This is a direct comparison of the two savings from claim-det-comparison-2 and claim-det-comparison-3 with the lower bound in det-arithmetic. The stated strict inequalities and vanishing error term make the contradiction follow for sufficiently large HH.

Uses

lemArithmetic lower bound on minor determinantclaimMany light indices force collisionsclaimMany heavy indices force approximation saving

Used by

Nothing in the paper

Sources

PaperOpen
Section
§3.4 A comparison with two alternatives
Page
—
Label
—
Line
sections/determinant.tex:418
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Either saving defeats arithmetic lower bound" rests on claim-det-comparison-2
  • info
    inferred_dep
    outline: "Either saving defeats arithmetic lower bound" rests on claim-det-comparison-3