whitepaper: first machine-checked EML + 3-way i5-8350U benchmark

Two landings fox requested.

§8.6 EML verification section gains a "First machine-checked
treatment" paragraph. Sub-agent WebFetched arXiv:2603.21852v2 and
confirmed Odrzywołek's original paper is pure LaTeX prose with
no formal tool; the Zenodo companion is symbolic-regression code,
not a verification artifact. Our Lean 4 proof appears to be the
first machine-checked EML formalization — five theorems, zero
`sorry`, no Mathlib dependency, 40× faster than the brute-force
numerical search.

§6.4 "Three Implementations Head-to-Head" is new — benchmark
numbers from the actual i5-8350U hardware, collected via in-
process `current-time-ms` timing on each impl:

  sum-to(100k)      asm 74 ms  <  C 121 ms  <  Python-fast 583 ms
  sum-to(1M)        asm 734 ms <  C 1.2 s   <  Python-fast 5.4 s
  ackermann(3,8)    asm 2.4 s  <  Python-fast 18.5 s  (C segfaults)

asm beats every other impl on every measurable workload. The C
interpreter segfaults on ack(3,8) — its evaluator uses the host
C stack, and deep recursion exhausts it. asm and Python-fast use
explicit frame storage and handle deep recursion cleanly.

Also documents what I tried and backed off:
- asm env-lookup inline cache: upper bound ~5% win, not 20-40%,
  because asm chains are typically 2 deep. Parked.
- asm's real bottleneck is `env_define` allocating 24 bytes per
  parameter per call — 48 MB for sum-to(1M). Future optimization:
  per-frame batched allocation or self-tail-call env reuse.

Profiling done on the real hardware. No inline-cache code change
landed; the finding itself is the commit.

whitepaper/uncommonlisp-whitepaper.rst

@@ -385,6 +385,26 @@ The important comparison is not uncommonlisp vs CPython (different languages), b
 - **mergesort**: Recursive divide-and-conquer on 200 elements. Tests ``cons`` allocation throughput
 - **hash-table**: 1,000 ``set!`` + ``ref`` operations. Tests Python dict interop overhead
 
+6.4 Three Implementations Head-to-Head (i5-8350U)
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Same hardware, same workloads, in-process timing via ``current-time-ms``. Best of two runs.
+
+.. table::
+   :widths: 26 18 18 18
+
+   ======================== =========== =========== ===========
+   Benchmark                Python fast C           asm
+   ======================== =========== =========== ===========
+   sum-to(100 000)          583 ms      121 ms      **74 ms**
+   sum-to(1 000 000)        5,432 ms    1,200 ms    **734 ms**
+   fib(35) iterative        ~0 ms       ~0 ms       ~0 ms
+   ackermann(3, 8) = 2045   18,479 ms   (segfault)  **2,383 ms**
+   ======================== =========== =========== ===========
+
+asm wins every measurable workload on this hardware. The C interpreter segfaults on ackermann(3, 8) because its evaluator uses the host C stack for Scheme frames; ackermann recurses thousands of levels deep. asm and Python-fast both use explicit frame storage and handle the recursion cleanly. asm beats Python-fast by ~7× on ``sum-to(1M)`` and ~8× on ``ackermann(3, 8)`` despite asm being a tree-walker with no JIT — the constant-factor difference from eliminating Python's dict lookups, stack frames, and GC coordination is large.
+
+**asm's remaining bottleneck is allocation, not lookup.** Profiling ``sum-to(1M)`` shows ~170 MB RSS — each tail call through ``apply_closure`` + ``env_define`` allocates 24 bytes per parameter (sym / val / parent), twice per ``loop`` iteration, for 48 MB total before the three ``heap_grow`` events that follow. A future optimization candidate is per-frame batched allocation (``8 + 16N`` bytes once per call instead of ``24N``), or env-cell in-place reuse for self-tail-calls. An inline cache for env lookups (ported from Python's VM) turns out to help less than anticipated because asm's env chains are typically only 2 deep and each step is a pointer dereference; measured upper bound is ~5%.
 
 7. Portal: Feedback Across Time
 ----------------------------------------
@@ -652,6 +672,8 @@ The numerical approaches enumerate all pairwise EML compositions at each depth,
 
 The Lean proof operates over abstract ``exp`` & ``ln`` functions with the axioms ``exp(ln(x)) = x``, ``ln(exp(x)) = x``, & ``ln(1) = 0``. This makes the result independent of any particular real number implementation.
 
+**First machine-checked treatment.** The original paper (Odrzywołek, arXiv:2603.21852v2, 2026-04-04) presents the EML universality claim analytically — pure LaTeX mathematics, no formal tool. The companion Zenodo artifact is symbolic-regression / gradient-optimization code, not a verification. To our knowledge the Lean 4 proof shipped in this repo is the first machine-checked treatment of the EML identities. Five theorems, zero ``sorry``, no Mathlib dependency — 40× faster than the brute-force numerical search it replaced, and carrying the additional guarantee that no implementation quirk of floating point can ever break the conclusion.
+
 
 9. Language Coverage
 ---------------------