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. (An earlier version of this card also said there is no depth 4. There is: x + 1 needs EML tree depth exactly 4 on (0, ∞).)

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₁. It shows that depth-5 values have Im(z) ≤ 0 and that a depth-6 value comes within 4.76×10⁻⁶ of i. Its "transcendental obstruction" (exact Im = 1 needs Re(y) = π/tan(1)) is not a proof, and a depth-7 tree gets its imaginary part within 7.9×10⁻¹² of 1; the blog post below is corrected.

EML theorems formalized in Lean 4: 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. InfiniteZerosBarrier.lean carries 2 documented sorries on Part D, pending o-minimal theory. Per-file statement and sorry counts, and the full source of each flagship theorem, are on /proofs; both are checked against a pinned monogate-lean commit before every deploy.