Certified exponential bounds for EML: negative arguments

Proved

EmlComplexity.exp_bounds_negative

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

analysiscertified-computationexponential

For each of the 75 rational negative inputs $x<0$ 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$
$-12$	$\frac{30721}{5000000000}$	$\frac{61443}{10000000000}$
$-\frac{59473}{5000}$	$\frac{68271}{10000000000}$	$\frac{4267}{625000000}$
$-\frac{14867}{1250}$	$\frac{3417}{500000000}$	$\frac{68341}{10000000000}$
$-\frac{1165799}{100000}$	$\frac{2703}{312500000}$	$\frac{86497}{10000000000}$
$-\frac{1143611}{100000}$	$\frac{5399}{500000000}$	$\frac{10799}{1000000000}$
$-\frac{571797}{50000}$	$\frac{27}{2500000}$	$\frac{10801}{1000000000}$
$-\frac{571747}{50000}$	$\frac{10811}{1000000000}$	$\frac{2703}{250000000}$
$-\frac{135247}{12500}$	$\frac{1}{50000}$	$\frac{20001}{1000000000}$
$-\frac{214353}{20000}$	$\frac{443}{20000000}$	$\frac{22151}{1000000000}$
$-\frac{97859}{10000}$	$\frac{56239}{1000000000}$	$\frac{703}{12500000}$
$-\frac{194353}{20000}$	$\frac{60211}{1000000000}$	$\frac{15053}{250000000}$
$-\frac{194333}{20000}$	$\frac{60271}{1000000000}$	$\frac{3767}{62500000}$
$-\frac{239481}{25000}$	$\frac{69149}{1000000000}$	$\frac{1383}{20000000}$
$-\frac{29932}{3125}$	$\frac{34609}{500000000}$	$\frac{69219}{1000000000}$
$-\frac{214481}{25000}$	$\frac{4699}{25000000}$	$\frac{18797}{100000000}$
$-\frac{345387}{50000}$	$\frac{1}{1000}$	$\frac{10001}{10000000}$
$-\frac{633459}{100000}$	$\frac{8869}{5000000}$	$\frac{17739}{10000000}$
$-\frac{305049}{50000}$	$\frac{11203}{5000000}$	$\frac{22407}{10000000}$
$-\frac{302549}{50000}$	$\frac{4711}{2000000}$	$\frac{5889}{2500000}$
$-\frac{255049}{50000}$	$\frac{60907}{10000000}$	$\frac{15227}{2500000}$
$-\frac{16971}{4000}$	$\frac{449}{31250}$	$\frac{14369}{1000000}$
$-\frac{165729}{50000}$	$\frac{36349}{1000000}$	$\frac{727}{20000}$
$-\frac{331317}{100000}$	$\frac{91}{2500}$	$\frac{36401}{1000000}$
$-\frac{164733}{50000}$	$\frac{927}{25000}$	$\frac{37081}{1000000}$
$-\frac{62133}{20000}$	$\frac{179}{4000}$	$\frac{44751}{1000000}$
$-\frac{18391}{6250}$	$\frac{5273}{100000}$	$\frac{52731}{1000000}$
$-\frac{285671}{100000}$	$\frac{57457}{1000000}$	$\frac{28729}{500000}$
$-\frac{8927}{3125}$	$\frac{57461}{1000000}$	$\frac{28731}{500000}$
$-\frac{35583}{12500}$	$\frac{58039}{1000000}$	$\frac{1451}{25000}$
$-\frac{35083}{12500}$	$\frac{60407}{1000000}$	$\frac{7551}{125000}$
$-\frac{271827}{100000}$	$\frac{16497}{250000}$	$\frac{65989}{1000000}$
$-\frac{134237}{50000}$	$\frac{34119}{500000}$	$\frac{68239}{1000000}$
$-\frac{134199}{50000}$	$\frac{6829}{100000}$	$\frac{68291}{1000000}$
$-\frac{132479}{50000}$	$\frac{1767}{25000}$	$\frac{70681}{1000000}$
$-\frac{23153}{10000}$	$\frac{6171}{62500}$	$\frac{98737}{1000000}$
$-\frac{224647}{100000}$	$\frac{10577}{100000}$	$\frac{5289}{50000}$
$-\frac{211717}{100000}$	$\frac{12037}{100000}$	$\frac{6019}{50000}$
$-\frac{186361}{100000}$	$\frac{15511}{100000}$	$\frac{1939}{12500}$
$-\frac{5802}{3125}$	$\frac{15619}{100000}$	$\frac{781}{5000}$
$-\frac{10979}{6250}$	$\frac{8631}{50000}$	$\frac{17263}{100000}$
$-\frac{42957}{25000}$	$\frac{17937}{100000}$	$\frac{8969}{50000}$
$-\frac{85203}{50000}$	$\frac{9097}{50000}$	$\frac{3639}{20000}$
$-\frac{33}{20}$	$\frac{4801}{25000}$	$\frac{3841}{20000}$
$-\frac{1649}{1000}$	$\frac{2403}{12500}$	$\frac{769}{4000}$
$-\frac{4119}{2500}$	$\frac{19251}{100000}$	$\frac{4813}{25000}$
$-\frac{81791}{50000}$	$\frac{19479}{100000}$	$\frac{487}{2500}$
$-\frac{81061}{50000}$	$\frac{3953}{20000}$	$\frac{9883}{50000}$
$-\frac{81047}{50000}$	$\frac{19771}{100000}$	$\frac{4943}{25000}$
$-\frac{30409}{20000}$	$\frac{21861}{100000}$	$\frac{10931}{50000}$
$-\frac{75233}{50000}$	$\frac{22209}{100000}$	$\frac{2221}{10000}$
$-\frac{99999}{100000}$	$\frac{9197}{25000}$	$\frac{36789}{100000}$
$-\frac{999989199}{1000000000}$	$\frac{9197}{25000}$	$\frac{36789}{100000}$
$-\frac{471269}{500000}$	$\frac{38963}{100000}$	$\frac{9741}{25000}$
$-\frac{77937}{100000}$	$\frac{45869}{100000}$	$\frac{4587}{10000}$
$-\frac{19483}{25000}$	$\frac{45871}{100000}$	$\frac{2867}{6250}$
$-\frac{17957}{25000}$	$\frac{48759}{100000}$	$\frac{1219}{2500}$
$-\frac{12721}{20000}$	$\frac{52937}{100000}$	$\frac{26469}{50000}$
$-\frac{30689}{50000}$	$\frac{5413}{10000}$	$\frac{54131}{100000}$
$-\frac{61369}{100000}$	$\frac{27067}{50000}$	$\frac{10827}{20000}$
$-\frac{5413}{10000}$	$\frac{58199}{100000}$	$\frac{291}{500}$
$-\frac{50299}{100000}$	$\frac{60471}{100000}$	$\frac{7559}{12500}$
$-\frac{41291}{100000}$	$\frac{16543}{25000}$	$\frac{66173}{100000}$
$-\frac{5139}{12500}$	$\frac{6629}{10000}$	$\frac{66291}{100000}$
$-\frac{8271}{25000}$	$\frac{8979}{12500}$	$\frac{71833}{100000}$
$-\frac{6277}{25000}$	$\frac{19449}{25000}$	$\frac{77797}{100000}$
$-\frac{1}{4}$	$\frac{1947}{2500}$	$\frac{77881}{100000}$
$-\frac{1019}{6250}$	$\frac{16991}{20000}$	$\frac{21239}{25000}$
$-\frac{2767}{20000}$	$\frac{87079}{100000}$	$\frac{2177}{2500}$
$-\frac{1}{10}$	$\frac{90483}{100000}$	$\frac{22621}{25000}$
$-\frac{1889}{20000}$	$\frac{90987}{100000}$	$\frac{22747}{25000}$
$-\frac{8193}{100000}$	$\frac{92133}{100000}$	$\frac{46067}{50000}$
$-\frac{6927}{100000}$	$\frac{93307}{100000}$	$\frac{23327}{25000}$
$-\frac{1}{20}$	$\frac{47561}{50000}$	$\frac{95123}{100000}$
$-\frac{1}{100}$	$\frac{24751}{25000}$	$\frac{19801}{20000}$
$-\frac{1}{1000}$	$\frac{999}{1000}$	$\frac{99901}{100000}$

