Boundary Map

Four walls constrain what a finite EML expression can be. All four are leaky — an iterative algorithm stays inside ELC per step and converges across the wall. Walls constrain expressions, not computations.

Each wall, what it forbids, the cheapest ladder over it.

What it forbids

Functions with infinitely many isolated real zeros.

Canonical forbidden example

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

Theorem

T01 (Infinite-Zeros Barrier): a finite real EML tree is real-analytic on (0, ∞); non-zero analytic functions on a compact interval have finitely many zeros. sin has infinitely many. So sin ∉ EML(ℝ).

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-verified (partial). T01 substrate proved in Lean 4 (analyticity + compact-interval finite-zeros). Depth-k zero-count bound awaits o-minimal structure theory.

What it forbids

Roots of general polynomials of degree ≥ 5 as radical expressions.

Canonical forbidden example

roots of x⁵ − x − 1 = 0

Theorem

Abel-Ruffini (1824/1829): the Galois group of a generic degree-5 polynomial is S₅, which is not solvable. No expression in {+, −, ×, ÷, ⁿ√} evaluates to its roots.

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

classical proof. Standard Galois-theoretic proof. Not formalized in the monogate-lean suite.

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

Risch (1968): a decision procedure determines whether an elementary function has an elementary antiderivative. Most do not — the Gaussian integral is the canonical failure.

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

algorithmic. Risch's algorithm is implemented in Mathematica, Maple, SymPy. Fully decidable for a wide class.

What it forbids

Exact real-number constants that are transcendental over the algebraics.

Canonical forbidden example

π, e, e^π, sin(1), Γ(1/3)

Theorem

Lindemann-Weierstrass (1882/1885): if α₁, …, αₙ are algebraic and ℚ-linearly independent, then e^α₁, …, e^αₙ are algebraically independent. Corollary: π and e are transcendental.

Iterative bypass

AGM / BBP / Machin-like~21n for π to 64 bits via Gauss-Legendre AGM iteration

The AGM (arithmetic-geometric mean) doubles correct digits per iteration. Each AGM step is four arithmetic ops + one sqrt — all ELC-interior. The limit is 2π/(Gauss constant), outside ELC.

Formal status

classical proof. Standard transcendence theory. Not the kind of theorem that yields to formalization shortcuts.