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

Proved

EmlComplexity.exp_bounds_unit

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

analysiscertified-computationexponential

For each of the 92 rational inputs $0\leq x<1$ 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$
$0$	$1$	$1$
$\frac{4267}{625000000}$	$1$	$\frac{100001}{100000}$
$\frac{1}{100000}$	$\frac{100001}{100000}$	$\frac{50001}{50000}$
$\frac{5399}{500000000}$	$\frac{100001}{100000}$	$\frac{50001}{50000}$
$\frac{10801}{1000000000}$	$\frac{100001}{100000}$	$\frac{50001}{50000}$
$\frac{2703}{250000000}$	$\frac{100001}{100000}$	$\frac{50001}{50000}$
$\frac{1}{50000}$	$\frac{50001}{50000}$	$\frac{100003}{100000}$
$\frac{15053}{250000000}$	$\frac{50003}{50000}$	$\frac{100007}{100000}$
$\frac{1383}{20000000}$	$\frac{50003}{50000}$	$\frac{100007}{100000}$
$\frac{1}{1000}$	$\frac{1001}{1000}$	$\frac{100101}{100000}$
$\frac{101}{100000}$	$\frac{100101}{100000}$	$\frac{50051}{50000}$
$\frac{22407}{10000000}$	$\frac{3132}{3125}$	$\frac{4009}{4000}$
$\frac{1}{100}$	$\frac{20201}{20000}$	$\frac{50503}{50000}$
$\frac{1551}{50000}$	$\frac{2063}{2000}$	$\frac{103151}{100000}$
$\frac{727}{20000}$	$\frac{103701}{100000}$	$\frac{51851}{50000}$
$\frac{91}{2500}$	$\frac{103707}{100000}$	$\frac{25927}{25000}$
$\frac{927}{25000}$	$\frac{103777}{100000}$	$\frac{51889}{50000}$
$\frac{179}{4000}$	$\frac{3268}{3125}$	$\frac{104577}{100000}$
$\frac{1}{20}$	$\frac{105127}{100000}$	$\frac{13141}{12500}$
$\frac{5267}{100000}$	$\frac{3294}{3125}$	$\frac{105409}{100000}$
$\frac{5273}{100000}$	$\frac{52707}{50000}$	$\frac{21083}{20000}$
$\frac{57457}{1000000}$	$\frac{105913}{100000}$	$\frac{52957}{50000}$
$\frac{28731}{500000}$	$\frac{52957}{50000}$	$\frac{21183}{20000}$
$\frac{7551}{125000}$	$\frac{53113}{50000}$	$\frac{106227}{100000}$
$\frac{853}{12500}$	$\frac{53531}{50000}$	$\frac{107063}{100000}$
$\frac{6829}{100000}$	$\frac{107067}{100000}$	$\frac{26767}{25000}$
$\frac{3531}{50000}$	$\frac{107317}{100000}$	$\frac{53659}{50000}$
$\frac{1767}{25000}$	$\frac{107323}{100000}$	$\frac{26831}{25000}$
$\frac{973}{10000}$	$\frac{110219}{100000}$	$\frac{5511}{5000}$
$\frac{1}{10}$	$\frac{110517}{100000}$	$\frac{55259}{50000}$
$\frac{10577}{100000}$	$\frac{27789}{25000}$	$\frac{111157}{100000}$
$\frac{376}{3125}$	$\frac{22557}{20000}$	$\frac{56393}{50000}$
$\frac{12037}{100000}$	$\frac{112791}{100000}$	$\frac{14099}{12500}$
$\frac{7003}{50000}$	$\frac{57517}{50000}$	$\frac{23007}{20000}$
$\frac{15511}{100000}$	$\frac{58389}{50000}$	$\frac{116779}{100000}$
$\frac{781}{5000}$	$\frac{23381}{20000}$	$\frac{58453}{50000}$
$\frac{8969}{50000}$	$\frac{119647}{100000}$	$\frac{3739}{3125}$
$\frac{3607}{20000}$	$\frac{119763}{100000}$	$\frac{29941}{25000}$
$\frac{18043}{100000}$	$\frac{119773}{100000}$	$\frac{59887}{50000}$
$\frac{9097}{50000}$	$\frac{59977}{50000}$	$\frac{23991}{20000}$
$\frac{19219}{100000}$	$\frac{12119}{10000}$	$\frac{121191}{100000}$
$\frac{2403}{12500}$	$\frac{30299}{25000}$	$\frac{121197}{100000}$
$\frac{19479}{100000}$	$\frac{24301}{20000}$	$\frac{60753}{50000}$
$\frac{9883}{50000}$	$\frac{60927}{50000}$	$\frac{24371}{20000}$
$\frac{19771}{100000}$	$\frac{6093}{5000}$	$\frac{121861}{100000}$
$\frac{21861}{100000}$	$\frac{62217}{50000}$	$\frac{24887}{20000}$
$\frac{22209}{100000}$	$\frac{31217}{25000}$	$\frac{124869}{100000}$
$\frac{4473}{20000}$	$\frac{125063}{100000}$	$\frac{15633}{12500}$
$\frac{1}{4}$	$\frac{64201}{50000}$	$\frac{128403}{100000}$
$\frac{15687}{50000}$	$\frac{136853}{100000}$	$\frac{68427}{50000}$
$\frac{36789}{100000}$	$\frac{36117}{25000}$	$\frac{144469}{100000}$
$\frac{20763}{50000}$	$\frac{37869}{25000}$	$\frac{151477}{100000}$
$\frac{41913}{100000}$	$\frac{152063}{100000}$	$\frac{4752}{3125}$
$\frac{22933}{50000}$	$\frac{31639}{20000}$	$\frac{39549}{25000}$
$\frac{45869}{100000}$	$\frac{791}{500}$	$\frac{158201}{100000}$
$\frac{45871}{100000}$	$\frac{158203}{100000}$	$\frac{39551}{25000}$
$\frac{49779}{100000}$	$\frac{41127}{25000}$	$\frac{164509}{100000}$
$\frac{24969}{50000}$	$\frac{164769}{100000}$	$\frac{16477}{10000}$
$\frac{12801}{25000}$	$\frac{166869}{100000}$	$\frac{16687}{10000}$
$\frac{52937}{100000}$	$\frac{84893}{50000}$	$\frac{169787}{100000}$
$\frac{54131}{100000}$	$\frac{6873}{4000}$	$\frac{85913}{50000}$
$\frac{27067}{50000}$	$\frac{17183}{10000}$	$\frac{171831}{100000}$
$\frac{11121}{20000}$	$\frac{174377}{100000}$	$\frac{87189}{50000}$
$\frac{11611}{20000}$	$\frac{89351}{50000}$	$\frac{178703}{100000}$
$\frac{60471}{100000}$	$\frac{5721}{3125}$	$\frac{183073}{100000}$
$\frac{65097}{100000}$	$\frac{191739}{100000}$	$\frac{9587}{5000}$
$\frac{66163}{100000}$	$\frac{96897}{50000}$	$\frac{38759}{20000}$
$\frac{66171}{100000}$	$\frac{19381}{10000}$	$\frac{193811}{100000}$
$\frac{16571}{25000}$	$\frac{194029}{100000}$	$\frac{19403}{10000}$
$\frac{6629}{10000}$	$\frac{194041}{100000}$	$\frac{97021}{50000}$
$\frac{34601}{50000}$	$\frac{99887}{50000}$	$\frac{7991}{4000}$
$\frac{8651}{12500}$	$\frac{99893}{50000}$	$\frac{199787}{100000}$
$\frac{70621}{100000}$	$\frac{202629}{100000}$	$\frac{20263}{10000}$
$\frac{2873}{4000}$	$\frac{51271}{25000}$	$\frac{41017}{20000}$
$\frac{14409}{20000}$	$\frac{41107}{20000}$	$\frac{6423}{3125}$
$\frac{72051}{100000}$	$\frac{51387}{25000}$	$\frac{205549}{100000}$
$\frac{77791}{100000}$	$\frac{217691}{100000}$	$\frac{54423}{25000}$
$\frac{15559}{20000}$	$\frac{2177}{1000}$	$\frac{217701}{100000}$
$\frac{79127}{100000}$	$\frac{220619}{100000}$	$\frac{11031}{5000}$
$\frac{3353}{4000}$	$\frac{231231}{100000}$	$\frac{7226}{3125}$
$\frac{3639}{4000}$	$\frac{24837}{10000}$	$\frac{248371}{100000}$
$\frac{11513}{12500}$	$\frac{25119}{10000}$	$\frac{251191}{100000}$
$\frac{92447}{100000}$	$\frac{252053}{100000}$	$\frac{126027}{50000}$
$\frac{9313}{10000}$	$\frac{12689}{5000}$	$\frac{253781}{100000}$
$\frac{93137}{100000}$	$\frac{126899}{50000}$	$\frac{253799}{100000}$
$\frac{5831}{6250}$	$\frac{127101}{50000}$	$\frac{254203}{100000}$
$\frac{96353}{100000}$	$\frac{262093}{100000}$	$\frac{131047}{50000}$
$\frac{48727}{50000}$	$\frac{132497}{50000}$	$\frac{52999}{20000}$
$\frac{97459}{100000}$	$\frac{16563}{6250}$	$\frac{265009}{100000}$
$\frac{98651}{100000}$	$\frac{53637}{20000}$	$\frac{134093}{50000}$
$\frac{98851}{100000}$	$\frac{134361}{50000}$	$\frac{268723}{100000}$
$\frac{49999}{50000}$	$\frac{135911}{50000}$	$\frac{271823}{100000}$

