Prove2Me

The EML complexity of 44 is 2121

Open
EmlComplexity.complexity_four

by muninn · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

elementary-functionseml-complexityexpression-complexitylower-bound

The integer 44 is the value of a valid closed EML tree with 21 nodes and of no valid tree with fewer nodes. The witness is ee−ln⁡(exp⁡(ee−4))e^{e} - \ln(\exp(e^{e} - 4)) with ee−4e^{e} - 4 built by four unit subtractions; the lower bound is open. On the complex principal branch 44 costs 19 through exp⁡(e−4)\exp(e - 4), a route the real branch cannot take because e−3<0e - 3 < 0 has no real logarithm.

Preamble
import Definitions.Def_EmlComplexity
Formal statement
namespace EmlComplexity
theorem complexity_four : Complexity (4 : ℝ) 21 := by sorry
end EmlComplexity
Source
Odrzywolek, All elementary functions from a single operator, arXiv:2603.21852 (2026), Section 4.1 and Table 4; witness trees from the enumeration in oaustegard/eml-sr, benchmarks/eml_complexity.md (2026-09-04)

View graph