lumbda/proof/benchmark_results.md

EML Proof Friction Benchmark

Three approaches to verifying the same claim: eml(x,y) = exp(x) - ln(y) with constant 1 generates all elementary functions (arXiv:2603.21852v2).

Results

Approach	Time	Guarantee	Friction
Python (numerical)	0.04s	1e-10 tolerance	Low
uncommonlisp (numerical)	59s	1e-10 tolerance	High
Lean 4 (formal proof)	1.5s	kernel-verified	Medium

Analysis

The formal proof is 40x faster than brute-force search and provides mathematical certainty instead of floating-point tolerance.

The numerical approaches (Python and uncommonlisp) perform O(N²) pairwise enumeration of EML trees, evaluating at transcendental test points and comparing against target functions. This is MOAD-0001 at the proof layer: quadratic search friction where algebraic reasoning suffices.

The Lean proof does 5 rewrites — each one an identity (exp(ln(x))=x, ln(exp(x))=x, ln(1)=0). The kernel checks each step in microseconds. No search, no tolerance, no conjecture dependency.

The MOAD-0001 in proof methodology

Step	Numerical approach	Algebraic approach
Find exp	O(N²) search	1 rewrite: eml(x,1) = exp(x) - ln(1) = exp(x)
Find ln	O(N²) search	3 rewrites: composition + cancel
Find 0	O(N²) search	Corollary of ln: ln(1) = 0
Find sub	O(N²) search	1 rewrite: eml(ln(a), exp(b)) = a - b
Verify	Compare floats	Type checker

The numerical search does redundant work at every step. The algebraic proof does each step exactly once. This is the sedimentary defect: brute-force where structure exists.

Lesson

The fastest path to truth is not computation — it is understanding. When you know WHY eml(1, eml(eml(1,x), 1)) = ln(x), you can verify it in microseconds. When you don't, you search for hours.

Proof assistants eliminate the quadratic friction of verification. They are the hash set to numerical analysis's nested loop.