Certified exponential bounds for EML: arguments in [1,2)

Proved

EmlComplexity.exp_bounds_one_two

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

analysiscertified-computationexponential

For each of the 78 rational inputs $1\leq x<2$ 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$
$1$	$\frac{67957}{25000}$	$\frac{271829}{100000}$
$\frac{100001}{100000}$	$\frac{27183}{10000}$	$\frac{271831}{100000}$
$\frac{50001}{50000}$	$\frac{271833}{100000}$	$\frac{135917}{50000}$
$\frac{103131}{100000}$	$\frac{280473}{100000}$	$\frac{140237}{50000}$
$\frac{103149}{100000}$	$\frac{70131}{25000}$	$\frac{11221}{4000}$
$\frac{103701}{100000}$	$\frac{282077}{100000}$	$\frac{141039}{50000}$
$\frac{25927}{25000}$	$\frac{17631}{6250}$	$\frac{282097}{100000}$
$\frac{104963}{100000}$	$\frac{285659}{100000}$	$\frac{14283}{5000}$
$\frac{104969}{100000}$	$\frac{71419}{25000}$	$\frac{285677}{100000}$
$\frac{3294}{3125}$	$\frac{286933}{100000}$	$\frac{143467}{50000}$
$\frac{105913}{100000}$	$\frac{144193}{50000}$	$\frac{288387}{100000}$
$\frac{26557}{25000}$	$\frac{57859}{20000}$	$\frac{18081}{6250}$
$\frac{53531}{50000}$	$\frac{145859}{50000}$	$\frac{291719}{100000}$
$\frac{26767}{25000}$	$\frac{36467}{12500}$	$\frac{291737}{100000}$
$\frac{107317}{100000}$	$\frac{292463}{100000}$	$\frac{18279}{6250}$
$\frac{26831}{25000}$	$\frac{73121}{25000}$	$\frac{58497}{20000}$
$\frac{107331}{100000}$	$\frac{36563}{12500}$	$\frac{58501}{20000}$
$\frac{108833}{100000}$	$\frac{296931}{100000}$	$\frac{74233}{25000}$
$\frac{110211}{100000}$	$\frac{301051}{100000}$	$\frac{75263}{25000}$
$\frac{55827}{50000}$	$\frac{152713}{50000}$	$\frac{305427}{100000}$
$\frac{22557}{20000}$	$\frac{3089}{1000}$	$\frac{308901}{100000}$
$\frac{5707}{5000}$	$\frac{156557}{50000}$	$\frac{62623}{20000}$
$\frac{57513}{50000}$	$\frac{315901}{100000}$	$\frac{157951}{50000}$
$\frac{59883}{50000}$	$\frac{66247}{20000}$	$\frac{82809}{25000}$
$\frac{119771}{100000}$	$\frac{82813}{25000}$	$\frac{331253}{100000}$
$\frac{24071}{20000}$	$\frac{41649}{12500}$	$\frac{333193}{100000}$
$\frac{120361}{100000}$	$\frac{83303}{25000}$	$\frac{333213}{100000}$
$\frac{12119}{10000}$	$\frac{167993}{50000}$	$\frac{335987}{100000}$
$\frac{60927}{50000}$	$\frac{21139}{6250}$	$\frac{13529}{4000}$
$\frac{30579}{25000}$	$\frac{33979}{10000}$	$\frac{339791}{100000}$
$\frac{2501}{2000}$	$\frac{43651}{12500}$	$\frac{349209}{100000}$
$\frac{15651}{12500}$	$\frac{349761}{100000}$	$\frac{174881}{50000}$
$\frac{67489}{50000}$	$\frac{385657}{100000}$	$\frac{192829}{50000}$
$\frac{134983}{100000}$	$\frac{96419}{25000}$	$\frac{385677}{100000}$
$\frac{27369}{20000}$	$\frac{15717}{4000}$	$\frac{196463}{50000}$
$\frac{139977}{100000}$	$\frac{202713}{50000}$	$\frac{405427}{100000}$
$\frac{3613}{2500}$	$\frac{42427}{10000}$	$\frac{424271}{100000}$
$\frac{9173}{6250}$	$\frac{86783}{20000}$	$\frac{108479}{25000}$
$\frac{73389}{50000}$	$\frac{433959}{100000}$	$\frac{10849}{2500}$
$\frac{147413}{100000}$	$\frac{436723}{100000}$	$\frac{109181}{25000}$
$\frac{151467}{100000}$	$\frac{56849}{12500}$	$\frac{454793}{100000}$
$\frac{76029}{50000}$	$\frac{457487}{100000}$	$\frac{28593}{6250}$
$\frac{76031}{50000}$	$\frac{228753}{50000}$	$\frac{457507}{100000}$
$\frac{156797}{100000}$	$\frac{47969}{10000}$	$\frac{479691}{100000}$
$\frac{78401}{50000}$	$\frac{239857}{50000}$	$\frac{95943}{20000}$
$\frac{39399}{25000}$	$\frac{241769}{50000}$	$\frac{483539}{100000}$
$\frac{31639}{20000}$	$\frac{486443}{100000}$	$\frac{121611}{25000}$
$\frac{159167}{100000}$	$\frac{245597}{50000}$	$\frac{98239}{20000}$
$\frac{40403}{25000}$	$\frac{62919}{12500}$	$\frac{503353}{100000}$
$\frac{161617}{100000}$	$\frac{503377}{100000}$	$\frac{251689}{50000}$
$\frac{164497}{100000}$	$\frac{103617}{20000}$	$\frac{259043}{50000}$
$\frac{4119}{2500}$	$\frac{519449}{100000}$	$\frac{10389}{2000}$
$\frac{166859}{100000}$	$\frac{132617}{25000}$	$\frac{530469}{100000}$
$\frac{168041}{100000}$	$\frac{21471}{4000}$	$\frac{67097}{12500}$
$\frac{4217}{2500}$	$\frac{67527}{12500}$	$\frac{540217}{100000}$
$\frac{168697}{100000}$	$\frac{135077}{25000}$	$\frac{540309}{100000}$
$\frac{6873}{4000}$	$\frac{139369}{25000}$	$\frac{557477}{100000}$
$\frac{42957}{25000}$	$\frac{557493}{100000}$	$\frac{278747}{50000}$
$\frac{171829}{100000}$	$\frac{278749}{50000}$	$\frac{557499}{100000}$
$\frac{43339}{25000}$	$\frac{566077}{100000}$	$\frac{283039}{50000}$
$\frac{174369}{100000}$	$\frac{3574}{625}$	$\frac{571841}{100000}$
$\frac{178523}{100000}$	$\frac{119219}{20000}$	$\frac{18628}{3125}$
$\frac{44633}{25000}$	$\frac{149037}{25000}$	$\frac{596149}{100000}$
$\frac{178691}{100000}$	$\frac{597097}{100000}$	$\frac{298549}{50000}$
$\frac{179697}{100000}$	$\frac{301567}{50000}$	$\frac{120627}{20000}$
$\frac{44931}{25000}$	$\frac{603297}{100000}$	$\frac{301649}{50000}$
$\frac{180843}{100000}$	$\frac{305043}{50000}$	$\frac{610087}{100000}$
$\frac{180853}{100000}$	$\frac{610147}{100000}$	$\frac{152537}{25000}$
$\frac{45489}{25000}$	$\frac{308457}{50000}$	$\frac{123383}{20000}$
$\frac{184601}{100000}$	$\frac{633449}{100000}$	$\frac{12669}{2000}$
$\frac{11621}{6250}$	$\frac{320981}{50000}$	$\frac{641963}{100000}$
$\frac{95859}{50000}$	$\frac{27207}{4000}$	$\frac{42511}{6250}$
$\frac{38367}{20000}$	$\frac{680971}{100000}$	$\frac{170243}{25000}$
$\frac{96897}{50000}$	$\frac{694443}{100000}$	$\frac{173611}{25000}$
$\frac{194033}{100000}$	$\frac{87013}{12500}$	$\frac{139221}{20000}$
$\frac{97019}{50000}$	$\frac{696139}{100000}$	$\frac{34807}{5000}$
$\frac{98011}{50000}$	$\frac{88761}{12500}$	$\frac{710089}{100000}$
$\frac{199777}{100000}$	$\frac{737259}{100000}$	$\frac{36863}{5000}$

