Left size $3$ , right size $3$ : no such EML tree evaluates to $2$

Proved

EmlComplexity.not_attains_two_pair_3_3

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

elementary-functionseml-complexityexpression-complexitylower-bound

For closed EML trees $a$ of size $3$ and $b$ of size $3$ , if $\mathrm{node}(a,b)$ is valid then its real-branch value is not $2$ . Finite check over the shape pairs of this split, by certified enclosures with exact degenerate handling. One pair of the size- $7$ lower-bound band.

Preamble

import Definitions.Def_EmlComplexity

Formal statement

namespace EmlComplexity
theorem not_attains_two_pair_3_3 : ∀ a b : Tree, a.size = 3 → b.size = 3 → Tree.valid (Tree.node a b) → Tree.eval (Tree.node a b) ≠ 2 := 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

Left size 333, right size 333: no such EML tree evaluates to 222

Left size $3$ , right size $3$ : no such EML tree evaluates to $2$