Boundary Map

Four classical impossibility theorems, and what each one means for a finite EML expression. One is a machine-checked EML barrier; one is machine-checked for radicals and open for EML; one is a classical theorem that applies to EML; one walls in algebraic formulas — and EML steps over it in one node. Walls constrain expressions, not computations: an iterative algorithm stays inside per step and converges across.

Each wall, what it forbids, whether it binds EML, and the cheapest ladder over it.

What it forbids

Functions that never settle into one sign as x grows.

Canonical forbidden example

sin(x), cos(x), Bessel J₀(x)

Theorem

Periodic barrier (Lean, MachLib): every real EML tree defined for large x eventually keeps one sign; sin never does. So sin ∉ EML(ℝ). Counting zeros alone would not show it — sin, like every tree that is not identically zero, has finitely many zeros on any compact interval.

Iterative bypass

Chebyshev / CORDIC60–250n for 64-bit precision per evaluation

Approximate sin(x) as a polynomial of Chebyshev polynomials or iterate CORDIC rotations. Each step stays inside ELC; the fixed-point converges outside the barrier.

Formal status

Machine-checked EML barrier Lean, MachLib: no_tree_eq_sin_via_periodic_barrier — no real EML tree equals sin on ℝ, at any EML depth. ledger entry →

What it forbids

A root of x⁵ − 4x + 2 as a radical expression in the rationals.

Canonical forbidden example

a root of x⁵ − 4x + 2 = 0

Theorem

Abel–Ruffini (Ruffini 1799, Abel 1824): x⁵ − 4x + 2 has Galois group S₅, which is not solvable, so no expression built from rationals with +, −, ×, ÷ and n-th roots reaches its roots. EML also has exp and log, and whether they reach such a root is open: Chow (1999) shows they do not if Schanuel's conjecture holds.

Iterative bypass

Newton's method~240n per quintic root (64-bit precision)

Iterate xₙ₊₁ = xₙ − f(xₙ)/f'(xₙ). Each step is ELC-interior; the fixed point is the root. Quadratic convergence: ~53 iterations from a reasonable seed.

Formal status

Machine-checked for radicals; open for EML Lean, Mathlib's proof (AbelRuffini.exists_not_solvable_by_rad). For exp and log the wall is conditional on Schanuel's conjecture. ledger entry →

What it forbids

Antiderivatives that cannot be written in closed form using elementary functions.

Canonical forbidden example

∫ e^(−x²) dx, ∫ sin(x)/x dx, ∫ 1/ln(x) dx

Theorem

Liouville (1830s) and Risch (1968): ∫ e^(−x²) dx has no elementary antiderivative, and Risch's algorithm decides the question for elementary integrands. Every EML tree is an elementary function, so no tree is that antiderivative.

Iterative bypass

Gauss-Legendre quadrature50–200n per definite integral to 64-bit precision

Evaluate the integrand at optimized nodes and take a weighted sum. Each evaluation is ELC-interior; the sum converges to the definite integral whether or not its antiderivative has closed form.

Formal status

Classical theorem — applies to EML, not machine-checked Liouville's theorem on elementary integrals is not in Mathlib; formalizing it would be a research project. Risch's algorithm is implemented in Mathematica, Maple and SymPy.

What it forbids

Algebraic formulas — roots of polynomials with rational coefficients — that equal π or e.

Canonical forbidden example

π, e, e^π as algebraic numbers

Theorem

Lindemann-Weierstrass (1882/1885): if α₁, …, αₙ are algebraic and ℚ-linearly independent, then e^α₁, …, e^αₙ are algebraically independent. So π and e are transcendental: no algebraic formula reaches them. EML is not an algebraic formula — exp is built in: e = eml(1, 1) is one node, and over ℂ, π enters through Log(−1) = iπ.

Iterative bypass

None needed for EML1 node for e = eml(1, 1)

eml(1, 1) = exp(1) − ln 1 = e. Algebraic formulas need iteration to approach π or e (the AGM doubles π's correct digits per step); EML writes e in one node.

Formal status

Not a wall for EML True and classical (Mathlib has only its analytic half). It bounds algebraic formulas, not ones with exp and log.