Prove2Me

Size-8 EML band, left size 33, right size 44 (mono block): no such tree evaluates to 22

Proved
EmlComplexity.not_attains_two_bundle_3_4_M

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

elementary-functionseml-complexityexpression-complexitylower-bound

Monotonicity-transport separations for 3 near-degenerate closed EML tree shapes with left subtree of size 33 and right subtree of size 44 (total size 88): each shape's real value is certified away from 22 by transporting a moderate Taylor bound across a huge range with exp/log monotonicity. One group of the size-88 lower-bound band for the EML complexity of 22.

Preamble
import Definitions.Def_EmlComplexity
Formal statement
namespace EmlComplexity
theorem not_attains_two_bundle_3_4_M : EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) EmlComplexity.Tree.one) (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one) (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one)) ≠ 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