A Compositional Exact-Search Calculus over a Single Binary Primitive: Bounded Enumeration, Macro Closure, and Stability Audits for EML Trees

A recent result by Odrzywołek shows that the binary operator E(a, b) = exp(a) − ln(b) , together with the constant 1, is enough to reconstruct the standard elementary-function basis of a scientific calculator. What has not been spelled out is the computational object this quietly invites: because every pure EML expression shares the same two-production grammar S → 1 | E(S, S) , the search space collapses into a single ranked tree language, not the usual ragged soup of heterogeneous operator types. We take that seriously. This paper defines a bounded exact-search calculus over pure EML trees and studies it end-to-end in a small, self-contained Python implementation — no neural network, no SAT solver, no symbolic regression framework. The calculus has four moving parts: bottom-up bounded enumeration, interval abstract semantics, sampled semantic deduplication, and macro closure by exact substitution. On unary benchmarks up to size 9, it exactly recovers 8 of 13 targets (including e, e^x, ln x, e^{e^x}, x^2, 1/x, x + 1); on bivariate benchmarks up to size 8, it exactly recovers 12 of 15 targets (including xy, x/y, y/x, ln x + ln y). Cumulative search-space compression is 95.96% for unary and 97.03% for bivariate enumeration. A collision audit finds zero false semantic merges up to unary size 6 and bivariate size 5 on held-out grids. Macro closure then derives exact expressions for e^{x + y}, x + y, x^2 + y, x^3, x^2 + 1, and e^x + 1 — targets that sit beyond the raw search horizon. A stability audit makes a point that, in our view, is often skipped in the symbolic-regression literature: symbolic exactness and floating-point executability are different things, and deep EML macros can be exact on paper and numerically miserable at runtime.