Certified exponential bounds for EML: arguments at least 2

Proved

EmlComplexity.exp_bounds_large

by wamlart · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysiscertified-computationexponential

For each of the 74 rational inputs $x\geq2$ in the table below, the exponential satisfies the indicated closed interval bound:

l\leq\exp(x)\leq u.

The statement is exactly the conjunction of these table entries. This finite analytic certificate supplies bounds used by the complete exclusion of EML expression trees with fewer than nine internal nodes from the value two. The numerical table is new auxiliary work for that formal parent; it is not claimed to appear in the original external EML source.

Input $x$	Lower bound $l$	Upper bound $u$
$\frac{10131}{5000}$	$\frac{18963}{2500}$	$\frac{758521}{100000}$
$\frac{102769}{50000}$	$\frac{39049}{5000}$	$\frac{780981}{100000}$
$\frac{102829}{50000}$	$\frac{390959}{50000}$	$\frac{781919}{100000}$
$\frac{41133}{20000}$	$\frac{195493}{25000}$	$\frac{781973}{100000}$
$\frac{104229}{50000}$	$\frac{804121}{100000}$	$\frac{402061}{50000}$
$\frac{26391}{12500}$	$\frac{20647}{2500}$	$\frac{825881}{100000}$
$\frac{105679}{50000}$	$\frac{413891}{50000}$	$\frac{827783}{100000}$
$\frac{105683}{50000}$	$\frac{103481}{12500}$	$\frac{827849}{100000}$
$\frac{217691}{100000}$	$\frac{881901}{100000}$	$\frac{440951}{50000}$
$\frac{108847}{50000}$	$\frac{881927}{100000}$	$\frac{110241}{12500}$
$\frac{108849}{50000}$	$\frac{881963}{100000}$	$\frac{220491}{25000}$
$\frac{13789}{6250}$	$\frac{18163}{2000}$	$\frac{908151}{100000}$
$\frac{112979}{50000}$	$\frac{478953}{50000}$	$\frac{957907}{100000}$
$\frac{56491}{25000}$	$\frac{957963}{100000}$	$\frac{239491}{25000}$
$\frac{45289}{20000}$	$\frac{481291}{50000}$	$\frac{962583}{100000}$
$\frac{46247}{20000}$	$\frac{252453}{25000}$	$\frac{1009813}{100000}$
$\frac{14743}{6250}$	$\frac{1057909}{100000}$	$\frac{105791}{10000}$
$\frac{126029}{50000}$	$\frac{62179}{5000}$	$\frac{1243581}{100000}$
$\frac{126031}{50000}$	$\frac{124363}{10000}$	$\frac{1243631}{100000}$
$\frac{5047}{2000}$	$\frac{1247217}{100000}$	$\frac{623609}{50000}$
$\frac{126177}{50000}$	$\frac{1247267}{100000}$	$\frac{311817}{25000}$
$\frac{1578}{625}$	$\frac{1248839}{100000}$	$\frac{31221}{2500}$
$\frac{50521}{20000}$	$\frac{1250401}{100000}$	$\frac{625201}{50000}$
$\frac{252609}{100000}$	$\frac{1250451}{100000}$	$\frac{312613}{25000}$
$\frac{253021}{100000}$	$\frac{627807}{50000}$	$\frac{251123}{20000}$
$\frac{253591}{100000}$	$\frac{1262791}{100000}$	$\frac{157849}{12500}$
$\frac{50727}{20000}$	$\frac{1263347}{100000}$	$\frac{315837}{25000}$
$\frac{253639}{100000}$	$\frac{1263397}{100000}$	$\frac{631699}{50000}$
$\frac{50757}{20000}$	$\frac{1265243}{100000}$	$\frac{316311}{25000}$
$\frac{128159}{50000}$	$\frac{1297701}{100000}$	$\frac{648851}{50000}$
$\frac{256323}{100000}$	$\frac{648883}{50000}$	$\frac{1297767}{100000}$
$\frac{257241}{100000}$	$\frac{261947}{20000}$	$\frac{163717}{12500}$
$\frac{413}{160}$	$\frac{330341}{25000}$	$\frac{264273}{20000}$
$\frac{16237}{6250}$	$\frac{167947}{12500}$	$\frac{1343577}{100000}$
$\frac{64949}{25000}$	$\frac{134363}{10000}$	$\frac{1343631}{100000}$
$\frac{10401}{4000}$	$\frac{134671}{10000}$	$\frac{1346711}{100000}$
$\frac{260549}{100000}$	$\frac{270757}{20000}$	$\frac{676893}{50000}$
$\frac{65313}{25000}$	$\frac{170417}{12500}$	$\frac{1363337}{100000}$
$\frac{261257}{100000}$	$\frac{340851}{25000}$	$\frac{272681}{20000}$
$\frac{131049}{50000}$	$\frac{1374919}{100000}$	$\frac{34373}{2500}$
$\frac{33081}{12500}$	$\frac{141043}{10000}$	$\frac{1410431}{100000}$
$\frac{53}{20}$	$\frac{1415403}{100000}$	$\frac{353851}{25000}$
$\frac{66251}{25000}$	$\frac{70773}{5000}$	$\frac{1415461}{100000}$
$\frac{66639}{25000}$	$\frac{1437599}{100000}$	$\frac{1797}{125}$
$\frac{266561}{100000}$	$\frac{1437671}{100000}$	$\frac{179709}{12500}$
$\frac{53391}{20000}$	$\frac{1443347}{100000}$	$\frac{360837}{25000}$
$\frac{133677}{50000}$	$\frac{1449117}{100000}$	$\frac{724559}{50000}$
$\frac{133679}{50000}$	$\frac{57967}{4000}$	$\frac{181147}{12500}$
$\frac{268189}{100000}$	$\frac{365317}{25000}$	$\frac{1461269}{100000}$
$\frac{268193}{100000}$	$\frac{730663}{50000}$	$\frac{1461327}{100000}$
$\frac{134363}{50000}$	$\frac{91821}{6250}$	$\frac{1469137}{100000}$
$\frac{270629}{100000}$	$\frac{748681}{50000}$	$\frac{1497363}{100000}$
$\frac{2171}{800}$	$\frac{754287}{50000}$	$\frac{60343}{4000}$
$\frac{13591}{5000}$	$\frac{757651}{50000}$	$\frac{1515303}{100000}$
$\frac{271827}{100000}$	$\frac{94713}{6250}$	$\frac{1515409}{100000}$
$\frac{67957}{25000}$	$\frac{1515423}{100000}$	$\frac{47357}{3125}$
$\frac{271829}{100000}$	$\frac{757719}{50000}$	$\frac{1515439}{100000}$
$\frac{68949}{25000}$	$\frac{394191}{25000}$	$\frac{315353}{20000}$
$\frac{55949}{20000}$	$\frac{410069}{25000}$	$\frac{1640277}{100000}$
$\frac{280473}{100000}$	$\frac{1652261}{100000}$	$\frac{826131}{50000}$
$\frac{70497}{25000}$	$\frac{1677483}{100000}$	$\frac{419371}{25000}$
$\frac{282077}{100000}$	$\frac{1678977}{100000}$	$\frac{839489}{50000}$
$\frac{8927}{3125}$	$\frac{348059}{20000}$	$\frac{217537}{12500}$
$\frac{288133}{100000}$	$\frac{891899}{50000}$	$\frac{1783799}{100000}$
$\frac{288141}{100000}$	$\frac{89197}{5000}$	$\frac{1783941}{100000}$
$\frac{2893}{1000}$	$\frac{1804737}{100000}$	$\frac{902369}{50000}$
$\frac{291599}{100000}$	$\frac{461677}{25000}$	$\frac{1846709}{100000}$
$\frac{145859}{50000}$	$\frac{1848907}{100000}$	$\frac{462227}{25000}$
$\frac{292489}{100000}$	$\frac{1863217}{100000}$	$\frac{931609}{50000}$
$\frac{37117}{12500}$	$\frac{243493}{12500}$	$\frac{389589}{20000}$
$3$	$\frac{2008553}{100000}$	$\frac{1004277}{50000}$
$\frac{10367}{3125}$	$\frac{2758963}{100000}$	$\frac{689741}{25000}$
$5$	$\frac{2968263}{20000}$	$\frac{3710329}{25000}$
$10$	$\frac{2202646579}{100000}$	$\frac{110132329}{5000}$

