Paper

Proves that the single operator eml(x, y) = exp(x) − ln(y) generates every elementary function as a finite binary tree, with explicit constructions for all standard functions. Introduces the EML depth hierarchy: five strata from arithmetic (depth 0) through oscillatory (depth 3), with a gap — there is no depth 4.

Studies the EML operator eml(x,y) = exp(x) − ln(y) and the smallest set EML₁ containing 1 and closed under eml. Central question: whether i ∈ EML₁. Proves depth-5 values have Im(z) ≤ 0, and that depth-6 values can reach Im ≈ 0.99999524 (gap 4.76×10⁻⁶). The obstruction: exact Im = 1 requires Re(y) = π/tan(1), which is transcendental (Hermite–Lindemann).

50 original EML theorems verified in Lean 4 across 14 files (478 total Lean statements). Zero sorries in 13 of 14 files; the 14th file (InfiniteZerosBarrier.lean) carries 2 documented sorries on Part D pending o-minimal theory. Covers the SuperBEST routing table lower bounds — SB(add) ≥ 2, SB(sub) ≥ 2, SB(mul) ≥ 2, SB(div) ≥ 2, and extended division — plus upper-bound 1-node constructions and the depth-1 analyticity substrate. Checked by Lean 4 and Mathlib.