Preamble

import Mathlib.Analysis.Complex.ExponentialBounds

Formal statement

theorem EmlComplexity.exp_bounds_one_two :
((67957/25000:ℝ)≤Real.exp (1:ℝ)∧Real.exp (1:ℝ)≤(271829/100000:ℝ)) ∧
((557493/100000:ℝ)≤Real.exp (42957/25000:ℝ)∧Real.exp (42957/25000:ℝ)≤(278747/50000:ℝ)) ∧
((457487/100000:ℝ)≤Real.exp (76029/50000:ℝ)∧Real.exp (76029/50000:ℝ)≤(28593/6250:ℝ)) ∧
((87013/12500:ℝ)≤Real.exp (194033/100000:ℝ)∧Real.exp (194033/100000:ℝ)≤(139221/20000:ℝ)) ∧
((67527/12500:ℝ)≤Real.exp (4217/2500:ℝ)∧Real.exp (4217/2500:ℝ)≤(540217/100000:ℝ)) ∧
((278749/50000:ℝ)≤Real.exp (171829/100000:ℝ)∧Real.exp (171829/100000:ℝ)≤(557499/100000:ℝ)) ∧
((228753/50000:ℝ)≤Real.exp (76031/50000:ℝ)∧Real.exp (76031/50000:ℝ)≤(457507/100000:ℝ)) ∧
((62919/12500:ℝ)≤Real.exp (40403/25000:ℝ)∧Real.exp (40403/25000:ℝ)≤(503353/100000:ℝ)) ∧
((285659/100000:ℝ)≤Real.exp (104963/100000:ℝ)∧Real.exp (104963/100000:ℝ)≤(14283/5000:ℝ)) ∧
((66247/20000:ℝ)≤Real.exp (59883/50000:ℝ)∧Real.exp (59883/50000:ℝ)≤(82809/25000:ℝ)) ∧
((145859/50000:ℝ)≤Real.exp (53531/50000:ℝ)∧Real.exp (53531/50000:ℝ)≤(291719/100000:ℝ)) ∧
((135077/25000:ℝ)≤Real.exp (168697/100000:ℝ)∧Real.exp (168697/100000:ℝ)≤(540309/100000:ℝ)) ∧
((301567/50000:ℝ)≤Real.exp (179697/100000:ℝ)∧Real.exp (179697/100000:ℝ)≤(120627/20000:ℝ)) ∧
((86783/20000:ℝ)≤Real.exp (9173/6250:ℝ)∧Real.exp (9173/6250:ℝ)≤(108479/25000:ℝ)) ∧
((41649/12500:ℝ)≤Real.exp (24071/20000:ℝ)∧Real.exp (24071/20000:ℝ)≤(333193/100000:ℝ)) ∧
((503377/100000:ℝ)≤Real.exp (161617/100000:ℝ)∧Real.exp (161617/100000:ℝ)≤(251689/50000:ℝ)) ∧
((71419/25000:ℝ)≤Real.exp (104969/100000:ℝ)∧Real.exp (104969/100000:ℝ)≤(285677/100000:ℝ)) ∧
((47969/10000:ℝ)≤Real.exp (156797/100000:ℝ)∧Real.exp (156797/100000:ℝ)≤(479691/100000:ℝ)) ∧
((73121/25000:ℝ)≤Real.exp (26831/25000:ℝ)∧Real.exp (26831/25000:ℝ)≤(58497/20000:ℝ)) ∧
((385657/100000:ℝ)≤Real.exp (67489/50000:ℝ)∧Real.exp (67489/50000:ℝ)≤(192829/50000:ℝ)) ∧
((305043/50000:ℝ)≤Real.exp (180843/100000:ℝ)∧Real.exp (180843/100000:ℝ)≤(610087/100000:ℝ)) ∧
((119219/20000:ℝ)≤Real.exp (178523/100000:ℝ)∧Real.exp (178523/100000:ℝ)≤(18628/3125:ℝ)) ∧
((36467/12500:ℝ)≤Real.exp (26767/25000:ℝ)∧Real.exp (26767/25000:ℝ)≤(291737/100000:ℝ)) ∧
((737259/100000:ℝ)≤Real.exp (199777/100000:ℝ)∧Real.exp (199777/100000:ℝ)≤(36863/5000:ℝ)) ∧
((280473/100000:ℝ)≤Real.exp (103131/100000:ℝ)∧Real.exp (103131/100000:ℝ)≤(140237/50000:ℝ)) ∧
((301051/100000:ℝ)≤Real.exp (110211/100000:ℝ)∧Real.exp (110211/100000:ℝ)≤(75263/25000:ℝ)) ∧
((132617/25000:ℝ)≤Real.exp (166859/100000:ℝ)∧Real.exp (166859/100000:ℝ)≤(530469/100000:ℝ)) ∧
((282077/100000:ℝ)≤Real.exp (103701/100000:ℝ)∧Real.exp (103701/100000:ℝ)≤(141039/50000:ℝ)) ∧
((21139/6250:ℝ)≤Real.exp (60927/50000:ℝ)∧Real.exp (60927/50000:ℝ)≤(13529/4000:ℝ)) ∧
((139369/25000:ℝ)≤Real.exp (6873/4000:ℝ)∧Real.exp (6873/4000:ℝ)≤(557477/100000:ℝ)) ∧
((603297/100000:ℝ)≤Real.exp (44931/25000:ℝ)∧Real.exp (44931/25000:ℝ)≤(301649/50000:ℝ)) ∧
((433959/100000:ℝ)≤Real.exp (73389/50000:ℝ)∧Real.exp (73389/50000:ℝ)≤(10849/2500:ℝ)) ∧
((83303/25000:ℝ)≤Real.exp (120361/100000:ℝ)∧Real.exp (120361/100000:ℝ)≤(333213/100000:ℝ)) ∧
((566077/100000:ℝ)≤Real.exp (43339/25000:ℝ)∧Real.exp (43339/25000:ℝ)≤(283039/50000:ℝ)) ∧
((436723/100000:ℝ)≤Real.exp (147413/100000:ℝ)∧Real.exp (147413/100000:ℝ)≤(109181/25000:ℝ)) ∧
((241769/50000:ℝ)≤Real.exp (39399/25000:ℝ)∧Real.exp (39399/25000:ℝ)≤(483539/100000:ℝ)) ∧
((156557/50000:ℝ)≤Real.exp (5707/5000:ℝ)∧Real.exp (5707/5000:ℝ)≤(62623/20000:ℝ)) ∧
((296931/100000:ℝ)≤Real.exp (108833/100000:ℝ)∧Real.exp (108833/100000:ℝ)≤(74233/25000:ℝ)) ∧
((239857/50000:ℝ)≤Real.exp (78401/50000:ℝ)∧Real.exp (78401/50000:ℝ)≤(95943/20000:ℝ)) ∧
((36563/12500:ℝ)≤Real.exp (107331/100000:ℝ)∧Real.exp (107331/100000:ℝ)≤(58501/20000:ℝ)) ∧
((96419/25000:ℝ)≤Real.exp (134983/100000:ℝ)∧Real.exp (134983/100000:ℝ)≤(385677/100000:ℝ)) ∧
((610147/100000:ℝ)≤Real.exp (180853/100000:ℝ)∧Real.exp (180853/100000:ℝ)≤(152537/25000:ℝ)) ∧
((349761/100000:ℝ)≤Real.exp (15651/12500:ℝ)∧Real.exp (15651/12500:ℝ)≤(174881/50000:ℝ)) ∧
((696139/100000:ℝ)≤Real.exp (97019/50000:ℝ)∧Real.exp (97019/50000:ℝ)≤(34807/5000:ℝ)) ∧
((149037/25000:ℝ)≤Real.exp (44633/25000:ℝ)∧Real.exp (44633/25000:ℝ)≤(596149/100000:ℝ)) ∧
((21471/4000:ℝ)≤Real.exp (168041/100000:ℝ)∧Real.exp (168041/100000:ℝ)≤(67097/12500:ℝ)) ∧
((633449/100000:ℝ)≤Real.exp (184601/100000:ℝ)∧Real.exp (184601/100000:ℝ)≤(12669/2000:ℝ)) ∧
((245597/50000:ℝ)≤Real.exp (159167/100000:ℝ)∧Real.exp (159167/100000:ℝ)≤(98239/20000:ℝ)) ∧
((57859/20000:ℝ)≤Real.exp (26557/25000:ℝ)∧Real.exp (26557/25000:ℝ)≤(18081/6250:ℝ)) ∧
((152713/50000:ℝ)≤Real.exp (55827/50000:ℝ)∧Real.exp (55827/50000:ℝ)≤(305427/100000:ℝ)) ∧
((202713/50000:ℝ)≤Real.exp (139977/100000:ℝ)∧Real.exp (139977/100000:ℝ)≤(405427/100000:ℝ)) ∧
((33979/10000:ℝ)≤Real.exp (30579/25000:ℝ)∧Real.exp (30579/25000:ℝ)≤(339791/100000:ℝ)) ∧
((308457/50000:ℝ)≤Real.exp (45489/25000:ℝ)∧Real.exp (45489/25000:ℝ)≤(123383/20000:ℝ)) ∧
((88761/12500:ℝ)≤Real.exp (98011/50000:ℝ)∧Real.exp (98011/50000:ℝ)≤(710089/100000:ℝ)) ∧
((320981/50000:ℝ)≤Real.exp (11621/6250:ℝ)∧Real.exp (11621/6250:ℝ)≤(641963/100000:ℝ)) ∧
((42427/10000:ℝ)≤Real.exp (3613/2500:ℝ)∧Real.exp (3613/2500:ℝ)≤(424271/100000:ℝ)) ∧
((680971/100000:ℝ)≤Real.exp (38367/20000:ℝ)∧Real.exp (38367/20000:ℝ)≤(170243/25000:ℝ)) ∧
((82813/25000:ℝ)≤Real.exp (119771/100000:ℝ)∧Real.exp (119771/100000:ℝ)≤(331253/100000:ℝ)) ∧
((70131/25000:ℝ)≤Real.exp (103149/100000:ℝ)∧Real.exp (103149/100000:ℝ)≤(11221/4000:ℝ)) ∧
((17631/6250:ℝ)≤Real.exp (25927/25000:ℝ)∧Real.exp (25927/25000:ℝ)≤(282097/100000:ℝ)) ∧
((271833/100000:ℝ)≤Real.exp (50001/50000:ℝ)∧Real.exp (50001/50000:ℝ)≤(135917/50000:ℝ)) ∧
((43651/12500:ℝ)≤Real.exp (2501/2000:ℝ)∧Real.exp (2501/2000:ℝ)≤(349209/100000:ℝ)) ∧
((597097/100000:ℝ)≤Real.exp (178691/100000:ℝ)∧Real.exp (178691/100000:ℝ)≤(298549/50000:ℝ)) ∧
((56849/12500:ℝ)≤Real.exp (151467/100000:ℝ)∧Real.exp (151467/100000:ℝ)≤(454793/100000:ℝ)) ∧
((3574/625:ℝ)≤Real.exp (174369/100000:ℝ)∧Real.exp (174369/100000:ℝ)≤(571841/100000:ℝ)) ∧
((315901/100000:ℝ)≤Real.exp (57513/50000:ℝ)∧Real.exp (57513/50000:ℝ)≤(157951/50000:ℝ)) ∧
((103617/20000:ℝ)≤Real.exp (164497/100000:ℝ)∧Real.exp (164497/100000:ℝ)≤(259043/50000:ℝ)) ∧
((15717/4000:ℝ)≤Real.exp (27369/20000:ℝ)∧Real.exp (27369/20000:ℝ)≤(196463/50000:ℝ)) ∧
((519449/100000:ℝ)≤Real.exp (4119/2500:ℝ)∧Real.exp (4119/2500:ℝ)≤(10389/2000:ℝ)) ∧
((27207/4000:ℝ)≤Real.exp (95859/50000:ℝ)∧Real.exp (95859/50000:ℝ)≤(42511/6250:ℝ)) ∧
((286933/100000:ℝ)≤Real.exp (3294/3125:ℝ)∧Real.exp (3294/3125:ℝ)≤(143467/50000:ℝ)) ∧
((167993/50000:ℝ)≤Real.exp (12119/10000:ℝ)∧Real.exp (12119/10000:ℝ)≤(335987/100000:ℝ)) ∧
((3089/1000:ℝ)≤Real.exp (22557/20000:ℝ)∧Real.exp (22557/20000:ℝ)≤(308901/100000:ℝ)) ∧
((694443/100000:ℝ)≤Real.exp (96897/50000:ℝ)∧Real.exp (96897/50000:ℝ)≤(173611/25000:ℝ)) ∧
((486443/100000:ℝ)≤Real.exp (31639/20000:ℝ)∧Real.exp (31639/20000:ℝ)≤(121611/25000:ℝ)) ∧
((292463/100000:ℝ)≤Real.exp (107317/100000:ℝ)∧Real.exp (107317/100000:ℝ)≤(18279/6250:ℝ)) ∧
((27183/10000:ℝ)≤Real.exp (100001/100000:ℝ)∧Real.exp (100001/100000:ℝ)≤(271831/100000:ℝ)) ∧
((144193/50000:ℝ)≤Real.exp (105913/100000:ℝ)∧Real.exp (105913/100000:ℝ)≤(288387/100000:ℝ)) := 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