No valid real EML tree of at most 2 nodes evaluates to $2$

Proved

EmlComplexity.not_attains_two_upto_two

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

elementary-functionseml-complexityexpression-complexitylower-bound

For every natural number $m \\le 2$ there is no valid closed EML tree with exactly $m$ nodes whose real-branch value is $2$ . This is a finite check over the $4$ trees of size at most $2$ : the single node evaluates to $e \\ne 2$ , and the two $2$ -node trees evaluate to $e - 1$ and $e^{e}$ , both separated from $2$ by certified exponential bounds. It is the base chunk of the full lower bound below $9$ nodes.

Preamble

import Definitions.Def_EmlComplexity

Formal statement

namespace EmlComplexity
theorem not_attains_two_upto_two : ∀ m : ℕ, m ≤ 2 → ¬ Attains (2 : ℝ) m := 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

No valid real EML tree of at most 2 nodes evaluates to 222

No valid real EML tree of at most 2 nodes evaluates to $2$