Preamble

import Mathlib.Analysis.Complex.ExponentialBounds

Formal statement

theorem EmlComplexity.exp_bounds_large :
((1515423/100000:ℝ)≤Real.exp (67957/25000:ℝ)∧Real.exp (67957/25000:ℝ)≤(47357/3125:ℝ)) ∧
((2202646579/100000:ℝ)≤Real.exp (10:ℝ)∧Real.exp (10:ℝ)≤(110132329/5000:ℝ)) ∧
((1415403/100000:ℝ)≤Real.exp (53/20:ℝ)∧Real.exp (53/20:ℝ)≤(353851/25000:ℝ)) ∧
((881927/100000:ℝ)≤Real.exp (108847/50000:ℝ)∧Real.exp (108847/50000:ℝ)≤(110241/12500:ℝ)) ∧
((2968263/20000:ℝ)≤Real.exp (5:ℝ)∧Real.exp (5:ℝ)≤(3710329/25000:ℝ)) ∧
((757719/50000:ℝ)≤Real.exp (271829/100000:ℝ)∧Real.exp (271829/100000:ℝ)≤(1515439/100000:ℝ)) ∧
((70773/5000:ℝ)≤Real.exp (66251/25000:ℝ)∧Real.exp (66251/25000:ℝ)≤(1415461/100000:ℝ)) ∧
((365317/25000:ℝ)≤Real.exp (268189/100000:ℝ)∧Real.exp (268189/100000:ℝ)≤(1461269/100000:ℝ)) ∧
((62179/5000:ℝ)≤Real.exp (126029/50000:ℝ)∧Real.exp (126029/50000:ℝ)≤(1243581/100000:ℝ)) ∧
((2008553/100000:ℝ)≤Real.exp (3:ℝ)∧Real.exp (3:ℝ)≤(1004277/50000:ℝ)) ∧
((730663/50000:ℝ)≤Real.exp (268193/100000:ℝ)∧Real.exp (268193/100000:ℝ)≤(1461327/100000:ℝ)) ∧
((124363/10000:ℝ)≤Real.exp (126031/50000:ℝ)∧Real.exp (126031/50000:ℝ)≤(1243631/100000:ℝ)) ∧
((1437599/100000:ℝ)≤Real.exp (66639/25000:ℝ)∧Real.exp (66639/25000:ℝ)≤(1797/125:ℝ)) ∧
((1250401/100000:ℝ)≤Real.exp (50521/20000:ℝ)∧Real.exp (50521/20000:ℝ)≤(625201/50000:ℝ)) ∧
((167947/12500:ℝ)≤Real.exp (16237/6250:ℝ)∧Real.exp (16237/6250:ℝ)≤(1343577/100000:ℝ)) ∧
((390959/50000:ℝ)≤Real.exp (102829/50000:ℝ)∧Real.exp (102829/50000:ℝ)≤(781919/100000:ℝ)) ∧
((39049/5000:ℝ)≤Real.exp (102769/50000:ℝ)∧Real.exp (102769/50000:ℝ)≤(780981/100000:ℝ)) ∧
((348059/20000:ℝ)≤Real.exp (8927/3125:ℝ)∧Real.exp (8927/3125:ℝ)≤(217537/12500:ℝ)) ∧
((1437671/100000:ℝ)≤Real.exp (266561/100000:ℝ)∧Real.exp (266561/100000:ℝ)≤(179709/12500:ℝ)) ∧
((1250451/100000:ℝ)≤Real.exp (252609/100000:ℝ)∧Real.exp (252609/100000:ℝ)≤(312613/25000:ℝ)) ∧
((134363/10000:ℝ)≤Real.exp (64949/25000:ℝ)∧Real.exp (64949/25000:ℝ)≤(1343631/100000:ℝ)) ∧
((881963/100000:ℝ)≤Real.exp (108849/50000:ℝ)∧Real.exp (108849/50000:ℝ)≤(220491/25000:ℝ)) ∧
((195493/25000:ℝ)≤Real.exp (41133/20000:ℝ)∧Real.exp (41133/20000:ℝ)≤(781973/100000:ℝ)) ∧
((1449117/100000:ℝ)≤Real.exp (133677/50000:ℝ)∧Real.exp (133677/50000:ℝ)≤(724559/50000:ℝ)) ∧
((891899/50000:ℝ)≤Real.exp (288133/100000:ℝ)∧Real.exp (288133/100000:ℝ)≤(1783799/100000:ℝ)) ∧
((1247217/100000:ℝ)≤Real.exp (5047/2000:ℝ)∧Real.exp (5047/2000:ℝ)≤(623609/50000:ℝ)) ∧
((1263347/100000:ℝ)≤Real.exp (50727/20000:ℝ)∧Real.exp (50727/20000:ℝ)≤(315837/25000:ℝ)) ∧
((170417/12500:ℝ)≤Real.exp (65313/25000:ℝ)∧Real.exp (65313/25000:ℝ)≤(1363337/100000:ℝ)) ∧
((1297701/100000:ℝ)≤Real.exp (128159/50000:ℝ)∧Real.exp (128159/50000:ℝ)≤(648851/50000:ℝ)) ∧
((478953/50000:ℝ)≤Real.exp (112979/50000:ℝ)∧Real.exp (112979/50000:ℝ)≤(957907/100000:ℝ)) ∧
((413891/50000:ℝ)≤Real.exp (105679/50000:ℝ)∧Real.exp (105679/50000:ℝ)≤(827783/100000:ℝ)) ∧
((1265243/100000:ℝ)≤Real.exp (50757/20000:ℝ)∧Real.exp (50757/20000:ℝ)≤(316311/25000:ℝ)) ∧
((1863217/100000:ℝ)≤Real.exp (292489/100000:ℝ)∧Real.exp (292489/100000:ℝ)≤(931609/50000:ℝ)) ∧
((1848907/100000:ℝ)≤Real.exp (145859/50000:ℝ)∧Real.exp (145859/50000:ℝ)≤(462227/25000:ℝ)) ∧
((57967/4000:ℝ)≤Real.exp (133679/50000:ℝ)∧Real.exp (133679/50000:ℝ)≤(181147/12500:ℝ)) ∧
((1247267/100000:ℝ)≤Real.exp (126177/50000:ℝ)∧Real.exp (126177/50000:ℝ)≤(311817/25000:ℝ)) ∧
((1263397/100000:ℝ)≤Real.exp (253639/100000:ℝ)∧Real.exp (253639/100000:ℝ)≤(631699/50000:ℝ)) ∧
((340851/25000:ℝ)≤Real.exp (261257/100000:ℝ)∧Real.exp (261257/100000:ℝ)≤(272681/20000:ℝ)) ∧
((481291/50000:ℝ)≤Real.exp (45289/20000:ℝ)∧Real.exp (45289/20000:ℝ)≤(962583/100000:ℝ)) ∧
((648883/50000:ℝ)≤Real.exp (256323/100000:ℝ)∧Real.exp (256323/100000:ℝ)≤(1297767/100000:ℝ)) ∧
((957963/100000:ℝ)≤Real.exp (56491/25000:ℝ)∧Real.exp (56491/25000:ℝ)≤(239491/25000:ℝ)) ∧
((103481/12500:ℝ)≤Real.exp (105683/50000:ℝ)∧Real.exp (105683/50000:ℝ)≤(827849/100000:ℝ)) ∧
((757651/50000:ℝ)≤Real.exp (13591/5000:ℝ)∧Real.exp (13591/5000:ℝ)≤(1515303/100000:ℝ)) ∧
((1443347/100000:ℝ)≤Real.exp (53391/20000:ℝ)∧Real.exp (53391/20000:ℝ)≤(360837/25000:ℝ)) ∧
((134671/10000:ℝ)≤Real.exp (10401/4000:ℝ)∧Real.exp (10401/4000:ℝ)≤(1346711/100000:ℝ)) ∧
((461677/25000:ℝ)≤Real.exp (291599/100000:ℝ)∧Real.exp (291599/100000:ℝ)≤(1846709/100000:ℝ)) ∧
((1677483/100000:ℝ)≤Real.exp (70497/25000:ℝ)∧Real.exp (70497/25000:ℝ)≤(419371/25000:ℝ)) ∧
((748681/50000:ℝ)≤Real.exp (270629/100000:ℝ)∧Real.exp (270629/100000:ℝ)≤(1497363/100000:ℝ)) ∧
((394191/25000:ℝ)≤Real.exp (68949/25000:ℝ)∧Real.exp (68949/25000:ℝ)≤(315353/20000:ℝ)) ∧
((1248839/100000:ℝ)≤Real.exp (1578/625:ℝ)∧Real.exp (1578/625:ℝ)≤(31221/2500:ℝ)) ∧
((1262791/100000:ℝ)≤Real.exp (253591/100000:ℝ)∧Real.exp (253591/100000:ℝ)≤(157849/12500:ℝ)) ∧
((627807/50000:ℝ)≤Real.exp (253021/100000:ℝ)∧Real.exp (253021/100000:ℝ)≤(251123/20000:ℝ)) ∧
((270757/20000:ℝ)≤Real.exp (260549/100000:ℝ)∧Real.exp (260549/100000:ℝ)≤(676893/50000:ℝ)) ∧
((141043/10000:ℝ)≤Real.exp (33081/12500:ℝ)∧Real.exp (33081/12500:ℝ)≤(1410431/100000:ℝ)) ∧
((261947/20000:ℝ)≤Real.exp (257241/100000:ℝ)∧Real.exp (257241/100000:ℝ)≤(163717/12500:ℝ)) ∧
((330341/25000:ℝ)≤Real.exp (413/160:ℝ)∧Real.exp (413/160:ℝ)≤(264273/20000:ℝ)) ∧
((754287/50000:ℝ)≤Real.exp (2171/800:ℝ)∧Real.exp (2171/800:ℝ)≤(60343/4000:ℝ)) ∧
((2758963/100000:ℝ)≤Real.exp (10367/3125:ℝ)∧Real.exp (10367/3125:ℝ)≤(689741/25000:ℝ)) ∧
((1057909/100000:ℝ)≤Real.exp (14743/6250:ℝ)∧Real.exp (14743/6250:ℝ)≤(105791/10000:ℝ)) ∧
((20647/2500:ℝ)≤Real.exp (26391/12500:ℝ)∧Real.exp (26391/12500:ℝ)≤(825881/100000:ℝ)) ∧
((804121/100000:ℝ)≤Real.exp (104229/50000:ℝ)∧Real.exp (104229/50000:ℝ)≤(402061/50000:ℝ)) ∧
((410069/25000:ℝ)≤Real.exp (55949/20000:ℝ)∧Real.exp (55949/20000:ℝ)≤(1640277/100000:ℝ)) ∧
((89197/5000:ℝ)≤Real.exp (288141/100000:ℝ)∧Real.exp (288141/100000:ℝ)≤(1783941/100000:ℝ)) ∧
((18963/2500:ℝ)≤Real.exp (10131/5000:ℝ)∧Real.exp (10131/5000:ℝ)≤(758521/100000:ℝ)) ∧
((91821/6250:ℝ)≤Real.exp (134363/50000:ℝ)∧Real.exp (134363/50000:ℝ)≤(1469137/100000:ℝ)) ∧
((1374919/100000:ℝ)≤Real.exp (131049/50000:ℝ)∧Real.exp (131049/50000:ℝ)≤(34373/2500:ℝ)) ∧
((18163/2000:ℝ)≤Real.exp (13789/6250:ℝ)∧Real.exp (13789/6250:ℝ)≤(908151/100000:ℝ)) ∧
((243493/12500:ℝ)≤Real.exp (37117/12500:ℝ)∧Real.exp (37117/12500:ℝ)≤(389589/20000:ℝ)) ∧
((94713/6250:ℝ)≤Real.exp (271827/100000:ℝ)∧Real.exp (271827/100000:ℝ)≤(1515409/100000:ℝ)) ∧
((1804737/100000:ℝ)≤Real.exp (2893/1000:ℝ)∧Real.exp (2893/1000:ℝ)≤(902369/50000:ℝ)) ∧
((252453/25000:ℝ)≤Real.exp (46247/20000:ℝ)∧Real.exp (46247/20000:ℝ)≤(1009813/100000:ℝ)) ∧
((1652261/100000:ℝ)≤Real.exp (280473/100000:ℝ)∧Real.exp (280473/100000:ℝ)≤(826131/50000:ℝ)) ∧
((881901/100000:ℝ)≤Real.exp (217691/100000:ℝ)∧Real.exp (217691/100000:ℝ)≤(440951/50000:ℝ)) ∧
((1678977/100000:ℝ)≤Real.exp (282077/100000:ℝ)∧Real.exp (282077/100000:ℝ)≤(839489/50000:ℝ)) := by sorry

Source

New auxiliary numerical certificate for Prove2Me EmlComplexity.complexity_two (theorem 4aef18dd-2336-49b8-810b-f0a58e507c1c), using the exact published EmlComplexity tree definition and Mathlib Real.exp_bound / Real.exp_nat_mul. The rational endpoints were generated and rigorously proved during this task; they are not attributed to the original external EML article.

View graph