Preamble

import Mathlib.Analysis.Complex.ExponentialBounds

Formal statement

theorem EmlComplexity.exp_bounds_negative :
((6829/100000:ℝ)≤Real.exp (-(134199/50000):ℝ)∧Real.exp (-(134199/50000):ℝ)≤(68291/1000000:ℝ)) ∧
((999/1000:ℝ)≤Real.exp (-(1/1000):ℝ)∧Real.exp (-(1/1000):ℝ)≤(99901/100000:ℝ)) ∧
((30721/5000000000:ℝ)≤Real.exp (-12:ℝ)∧Real.exp (-12:ℝ)≤(61443/10000000000:ℝ)) ∧
((91/2500:ℝ)≤Real.exp (-(331317/100000):ℝ)∧Real.exp (-(331317/100000):ℝ)≤(36401/1000000:ℝ)) ∧
((19771/100000:ℝ)≤Real.exp (-(81047/50000):ℝ)∧Real.exp (-(81047/50000):ℝ)≤(4943/25000:ℝ)) ∧
((27067/50000:ℝ)≤Real.exp (-(61369/100000):ℝ)∧Real.exp (-(61369/100000):ℝ)≤(10827/20000:ℝ)) ∧
((47561/50000:ℝ)≤Real.exp (-(1/20):ℝ)∧Real.exp (-(1/20):ℝ)≤(95123/100000:ℝ)) ∧
((27/2500000:ℝ)≤Real.exp (-(571797/50000):ℝ)∧Real.exp (-(571797/50000):ℝ)≤(10801/1000000000:ℝ)) ∧
((57461/1000000:ℝ)≤Real.exp (-(8927/3125):ℝ)∧Real.exp (-(8927/3125):ℝ)≤(28731/500000:ℝ)) ∧
((34119/500000:ℝ)≤Real.exp (-(134237/50000):ℝ)∧Real.exp (-(134237/50000):ℝ)≤(68239/1000000:ℝ)) ∧
((5273/100000:ℝ)≤Real.exp (-(18391/6250):ℝ)∧Real.exp (-(18391/6250):ℝ)≤(52731/1000000:ℝ)) ∧
((2403/12500:ℝ)≤Real.exp (-(1649/1000):ℝ)∧Real.exp (-(1649/1000):ℝ)≤(769/4000:ℝ)) ∧
((12037/100000:ℝ)≤Real.exp (-(211717/100000):ℝ)∧Real.exp (-(211717/100000):ℝ)≤(6019/50000:ℝ)) ∧
((16543/25000:ℝ)≤Real.exp (-(41291/100000):ℝ)∧Real.exp (-(41291/100000):ℝ)≤(66173/100000:ℝ)) ∧
((19449/25000:ℝ)≤Real.exp (-(6277/25000):ℝ)∧Real.exp (-(6277/25000):ℝ)≤(77797/100000:ℝ)) ∧
((1/1000:ℝ)≤Real.exp (-(345387/50000):ℝ)∧Real.exp (-(345387/50000):ℝ)≤(10001/10000000:ℝ)) ∧
((24751/25000:ℝ)≤Real.exp (-(1/100):ℝ)∧Real.exp (-(1/100):ℝ)≤(19801/20000:ℝ)) ∧
((45869/100000:ℝ)≤Real.exp (-(77937/100000):ℝ)∧Real.exp (-(77937/100000):ℝ)≤(4587/10000:ℝ)) ∧
((1767/25000:ℝ)≤Real.exp (-(132479/50000):ℝ)∧Real.exp (-(132479/50000):ℝ)≤(70681/1000000:ℝ)) ∧
((90483/100000:ℝ)≤Real.exp (-(1/10):ℝ)∧Real.exp (-(1/10):ℝ)≤(22621/25000:ℝ)) ∧
((10811/1000000000:ℝ)≤Real.exp (-(571747/50000):ℝ)∧Real.exp (-(571747/50000):ℝ)≤(2703/250000000:ℝ)) ∧
((60407/1000000:ℝ)≤Real.exp (-(35083/12500):ℝ)∧Real.exp (-(35083/12500):ℝ)≤(7551/125000:ℝ)) ∧
((68271/10000000000:ℝ)≤Real.exp (-(59473/5000):ℝ)∧Real.exp (-(59473/5000):ℝ)≤(4267/625000000:ℝ)) ∧
((60211/1000000000:ℝ)≤Real.exp (-(194353/20000):ℝ)∧Real.exp (-(194353/20000):ℝ)≤(15053/250000000:ℝ)) ∧
((15619/100000:ℝ)≤Real.exp (-(5802/3125):ℝ)∧Real.exp (-(5802/3125):ℝ)≤(781/5000:ℝ)) ∧
((11203/5000000:ℝ)≤Real.exp (-(305049/50000):ℝ)∧Real.exp (-(305049/50000):ℝ)≤(22407/10000000:ℝ)) ∧
((69149/1000000000:ℝ)≤Real.exp (-(239481/25000):ℝ)∧Real.exp (-(239481/25000):ℝ)≤(1383/20000000:ℝ)) ∧
((17937/100000:ℝ)≤Real.exp (-(42957/25000):ℝ)∧Real.exp (-(42957/25000):ℝ)≤(8969/50000:ℝ)) ∧
((9197/25000:ℝ)≤Real.exp (-(99999/100000):ℝ)∧Real.exp (-(99999/100000):ℝ)≤(36789/100000:ℝ)) ∧
((92133/100000:ℝ)≤Real.exp (-(8193/100000):ℝ)∧Real.exp (-(8193/100000):ℝ)≤(46067/50000:ℝ)) ∧
((36349/1000000:ℝ)≤Real.exp (-(165729/50000):ℝ)∧Real.exp (-(165729/50000):ℝ)≤(727/20000:ℝ)) ∧
((3953/20000:ℝ)≤Real.exp (-(81061/50000):ℝ)∧Real.exp (-(81061/50000):ℝ)≤(9883/50000:ℝ)) ∧
((5413/10000:ℝ)≤Real.exp (-(30689/50000):ℝ)∧Real.exp (-(30689/50000):ℝ)≤(54131/100000:ℝ)) ∧
((179/4000:ℝ)≤Real.exp (-(62133/20000):ℝ)∧Real.exp (-(62133/20000):ℝ)≤(44751/1000000:ℝ)) ∧
((19479/100000:ℝ)≤Real.exp (-(81791/50000):ℝ)∧Real.exp (-(81791/50000):ℝ)≤(487/2500:ℝ)) ∧
((9097/50000:ℝ)≤Real.exp (-(85203/50000):ℝ)∧Real.exp (-(85203/50000):ℝ)≤(3639/20000:ℝ)) ∧
((10577/100000:ℝ)≤Real.exp (-(224647/100000):ℝ)∧Real.exp (-(224647/100000):ℝ)≤(5289/50000:ℝ)) ∧
((15511/100000:ℝ)≤Real.exp (-(186361/100000):ℝ)∧Real.exp (-(186361/100000):ℝ)≤(1939/12500:ℝ)) ∧
((45871/100000:ℝ)≤Real.exp (-(19483/25000):ℝ)∧Real.exp (-(19483/25000):ℝ)≤(2867/6250:ℝ)) ∧
((60471/100000:ℝ)≤Real.exp (-(50299/100000):ℝ)∧Real.exp (-(50299/100000):ℝ)≤(7559/12500:ℝ)) ∧
((90987/100000:ℝ)≤Real.exp (-(1889/20000):ℝ)∧Real.exp (-(1889/20000):ℝ)≤(22747/25000:ℝ)) ∧
((93307/100000:ℝ)≤Real.exp (-(6927/100000):ℝ)∧Real.exp (-(6927/100000):ℝ)≤(23327/25000:ℝ)) ∧
((6629/10000:ℝ)≤Real.exp (-(5139/12500):ℝ)∧Real.exp (-(5139/12500):ℝ)≤(66291/100000:ℝ)) ∧
((22209/100000:ℝ)≤Real.exp (-(75233/50000):ℝ)∧Real.exp (-(75233/50000):ℝ)≤(2221/10000:ℝ)) ∧
((1947/2500:ℝ)≤Real.exp (-(1/4):ℝ)∧Real.exp (-(1/4):ℝ)≤(77881/100000:ℝ)) ∧
((52937/100000:ℝ)≤Real.exp (-(12721/20000):ℝ)∧Real.exp (-(12721/20000):ℝ)≤(26469/50000:ℝ)) ∧
((927/25000:ℝ)≤Real.exp (-(164733/50000):ℝ)∧Real.exp (-(164733/50000):ℝ)≤(37081/1000000:ℝ)) ∧
((21861/100000:ℝ)≤Real.exp (-(30409/20000):ℝ)∧Real.exp (-(30409/20000):ℝ)≤(10931/50000:ℝ)) ∧
((8979/12500:ℝ)≤Real.exp (-(8271/25000):ℝ)∧Real.exp (-(8271/25000):ℝ)≤(71833/100000:ℝ)) ∧
((1/50000:ℝ)≤Real.exp (-(135247/12500):ℝ)∧Real.exp (-(135247/12500):ℝ)≤(20001/1000000000:ℝ)) ∧
((16991/20000:ℝ)≤Real.exp (-(1019/6250):ℝ)∧Real.exp (-(1019/6250):ℝ)≤(21239/25000:ℝ)) ∧
((58039/1000000:ℝ)≤Real.exp (-(35583/12500):ℝ)∧Real.exp (-(35583/12500):ℝ)≤(1451/25000:ℝ)) ∧
((3417/500000000:ℝ)≤Real.exp (-(14867/1250):ℝ)∧Real.exp (-(14867/1250):ℝ)≤(68341/10000000000:ℝ)) ∧
((60271/1000000000:ℝ)≤Real.exp (-(194333/20000):ℝ)∧Real.exp (-(194333/20000):ℝ)≤(3767/62500000:ℝ)) ∧
((8631/50000:ℝ)≤Real.exp (-(10979/6250):ℝ)∧Real.exp (-(10979/6250):ℝ)≤(17263/100000:ℝ)) ∧
((4711/2000000:ℝ)≤Real.exp (-(302549/50000):ℝ)∧Real.exp (-(302549/50000):ℝ)≤(5889/2500000:ℝ)) ∧
((2703/312500000:ℝ)≤Real.exp (-(1165799/100000):ℝ)∧Real.exp (-(1165799/100000):ℝ)≤(86497/10000000000:ℝ)) ∧
((56239/1000000000:ℝ)≤Real.exp (-(97859/10000):ℝ)∧Real.exp (-(97859/10000):ℝ)≤(703/12500000:ℝ)) ∧
((443/20000000:ℝ)≤Real.exp (-(214353/20000):ℝ)∧Real.exp (-(214353/20000):ℝ)≤(22151/1000000000:ℝ)) ∧
((6171/62500:ℝ)≤Real.exp (-(23153/10000):ℝ)∧Real.exp (-(23153/10000):ℝ)≤(98737/1000000:ℝ)) ∧
((87079/100000:ℝ)≤Real.exp (-(2767/20000):ℝ)∧Real.exp (-(2767/20000):ℝ)≤(2177/2500:ℝ)) ∧
((60907/10000000:ℝ)≤Real.exp (-(255049/50000):ℝ)∧Real.exp (-(255049/50000):ℝ)≤(15227/2500000:ℝ)) ∧
((449/31250:ℝ)≤Real.exp (-(16971/4000):ℝ)∧Real.exp (-(16971/4000):ℝ)≤(14369/1000000:ℝ)) ∧
((34609/500000000:ℝ)≤Real.exp (-(29932/3125):ℝ)∧Real.exp (-(29932/3125):ℝ)≤(69219/1000000000:ℝ)) ∧
((4699/25000000:ℝ)≤Real.exp (-(214481/25000):ℝ)∧Real.exp (-(214481/25000):ℝ)≤(18797/100000000:ℝ)) ∧
((8869/5000000:ℝ)≤Real.exp (-(633459/100000):ℝ)∧Real.exp (-(633459/100000):ℝ)≤(17739/10000000:ℝ)) ∧
((4801/25000:ℝ)≤Real.exp (-(33/20):ℝ)∧Real.exp (-(33/20):ℝ)≤(3841/20000:ℝ)) ∧
((48759/100000:ℝ)≤Real.exp (-(17957/25000):ℝ)∧Real.exp (-(17957/25000):ℝ)≤(1219/2500:ℝ)) ∧
((19251/100000:ℝ)≤Real.exp (-(4119/2500):ℝ)∧Real.exp (-(4119/2500):ℝ)≤(4813/25000:ℝ)) ∧
((58199/100000:ℝ)≤Real.exp (-(5413/10000):ℝ)∧Real.exp (-(5413/10000):ℝ)≤(291/500:ℝ)) ∧
((16497/250000:ℝ)≤Real.exp (-(271827/100000):ℝ)∧Real.exp (-(271827/100000):ℝ)≤(65989/1000000:ℝ)) ∧
((9197/25000:ℝ)≤Real.exp (-(999989199/1000000000):ℝ)∧Real.exp (-(999989199/1000000000):ℝ)≤(36789/100000:ℝ)) ∧
((38963/100000:ℝ)≤Real.exp (-(471269/500000):ℝ)∧Real.exp (-(471269/500000):ℝ)≤(9741/25000:ℝ)) ∧
((5399/500000000:ℝ)≤Real.exp (-(1143611/100000):ℝ)∧Real.exp (-(1143611/100000):ℝ)≤(10799/1000000000:ℝ)) ∧
((57457/1000000:ℝ)≤Real.exp (-(285671/100000):ℝ)∧Real.exp (-(285671/100000):ℝ)≤(28729/500000:ℝ)) := 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