Size-8 EML band, left size $3$ , right size $4$ (first block): no such tree evaluates to $2$

Proved

EmlComplexity.not_attains_two_bundle_3_4_A

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

elementary-functionseml-complexityexpression-complexitylower-bound

Finite check over the first block of 34 closed EML tree shapes with left subtree of size $3$ and right subtree of size $4$ (total size $8$ ): no valid instance evaluates to $2$ . Of the 34 shapes, 28 separate from $2$ by certified real enclosures and 6 are invalid (certified one-sided bounds or exact degeneracy). One group of the size- $8$ lower-bound band for the EML complexity of $2$ .

Preamble

import Definitions.Def_EmlComplexity

Formal statement

namespace EmlComplexity
theorem not_attains_two_bundle_3_4_A : EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))))) ≠ 2 ∧ ¬ EmlComplexity.Tree.valid (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)))) ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)))) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) EmlComplexity.Tree.one))) ≠ 2 ∧ ¬ EmlComplexity.Tree.valid (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one))) ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)))) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one))) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (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.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) (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.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node 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.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))))) ≠ 2 ∧ ¬ EmlComplexity.Tree.valid (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)))) ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)))) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) EmlComplexity.Tree.one))) ≠ 2 ∧ ¬ EmlComplexity.Tree.valid (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one))) ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)))) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one))) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))) EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) EmlComplexity.Tree.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (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.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)) (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.one)) ≠ 2 ∧ EmlComplexity.Tree.eval (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (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.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one))))) ≠ 2 ∧ ¬ EmlComplexity.Tree.valid (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.one (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one)))) ∧ 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.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)))) ≠ 2 ∧ 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.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one)) EmlComplexity.Tree.one))) ≠ 2 ∧ ¬ EmlComplexity.Tree.valid (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.one (EmlComplexity.Tree.node (EmlComplexity.Tree.node (EmlComplexity.Tree.node EmlComplexity.Tree.one EmlComplexity.Tree.one) EmlComplexity.Tree.one) EmlComplexity.Tree.one))) ∧ 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.one EmlComplexity.Tree.one) (EmlComplexity.Tree.node EmlComplexity.Tree.one (EmlComplexity.Tree.node 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

Size-8 EML band, left size 333, right size 444 (first block): no such tree evaluates to 222

Size-8 EML band, left size $3$ , right size $4$ (first block): no such tree evaluates to $2$