$e-2$ has EML complexity at most 7

Proved

EmlComplexity.attains_e_sub_two

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

elementary-functionseml-complexityexpression-complexity

The constant $e - 2$ is the value of a valid closed EML tree with seven nodes. The tree computes $\ln(e-1)$ in five nodes and then subtracts $1$ through $\exp(\ln(e-1)) - \ln e$ .

Preamble

import Definitions.Def_EmlComplexity

Formal statement

namespace EmlComplexity
theorem attains_e_sub_two : Attains (Real.exp 1 - 2) 7 := 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

e−2e-2e−2 has EML complexity at most 7

$e-2$ has EML complexity at most 7