Prove2Me

No valid real EML tree of fewer than 21 nodes evaluates to 44

Open
EmlComplexity.not_attains_four_below_twenty_one

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

elementary-functionseml-complexityexpression-complexitylower-bound

For every natural number m<21m < 21 there is no valid closed EML tree with exactly mm nodes whose real-branch value is 44. Exhaustive numerical enumeration of the real branch to size 20 (327,841,920 distinct values, 11-digit observational dedupe, non-finite intermediates rejected) found none; a proof must handle every tree of size at most 20 exactly, including the ones the enumeration discarded as degenerate.

Preamble
import Definitions.Def_EmlComplexity
Formal statement
namespace EmlComplexity
theorem not_attains_four_below_twenty_one : ∀ m : ℕ, m < 21 → ¬ Attains (4 : ℝ) 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