Preamble

import Mathlib.Analysis.Complex.ExponentialBounds

Formal statement

theorem EmlComplexity.exp_bounds_unit :
((17183/10000:ℝ)≤Real.exp (27067/50000:ℝ)∧Real.exp (27067/50000:ℝ)≤(171831/100000:ℝ)) ∧
((217691/100000:ℝ)≤Real.exp (77791/100000:ℝ)∧Real.exp (77791/100000:ℝ)≤(54423/25000:ℝ)) ∧
((194041/100000:ℝ)≤Real.exp (6629/10000:ℝ)∧Real.exp (6629/10000:ℝ)≤(97021/50000:ℝ)) ∧
((6873/4000:ℝ)≤Real.exp (54131/100000:ℝ)∧Real.exp (54131/100000:ℝ)≤(85913/50000:ℝ)) ∧
((2177/1000:ℝ)≤Real.exp (15559/20000:ℝ)∧Real.exp (15559/20000:ℝ)≤(217701/100000:ℝ)) ∧
((1001/1000:ℝ)≤Real.exp (1/1000:ℝ)∧Real.exp (1/1000:ℝ)≤(100101/100000:ℝ)) ∧
((107067/100000:ℝ)≤Real.exp (6829/100000:ℝ)∧Real.exp (6829/100000:ℝ)≤(26767/25000:ℝ)) ∧
((41107/20000:ℝ)≤Real.exp (14409/20000:ℝ)∧Real.exp (14409/20000:ℝ)≤(6423/3125:ℝ)) ∧
((119773/100000:ℝ)≤Real.exp (18043/100000:ℝ)∧Real.exp (18043/100000:ℝ)≤(59887/50000:ℝ)) ∧
((105127/100000:ℝ)≤Real.exp (1/20:ℝ)∧Real.exp (1/20:ℝ)≤(13141/12500:ℝ)) ∧
((103707/100000:ℝ)≤Real.exp (91/2500:ℝ)∧Real.exp (91/2500:ℝ)≤(25927/25000:ℝ)) ∧
((6093/5000:ℝ)≤Real.exp (19771/100000:ℝ)∧Real.exp (19771/100000:ℝ)≤(121861/100000:ℝ)) ∧
((53531/50000:ℝ)≤Real.exp (853/12500:ℝ)∧Real.exp (853/12500:ℝ)≤(107063/100000:ℝ)) ∧
((100001/100000:ℝ)≤Real.exp (1/100000:ℝ)∧Real.exp (1/100000:ℝ)≤(50001/50000:ℝ)) ∧
((99893/50000:ℝ)≤Real.exp (8651/12500:ℝ)∧Real.exp (8651/12500:ℝ)≤(199787/100000:ℝ)) ∧
((194029/100000:ℝ)≤Real.exp (16571/25000:ℝ)∧Real.exp (16571/25000:ℝ)≤(19403/10000:ℝ)) ∧
((51387/25000:ℝ)≤Real.exp (72051/100000:ℝ)∧Real.exp (72051/100000:ℝ)≤(205549/100000:ℝ)) ∧
((2063/2000:ℝ)≤Real.exp (1551/50000:ℝ)∧Real.exp (1551/50000:ℝ)≤(103151/100000:ℝ)) ∧
((12689/5000:ℝ)≤Real.exp (9313/10000:ℝ)∧Real.exp (9313/10000:ℝ)≤(253781/100000:ℝ)) ∧
((110219/100000:ℝ)≤Real.exp (973/10000:ℝ)∧Real.exp (973/10000:ℝ)≤(5511/5000:ℝ)) ∧
((166869/100000:ℝ)≤Real.exp (12801/25000:ℝ)∧Real.exp (12801/25000:ℝ)≤(16687/10000:ℝ)) ∧
((132497/50000:ℝ)≤Real.exp (48727/50000:ℝ)∧Real.exp (48727/50000:ℝ)≤(52999/20000:ℝ)) ∧
((20201/20000:ℝ)≤Real.exp (1/100:ℝ)∧Real.exp (1/100:ℝ)≤(50503/50000:ℝ)) ∧
((110517/100000:ℝ)≤Real.exp (1/10:ℝ)∧Real.exp (1/10:ℝ)≤(55259/50000:ℝ)) ∧
((52707/50000:ℝ)≤Real.exp (5273/100000:ℝ)∧Real.exp (5273/100000:ℝ)≤(21083/20000:ℝ)) ∧
((30299/25000:ℝ)≤Real.exp (2403/12500:ℝ)∧Real.exp (2403/12500:ℝ)≤(121197/100000:ℝ)) ∧
((112791/100000:ℝ)≤Real.exp (12037/100000:ℝ)∧Real.exp (12037/100000:ℝ)≤(14099/12500:ℝ)) ∧
((19381/10000:ℝ)≤Real.exp (66171/100000:ℝ)∧Real.exp (66171/100000:ℝ)≤(193811/100000:ℝ)) ∧
((791/500:ℝ)≤Real.exp (45869/100000:ℝ)∧Real.exp (45869/100000:ℝ)≤(158201/100000:ℝ)) ∧
((107323/100000:ℝ)≤Real.exp (1767/25000:ℝ)∧Real.exp (1767/25000:ℝ)≤(26831/25000:ℝ)) ∧
((103701/100000:ℝ)≤Real.exp (727/20000:ℝ)∧Real.exp (727/20000:ℝ)≤(51851/50000:ℝ)) ∧
((60927/50000:ℝ)≤Real.exp (9883/50000:ℝ)∧Real.exp (9883/50000:ℝ)≤(24371/20000:ℝ)) ∧
((100001/100000:ℝ)≤Real.exp (10801/1000000000:ℝ)∧Real.exp (10801/1000000000:ℝ)≤(50001/50000:ℝ)) ∧
((52957/50000:ℝ)≤Real.exp (28731/500000:ℝ)∧Real.exp (28731/500000:ℝ)≤(21183/20000:ℝ)) ∧
((1:ℝ)≤Real.exp 0∧Real.exp 0≤1) ∧
((99887/50000:ℝ)≤Real.exp (34601/50000:ℝ)∧Real.exp (34601/50000:ℝ)≤(7991/4000:ℝ)) ∧
((202629/100000:ℝ)≤Real.exp (70621/100000:ℝ)∧Real.exp (70621/100000:ℝ)≤(20263/10000:ℝ)) ∧
((134361/50000:ℝ)≤Real.exp (98851/100000:ℝ)∧Real.exp (98851/100000:ℝ)≤(268723/100000:ℝ)) ∧
((125063/100000:ℝ)≤Real.exp (4473/20000:ℝ)∧Real.exp (4473/20000:ℝ)≤(15633/12500:ℝ)) ∧
((89351/50000:ℝ)≤Real.exp (11611/20000:ℝ)∧Real.exp (11611/20000:ℝ)≤(178703/100000:ℝ)) ∧
((119763/100000:ℝ)≤Real.exp (3607/20000:ℝ)∧Real.exp (3607/20000:ℝ)≤(29941/25000:ℝ)) ∧
((126899/50000:ℝ)≤Real.exp (93137/100000:ℝ)∧Real.exp (93137/100000:ℝ)≤(253799/100000:ℝ)) ∧
((37869/25000:ℝ)≤Real.exp (20763/50000:ℝ)∧Real.exp (20763/50000:ℝ)≤(151477/100000:ℝ)) ∧
((262093/100000:ℝ)≤Real.exp (96353/100000:ℝ)∧Real.exp (96353/100000:ℝ)≤(131047/50000:ℝ)) ∧
((220619/100000:ℝ)≤Real.exp (79127/100000:ℝ)∧Real.exp (79127/100000:ℝ)≤(11031/5000:ℝ)) ∧
((174377/100000:ℝ)≤Real.exp (11121/20000:ℝ)∧Real.exp (11121/20000:ℝ)≤(87189/50000:ℝ)) ∧
((16563/6250:ℝ)≤Real.exp (97459/100000:ℝ)∧Real.exp (97459/100000:ℝ)≤(265009/100000:ℝ)) ∧
((57517/50000:ℝ)≤Real.exp (7003/50000:ℝ)∧Real.exp (7003/50000:ℝ)≤(23007/20000:ℝ)) ∧
((41127/25000:ℝ)≤Real.exp (49779/100000:ℝ)∧Real.exp (49779/100000:ℝ)≤(164509/100000:ℝ)) ∧
((136853/100000:ℝ)≤Real.exp (15687/50000:ℝ)∧Real.exp (15687/50000:ℝ)≤(68427/50000:ℝ)) ∧
((53637/20000:ℝ)≤Real.exp (98651/100000:ℝ)∧Real.exp (98651/100000:ℝ)≤(134093/50000:ℝ)) ∧
((252053/100000:ℝ)≤Real.exp (92447/100000:ℝ)∧Real.exp (92447/100000:ℝ)≤(126027/50000:ℝ)) ∧
((152063/100000:ℝ)≤Real.exp (41913/100000:ℝ)∧Real.exp (41913/100000:ℝ)≤(4752/3125:ℝ)) ∧
((164769/100000:ℝ)≤Real.exp (24969/50000:ℝ)∧Real.exp (24969/50000:ℝ)≤(16477/10000:ℝ)) ∧
((135911/50000:ℝ)≤Real.exp (49999/50000:ℝ)∧Real.exp (49999/50000:ℝ)≤(271823/100000:ℝ)) ∧
((100101/100000:ℝ)≤Real.exp (101/100000:ℝ)∧Real.exp (101/100000:ℝ)≤(50051/50000:ℝ)) ∧
((64201/50000:ℝ)≤Real.exp (1/4:ℝ)∧Real.exp (1/4:ℝ)≤(128403/100000:ℝ)) ∧
((231231/100000:ℝ)≤Real.exp (3353/4000:ℝ)∧Real.exp (3353/4000:ℝ)≤(7226/3125:ℝ)) ∧
((191739/100000:ℝ)≤Real.exp (65097/100000:ℝ)∧Real.exp (65097/100000:ℝ)≤(9587/5000:ℝ)) ∧
((25119/10000:ℝ)≤Real.exp (11513/12500:ℝ)∧Real.exp (11513/12500:ℝ)≤(251191/100000:ℝ)) ∧
((3268/3125:ℝ)≤Real.exp (179/4000:ℝ)∧Real.exp (179/4000:ℝ)≤(104577/100000:ℝ)) ∧
((24301/20000:ℝ)≤Real.exp (19479/100000:ℝ)∧Real.exp (19479/100000:ℝ)≤(60753/50000:ℝ)) ∧
((59977/50000:ℝ)≤Real.exp (9097/50000:ℝ)∧Real.exp (9097/50000:ℝ)≤(23991/20000:ℝ)) ∧
((27789/25000:ℝ)≤Real.exp (10577/100000:ℝ)∧Real.exp (10577/100000:ℝ)≤(111157/100000:ℝ)) ∧
((58389/50000:ℝ)≤Real.exp (15511/100000:ℝ)∧Real.exp (15511/100000:ℝ)≤(116779/100000:ℝ)) ∧
((158203/100000:ℝ)≤Real.exp (45871/100000:ℝ)∧Real.exp (45871/100000:ℝ)≤(39551/25000:ℝ)) ∧
((5721/3125:ℝ)≤Real.exp (60471/100000:ℝ)∧Real.exp (60471/100000:ℝ)≤(183073/100000:ℝ)) ∧
((24837/10000:ℝ)≤Real.exp (3639/4000:ℝ)∧Real.exp (3639/4000:ℝ)≤(248371/100000:ℝ)) ∧
((127101/50000:ℝ)≤Real.exp (5831/6250:ℝ)∧Real.exp (5831/6250:ℝ)≤(254203/100000:ℝ)) ∧
((31217/25000:ℝ)≤Real.exp (22209/100000:ℝ)∧Real.exp (22209/100000:ℝ)≤(124869/100000:ℝ)) ∧
((84893/50000:ℝ)≤Real.exp (52937/100000:ℝ)∧Real.exp (52937/100000:ℝ)≤(169787/100000:ℝ)) ∧
((103777/100000:ℝ)≤Real.exp (927/25000:ℝ)∧Real.exp (927/25000:ℝ)≤(51889/50000:ℝ)) ∧
((62217/50000:ℝ)≤Real.exp (21861/100000:ℝ)∧Real.exp (21861/100000:ℝ)≤(24887/20000:ℝ)) ∧
((51271/25000:ℝ)≤Real.exp (2873/4000:ℝ)∧Real.exp (2873/4000:ℝ)≤(41017/20000:ℝ)) ∧
((50001/50000:ℝ)≤Real.exp (1/50000:ℝ)∧Real.exp (1/50000:ℝ)≤(100003/100000:ℝ)) ∧
((3294/3125:ℝ)≤Real.exp (5267/100000:ℝ)∧Real.exp (5267/100000:ℝ)≤(105409/100000:ℝ)) ∧
((12119/10000:ℝ)≤Real.exp (19219/100000:ℝ)∧Real.exp (19219/100000:ℝ)≤(121191/100000:ℝ)) ∧
((22557/20000:ℝ)≤Real.exp (376/3125:ℝ)∧Real.exp (376/3125:ℝ)≤(56393/50000:ℝ)) ∧
((96897/50000:ℝ)≤Real.exp (66163/100000:ℝ)∧Real.exp (66163/100000:ℝ)≤(38759/20000:ℝ)) ∧
((100001/100000:ℝ)≤Real.exp (2703/250000000:ℝ)∧Real.exp (2703/250000000:ℝ)≤(50001/50000:ℝ)) ∧
((53113/50000:ℝ)≤Real.exp (7551/125000:ℝ)∧Real.exp (7551/125000:ℝ)≤(106227/100000:ℝ)) ∧
((1:ℝ)≤Real.exp (4267/625000000:ℝ)∧Real.exp (4267/625000000:ℝ)≤(100001/100000:ℝ)) ∧
((50003/50000:ℝ)≤Real.exp (15053/250000000:ℝ)∧Real.exp (15053/250000000:ℝ)≤(100007/100000:ℝ)) ∧
((23381/20000:ℝ)≤Real.exp (781/5000:ℝ)∧Real.exp (781/5000:ℝ)≤(58453/50000:ℝ)) ∧
((3132/3125:ℝ)≤Real.exp (22407/10000000:ℝ)∧Real.exp (22407/10000000:ℝ)≤(4009/4000:ℝ)) ∧
((50003/50000:ℝ)≤Real.exp (1383/20000000:ℝ)∧Real.exp (1383/20000000:ℝ)≤(100007/100000:ℝ)) ∧
((31639/20000:ℝ)≤Real.exp (22933/50000:ℝ)∧Real.exp (22933/50000:ℝ)≤(39549/25000:ℝ)) ∧
((119647/100000:ℝ)≤Real.exp (8969/50000:ℝ)∧Real.exp (8969/50000:ℝ)≤(3739/3125:ℝ)) ∧
((107317/100000:ℝ)≤Real.exp (3531/50000:ℝ)∧Real.exp (3531/50000:ℝ)≤(53659/50000:ℝ)) ∧
((36117/25000:ℝ)≤Real.exp (36789/100000:ℝ)∧Real.exp (36789/100000:ℝ)≤(144469/100000:ℝ)) ∧
((100001/100000:ℝ)≤Real.exp (5399/500000000:ℝ)∧Real.exp (5399/500000000:ℝ)≤(50001/50000:ℝ)) ∧
((105913/100000:ℝ)≤Real.exp (57457/1000000:ℝ)∧Real.exp (57457/1000000:ℝ)≤(52957/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