$0$ has EML complexity at most 3

Proved

EmlComplexity.attains_zero

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

elementary-functionseml-complexityexpression-complexity

The constant $0$ is the value of a valid closed EML tree with three nodes: $\mathrm{eml}(1, \mathrm{eml}(\mathrm{eml}(1,1),1)) = e - \ln(e^{e}) = 0$ . Three is the least size at which a real closed tree evaluates to $0$ (that minimality is not part of this statement).

Preamble

import Definitions.Def_EmlComplexity

Formal statement

namespace EmlComplexity
theorem attains_zero : Attains ((0 : ℝ)) 3 := 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

000 has EML complexity at most 3

$0$ has EML complexity at most 3