From b81c8923c06191f541cbb6d167e4b7af68e91e49 Mon Sep 17 00:00:00 2001 From: "russell@unturf.com" Date: Tue, 14 Apr 2026 13:34:28 -0400 Subject: [PATCH] Add friction benchmark to whitepaper: MOAD-0001 at the proof layer MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Formal proof (Lean, 1.5s) is 40x faster than brute-force search (uncommonlisp, 59s) with mathematical certainty vs floating-point tolerance. This is O(N²) search friction where O(1) algebraic reasoning suffices — the sedimentary defect in proof methodology. Proof assistants are the hash set to numerical analysis's nested loop. --- whitepaper/uncommonlisp-whitepaper.pdf | 508 ++++++++++++++++--------- whitepaper/uncommonlisp-whitepaper.rst | 23 +- 2 files changed, 348 insertions(+), 183 deletions(-) diff --git a/whitepaper/uncommonlisp-whitepaper.pdf b/whitepaper/uncommonlisp-whitepaper.pdf index 57d2cb9..a5e4d3b 100644 --- a/whitepaper/uncommonlisp-whitepaper.pdf +++ b/whitepaper/uncommonlisp-whitepaper.pdf @@ -152,9 +152,7 @@ endobj 20 0 obj << /Contents 72 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 62 0 R /Resources << -/Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] /XObject << -/FormXob.d3ecd28ca03f587d6940049748681018 3 0 R ->> +/Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << >> @@ -181,7 +179,7 @@ endobj << /Contents 73 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 62 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] /XObject << -/FormXob.fc331aff86ff817ecac4c4ce4b2ecd3a 21 0 R +/FormXob.d3ecd28ca03f587d6940049748681018 3 0 R /FormXob.fc331aff86ff817ecac4c4ce4b2ecd3a 21 0 R >> >> /Rotate 0 /Trans << @@ -196,7 +194,7 @@ endobj endobj 25 0 obj << -/Author () /CreationDate (D:20260414133201-04'00') /Creator (\(unspecified\)) /Keywords () /ModDate (D:20260414133201-04'00') /Producer (ReportLab PDF Library - \(opensource\)) +/Author () /CreationDate (D:20260414133413-04'00') /Creator (\(unspecified\)) /Keywords () /ModDate (D:20260414133413-04'00') /Producer (ReportLab PDF Library - \(opensource\)) /Subject (\(unspecified\)) /Title () /Trapped /False >> endobj @@ -358,32 +356,32 @@ endobj endobj 56 0 obj << -/Dest [ 19 0 R /XYZ 57.02362 669.0236 0 ] /Parent 50 0 R /Prev 55 0 R /Title (8.6 Verification) +/Dest [ 19 0 R /XYZ 57.02362 669.0236 0 ] /Parent 50 0 R /Prev 55 0 R /Title (8.6 Verification & Friction Analysis) >> endobj 57 0 obj << -/Dest [ 19 0 R /XYZ 57.02362 393.8236 0 ] /Next 58 0 R /Parent 27 0 R /Prev 50 0 R /Title (9. Language Coverage) +/Dest [ 19 0 R /XYZ 57.02362 165.8236 0 ] /Next 58 0 R /Parent 27 0 R /Prev 50 0 R /Title (9. Language Coverage) >> endobj 58 0 obj << -/Dest [ 19 0 R /XYZ 57.02362 156.6236 0 ] /Next 59 0 R /Parent 27 0 R /Prev 57 0 R /Title (10. Relationship to Companion Papers) +/Dest [ 20 0 R /XYZ 57.02362 621.0236 0 ] /Next 59 0 R /Parent 27 0 R /Prev 57 0 R /Title (10. Relationship to Companion Papers) >> endobj 59 0 obj << -/Dest [ 20 0 R /XYZ 57.02362 603.0236 0 ] /Next 60 0 R /Parent 27 0 R /Prev 58 0 R /Title (11. Future Work) +/Dest [ 20 0 R /XYZ 57.02362 371.8236 0 ] /Next 60 0 R /Parent 27 0 R /Prev 58 0 R /Title (11. Future Work) >> endobj 60 0 obj << -/Dest [ 20 0 R /XYZ 57.02362 437.8236 0 ] /Next 61 0 R /Parent 27 0 R /Prev 59 0 R /Title (Citation) +/Dest [ 20 0 R /XYZ 57.02362 206.6236 0 ] /Next 61 0 R /Parent 27 0 R /Prev 59 0 R /Title (Citation) >> endobj 61 0 obj << -/Dest [ 20 0 R /XYZ 57.02362 356.6236 0 ] /Parent 27 0 R /Prev 60 0 R /Title (License) +/Dest [ 20 0 R /XYZ 57.02362 125.4236 0 ] /Parent 27 0 R /Prev 60 0 R /Title (License) >> endobj 62 0 obj @@ -3257,7 +3255,7 @@ endstream endobj 71 0 obj << -/Length 9140 +/Length 10228 >> stream 1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET @@ -3297,24 +3295,192 @@ Q q 1 0 0 1 57.02362 657.0236 cm q -BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (8.6 Verification) Tj T* ET +BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (8.6 Verification & Friction Analysis) Tj T* ET Q Q q 1 0 0 1 57.02362 639.0236 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (The proof is verified at three levels:) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (The proof is verified at three levels, with dramatically different friction:) Tj T* ET Q Q q 1 0 0 1 57.02362 633.0236 cm Q q -1 0 0 1 57.02362 633.0236 cm +1 0 0 1 57.02362 561.0236 cm +q +1 1 1 rg +n 0 72 481.2283 -18 re f* +.878431 .878431 .878431 rg +n 0 54 481.2283 -18 re f* +1 1 1 rg +n 0 36 481.2283 -18 re f* +.878431 .878431 .878431 rg +n 0 18 481.2283 -18 re f* +0 0 0 rg +BT /F3 10 Tf 12 TL ET +q +1 0 0 1 6 57 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 42.84925 0 Td (Approach) Tj T* -42.84925 0 Td ET +Q Q q -1 0 0 1 57.02362 597.0236 cm +1 0 0 1 150.3685 57 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 11.2037 0 Td (Time) Tj T* -11.2037 0 Td ET +Q +Q +q +1 0 0 1 208.1159 57 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 29.42354 0 Td (Guarantee) Tj T* -29.42354 0 Td ET +Q +Q +q +1 0 0 1 328.423 57 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 55.06768 0 Td (Friction) Tj T* -55.06768 0 Td ET +Q +Q +0 0 0 rg +BT /F1 10 Tf 12 TL ET +q +1 0 0 1 6 39 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Python \(numerical\)) Tj T* ET +Q +Q +q +1 0 0 1 150.3685 39 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (0.04s) Tj T* ET +Q +Q +q +1 0 0 1 208.1159 39 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (1e-10 tolerance) Tj T* ET +Q +Q +q +1 0 0 1 328.423 39 cm +q +BT 1 0 0 1 0 2 Tm 12 TL /F1 10 Tf 0 0 0 rg (Low: evaluate & compare) Tj T* ET +Q +Q +q +1 0 0 1 6 21 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (uncommonlisp \(numerical\)) Tj T* ET +Q +Q +q +1 0 0 1 150.3685 21 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (59s) Tj T* ET +Q +Q +q +1 0 0 1 208.1159 21 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (1e-10 tolerance) Tj T* ET +Q +Q +q +1 0 0 1 328.423 21 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (High: O\(N\262\) brute-force search) Tj T* ET +Q +Q +q +1 0 0 1 6 3 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Lean 4 \(formal proof\)) Tj T* ET +Q +Q +q +1 0 0 1 150.3685 3 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (1.5s) Tj T* ET +Q +Q +q +1 0 0 1 208.1159 3 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (kernel-verified certainty) Tj T* ET +Q +Q +q +1 0 0 1 328.423 3 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Medium: 5 rewrites, type-check) Tj T* ET +Q +Q +q +1 J +1 j +0 0 0 RG +.25 w +n 0 54 m 481.2283 54 l S +n 0 36 m 481.2283 36 l S +n 0 18 m 481.2283 18 l S +n 144.3685 0 m 144.3685 72 l S +n 202.1159 0 m 202.1159 72 l S +n 322.423 0 m 322.423 72 l S +n 0 72 m 481.2283 72 l S +n 0 0 m 481.2283 0 l S +n 0 0 m 0 72 l S +n 481.2283 0 m 481.2283 72 l S +Q +Q +Q +q +1 0 0 1 57.02362 561.0236 cm +Q +q +1 0 0 1 57.02362 519.0236 cm +q +BT 1 0 0 1 0 26 Tm .395596 Tw 12 TL /F3 10 Tf 0 0 0 rg (The formal proof is 40x faster than the brute-force search & provides mathematical certainty instead) Tj T* 0 Tw 1.066027 Tw (of floating-point tolerance.) Tj /F1 10 Tf ( This is MOAD-0001 \(the sedimentary defect\) at the proof methodology layer:) Tj T* 0 Tw (O\(N\262\) search friction where O\(1\) algebraic reasoning suffices.) Tj T* ET +Q +Q +q +1 0 0 1 57.02362 465.0236 cm +q +BT 1 0 0 1 0 38 Tm 2.309862 Tw 12 TL /F1 10 Tf 0 0 0 rg (The numerical approaches enumerate all pairwise EML compositions at each depth, comparing results) Tj T* 0 Tw .653022 Tw (against target functions. This grows quadratically with the number of known values. The Lean proof does 5) Tj T* 0 Tw .327397 Tw (algebraic rewrites, each applying an axiom \() Tj /F5 10 Tf (exp\(ln\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (x) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (ln\(exp\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (x) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (ln\(1\)) Tj ( ) Tj (=) Tj ( ) Tj (0) Tj /F1 10 Tf (\). The type) Tj T* 0 Tw (checker confirms each rewrite in microseconds. No search. No tolerance. No conjecture dependency.) Tj T* ET +Q +Q +q +1 0 0 1 57.02362 411.0236 cm +q +BT 1 0 0 1 0 38 Tm 3.571147 Tw 12 TL /F3 10 Tf 0 0 0 rg (Lesson) Tj /F1 10 Tf (: The fastest path to truth is not computation \227 it is understanding. When you know ) Tj /F4 10 Tf (why) Tj /F1 10 Tf T* 0 Tw .96189 Tw /F5 10 Tf (eml\(1,) Tj ( ) Tj (eml\(eml\(1,x\),) Tj ( ) Tj (1\)\)) Tj ( ) Tj (=) Tj ( ) Tj (ln\(x\)) Tj /F1 10 Tf (, you verify it in microseconds. When you don't, you search for) Tj T* 0 Tw 1.513223 Tw (hours. Proof assistants eliminate the quadratic friction of verification. They are the hash set to numerical) Tj T* 0 Tw (analysis's nested loop.) Tj T* ET +Q +Q +q +1 0 0 1 57.02362 405.0236 cm +Q +q +1 0 0 1 57.02362 405.0236 cm +Q +q +1 0 0 1 57.02362 369.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -3336,10 +3502,10 @@ Q Q Q q -1 0 0 1 57.02362 591.0236 cm +1 0 0 1 57.02362 363.0236 cm Q q -1 0 0 1 57.02362 555.0236 cm +1 0 0 1 57.02362 327.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -3361,10 +3527,10 @@ Q Q Q q -1 0 0 1 57.02362 549.0236 cm +1 0 0 1 57.02362 321.0236 cm Q q -1 0 0 1 57.02362 525.0236 cm +1 0 0 1 57.02362 297.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -3386,10 +3552,10 @@ Q Q Q q -1 0 0 1 57.02362 525.0236 cm +1 0 0 1 57.02362 297.0236 cm Q q -1 0 0 1 57.02362 455.8236 cm +1 0 0 1 57.02362 227.8236 cm q q 1 0 0 1 0 0 cm @@ -3410,95 +3576,110 @@ Q Q Q q -1 0 0 1 57.02362 411.8236 cm +1 0 0 1 57.02362 183.8236 cm q BT 1 0 0 1 0 26 Tm 4.138556 Tw 12 TL /F1 10 Tf 0 0 0 rg (The Lean proof operates over abstract ) Tj /F5 10 Tf (exp) Tj /F1 10 Tf ( & ) Tj /F5 10 Tf (ln) Tj /F1 10 Tf ( functions with the axioms ) Tj /F5 10 Tf (exp\(ln\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (x) Tj /F1 10 Tf (,) Tj T* 0 Tw 2.484897 Tw /F5 10 Tf (ln\(exp\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (x) Tj /F1 10 Tf (, & ) Tj /F5 10 Tf (ln\(1\)) Tj ( ) Tj (=) Tj ( ) Tj (0) Tj /F1 10 Tf (. This makes the result independent of any particular real number) Tj T* 0 Tw (implementation.) Tj T* ET Q Q q -1 0 0 1 57.02362 380.6236 cm +1 0 0 1 57.02362 152.6236 cm q BT 1 0 0 1 0 2.2 Tm 13.2 TL /F2 11 Tf .133333 .133333 .133333 rg (9. Language Coverage) Tj T* ET Q Q q -1 0 0 1 57.02362 360.6236 cm +1 0 0 1 57.02362 132.6236 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (uncommonlisp implements a near-complete R7RS-small Scheme:) Tj T* ET Q Q q -1 0 0 1 57.02362 306.6236 cm +1 0 0 1 57.02362 78.62362 cm q BT 1 0 0 1 0 38 Tm 1.369223 Tw 12 TL /F3 10 Tf 0 0 0 rg (Special forms) Tj /F1 10 Tf ( \(32\): ) Tj /F5 10 Tf (define) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (set!) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (lambda) Tj /F1 10 Tf (, ) Tj /F5 10 Tf /F6 10 Tf 12 TL (l) Tj /F5 10 Tf 12 TL /F1 10 Tf (, ) Tj /F5 10 Tf (if) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (cond) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (case) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (and) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (or) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (when) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (unless) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (begin) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (let) Tj /F1 10 Tf (,) Tj T* 0 Tw 10.15262 Tw /F5 10 Tf (let*) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (letrec) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (letrec*) Tj /F1 10 Tf (, named-let, ) Tj /F5 10 Tf (do) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (quasiquote) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (define-macro) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (define-syntax) Tj /F1 10 Tf (,) Tj T* 0 Tw 3.646907 Tw /F5 10 Tf (syntax-rules) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (let-syntax) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (letrec-syntax) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (apply) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (eval) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (values) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (call/cc) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (dynamic-wind) Tj /F1 10 Tf (,) Tj T* 0 Tw /F5 10 Tf (guard) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (parameterize) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (load) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (error) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (module) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (import) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (define-record-type) Tj /F1 10 Tf (.) Tj T* ET Q Q + +endstream +endobj +72 0 obj +<< +/Length 7723 +>> +stream +1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 276.6236 cm +1 0 0 1 57.02362 741.0236 cm q BT 1 0 0 1 0 14 Tm .150642 Tw 12 TL /F3 10 Tf 0 0 0 rg (Built-in functions) Tj /F1 10 Tf ( \(100+\): Full arithmetic \(exact rationals, inexact reals, trigonometry\), pairs & lists \(SRFI-1\),) Tj T* 0 Tw (strings \(mutable\), characters, vectors, hash tables, I/O \(ports, file system\), system interface, Python interop.) Tj T* ET Q Q q -1 0 0 1 57.02362 246.6236 cm +1 0 0 1 57.02362 711.0236 cm q BT 1 0 0 1 0 14 Tm 2.274835 Tw 12 TL /F3 10 Tf 0 0 0 rg (Hygienic macros) Tj /F1 10 Tf (: ) Tj /F5 10 Tf (syntax-rules) Tj /F1 10 Tf ( with ellipsis \() Tj /F5 10 Tf (...) Tj /F1 10 Tf (\) support. Pattern matching, template instantiation,) Tj T* 0 Tw (proper hygiene. Also ) Tj /F5 10 Tf (define-macro) Tj /F1 10 Tf ( for procedural macros.) Tj T* ET Q Q q -1 0 0 1 57.02362 216.6236 cm +1 0 0 1 57.02362 681.0236 cm q BT 1 0 0 1 0 14 Tm 1.958835 Tw 12 TL /F3 10 Tf 0 0 0 rg (Standard library) Tj /F1 10 Tf ( \() Tj /F5 10 Tf (stdlib.lsp) Tj /F1 10 Tf (, 385 lines\): Additional macros \() Tj /F5 10 Tf (swap!) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (fluid-let) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (while) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (dotimes) Tj /F1 10 Tf (\),) Tj T* 0 Tw (utility functions, simple object system, SRFI-2/8/64 test framework.) Tj T* ET Q Q q -1 0 0 1 57.02362 174.6236 cm +1 0 0 1 57.02362 639.0236 cm q BT 1 0 0 1 0 26 Tm 2.004488 Tw 12 TL /F3 10 Tf 0 0 0 rg (Test suite) Tj /F1 10 Tf (: 529 tests covering lexing, parsing, special forms, bytecode compilation, macros \(hygienic &) Tj T* 0 Tw 3.388705 Tw (procedural\), continuations, generators, record types, modules, arithmetic, higher-order functions, error) Tj T* 0 Tw (handling, & portal serialization.) Tj T* ET Q Q q -1 0 0 1 57.02362 143.4236 cm +1 0 0 1 57.02362 607.8236 cm q BT 1 0 0 1 0 2.2 Tm 13.2 TL /F2 11 Tf .133333 .133333 .133333 rg (10. Relationship to Companion Papers) Tj T* ET Q Q q -1 0 0 1 57.02362 123.4236 cm +1 0 0 1 57.02362 587.8236 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (uncommonlisp forms one piece of a larger permacomputer machine learning stack:) Tj T* ET Q Q q -1 0 0 1 57.02362 117.4236 cm +1 0 0 1 57.02362 581.8236 cm Q q -1 0 0 1 57.02362 69.42362 cm +1 0 0 1 57.02362 443.8236 cm q 1 1 1 rg -n 0 48 481.2283 -18 re f* +n 0 138 481.2283 -18 re f* .878431 .878431 .878431 rg +n 0 120 481.2283 -30 re f* +1 1 1 rg +n 0 90 481.2283 -30 re f* +.878431 .878431 .878431 rg +n 0 60 481.2283 -30 re f* +1 1 1 rg n 0 30 481.2283 -30 re f* 0 0 0 rg BT /F3 10 Tf 12 TL ET q -1 0 0 1 6 33 cm +1 0 0 1 6 123 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 28.78283 0 Td (Layer) Tj T* -28.78283 0 Td ET Q Q q -1 0 0 1 102.2457 33 cm +1 0 0 1 102.2457 123 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 64.31996 0 Td (Paper) Tj T* -64.31996 0 Td ET Q Q q -1 0 0 1 270.6756 33 cm +1 0 0 1 270.6756 123 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 91.44138 0 Td (Role) Tj T* -91.44138 0 Td ET @@ -3507,60 +3688,25 @@ Q 0 0 0 rg BT /F1 10 Tf 12 TL ET q -1 0 0 1 6 15 cm +1 0 0 1 6 105 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Runtime) Tj T* ET Q Q q -1 0 0 1 102.2457 3 cm +1 0 0 1 102.2457 93 cm q BT 1 0 0 1 0 14 Tm 12 TL /F3 10 Tf 0 0 0 rg (Feedback Is All You Need) Tj /F1 10 Tf ( \(this) Tj T* (paper\)) Tj T* ET Q Q q -1 0 0 1 270.6756 3 cm +1 0 0 1 270.6756 93 cm q BT 1 0 0 1 0 14 Tm 12 TL /F1 10 Tf 0 0 0 rg (Complete Scheme VM with continuations &) Tj T* (portal) Tj T* ET Q Q q -1 J -1 j -0 0 0 RG -.25 w -n 0 0 m 481.2283 0 l S -n 0 30 m 481.2283 30 l S -n 96.24567 0 m 96.24567 48 l S -n 264.6756 0 m 264.6756 48 l S -n 0 48 m 481.2283 48 l S -n 0 0 m 0 48 l S -n 481.2283 0 m 481.2283 48 l S -Q -Q -Q - -endstream -endobj -72 0 obj -<< -/Length 5076 ->> -stream -1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET -q -1 0 0 1 57.02362 675.0236 cm -q -1 1 1 rg -n 0 90 481.2283 -30 re f* -.878431 .878431 .878431 rg -n 0 60 481.2283 -30 re f* -1 1 1 rg -n 0 30 481.2283 -30 re f* -0 0 0 rg -BT /F1 10 Tf 12 TL ET -q 1 0 0 1 6 75 cm q 0 0 0 rg @@ -3627,40 +3773,42 @@ q 1 j 0 0 0 RG .25 w +n 0 120 m 481.2283 120 l S n 0 90 m 481.2283 90 l S n 0 60 m 481.2283 60 l S n 0 30 m 481.2283 30 l S -n 96.24567 0 m 96.24567 90 l S -n 264.6756 0 m 264.6756 90 l S -n 0 0 m 0 90 l S -n 481.2283 0 m 481.2283 90 l S +n 96.24567 0 m 96.24567 138 l S +n 264.6756 0 m 264.6756 138 l S +n 0 138 m 481.2283 138 l S n 0 0 m 481.2283 0 l S +n 0 0 m 0 138 l S +n 481.2283 0 m 481.2283 138 l S Q Q Q q -1 0 0 1 57.02362 675.0236 cm +1 0 0 1 57.02362 443.8236 cm Q q -1 0 0 1 57.02362 621.0236 cm +1 0 0 1 57.02362 389.8236 cm q BT 1 0 0 1 0 38 Tm 2.814488 Tw 12 TL /F1 10 Tf 0 0 0 rg (uncommonlisp provides the runtime layer: a language that can checkpoint its own execution, migrate) Tj T* 0 Tw 2.355696 Tw (between machines, & resume from serialized state. The portal system enables distributed computation) Tj T* 0 Tw 1.588941 Tw (across permacomputer nodes. Categorization & feedback activities could run inside uncommonlisp's VM,) Tj T* 0 Tw (with ) Tj /F5 10 Tf (call/cc) Tj /F1 10 Tf ( providing the state machine transitions & portal providing persistence.) Tj T* ET Q Q q -1 0 0 1 57.02362 589.8236 cm +1 0 0 1 57.02362 358.6236 cm q BT 1 0 0 1 0 2.2 Tm 13.2 TL /F2 11 Tf .133333 .133333 .133333 rg (11. Future Work) Tj T* ET Q Q q -1 0 0 1 57.02362 575.8236 cm +1 0 0 1 57.02362 344.6236 cm Q q -1 0 0 1 57.02362 575.8236 cm +1 0 0 1 57.02362 344.6236 cm Q q -1 0 0 1 57.02362 551.8236 cm +1 0 0 1 57.02362 320.6236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -3682,10 +3830,10 @@ Q Q Q q -1 0 0 1 57.02362 545.8236 cm +1 0 0 1 57.02362 314.6236 cm Q q -1 0 0 1 57.02362 521.8236 cm +1 0 0 1 57.02362 290.6236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -3707,10 +3855,10 @@ Q Q Q q -1 0 0 1 57.02362 515.8236 cm +1 0 0 1 57.02362 284.6236 cm Q q -1 0 0 1 57.02362 503.8236 cm +1 0 0 1 57.02362 272.6236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -3732,10 +3880,10 @@ Q Q Q q -1 0 0 1 57.02362 497.8236 cm +1 0 0 1 57.02362 266.6236 cm Q q -1 0 0 1 57.02362 473.8236 cm +1 0 0 1 57.02362 242.6236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -3757,16 +3905,16 @@ Q Q Q q -1 0 0 1 57.02362 455.8236 cm +1 0 0 1 57.02362 224.6236 cm Q q -1 0 0 1 57.02362 424.6236 cm +1 0 0 1 57.02362 193.4236 cm q BT 1 0 0 1 0 2.2 Tm 13.2 TL /F2 11 Tf .133333 .133333 .133333 rg (Citation) Tj T* ET Q Q q -1 0 0 1 57.02362 374.6236 cm +1 0 0 1 57.02362 143.4236 cm q q 1 0 0 1 0 0 cm @@ -3787,16 +3935,25 @@ Q Q Q q -1 0 0 1 57.02362 343.4236 cm +1 0 0 1 57.02362 112.2236 cm q BT 1 0 0 1 0 2.2 Tm 13.2 TL /F2 11 Tf .133333 .133333 .133333 rg (License) Tj T* ET Q Q q -1 0 0 1 57.02362 327.4236 cm +1 0 0 1 57.02362 96.22362 cm Q + +endstream +endobj +73 0 obj +<< +/Length 894 +>> +stream +1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 124.3477 cm +1 0 0 1 57.02362 561.9477 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -3812,22 +3969,13 @@ Q Q Q q -1 0 0 1 57.02362 116.3477 cm +1 0 0 1 57.02362 553.9477 cm Q q -1 0 0 1 57.02362 108.3477 cm +1 0 0 1 57.02362 545.9477 cm Q - -endstream -endobj -73 0 obj -<< -/Length 652 ->> -stream -1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 566.3681 cm +1 0 0 1 57.02362 347.2922 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -3843,17 +3991,17 @@ Q Q Q q -1 0 0 1 57.02362 558.3681 cm +1 0 0 1 57.02362 339.2922 cm Q q -1 0 0 1 57.02362 540.3681 cm +1 0 0 1 57.02362 321.2922 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F4 10 Tf 12 TL 155.3042 0 Td (GNU Affero General Public License v3) Tj T* -155.3042 0 Td ET Q Q q -1 0 0 1 57.02362 509.5681 cm +1 0 0 1 57.02362 290.4922 cm q q 1 0 0 1 0 0 cm @@ -3961,75 +4109,75 @@ xref 0001537501 00000 n 0001537707 00000 n 0001537913 00000 n -0001538182 00000 n -0001597158 00000 n -0001597468 00000 n -0001597738 00000 n -0001597844 00000 n -0001598099 00000 n -0001598174 00000 n -0001598324 00000 n -0001598434 00000 n -0001598599 00000 n -0001598794 00000 n -0001598911 00000 n -0001599029 00000 n -0001599171 00000 n -0001599371 00000 n -0001599506 00000 n -0001599642 00000 n -0001599812 00000 n -0001599936 00000 n -0001600067 00000 n -0001600189 00000 n -0001600385 00000 n -0001600502 00000 n -0001600629 00000 n -0001600759 00000 n -0001600951 00000 n -0001601070 00000 n -0001601204 00000 n -0001601342 00000 n -0001601487 00000 n -0001601670 00000 n -0001601788 00000 n -0001601945 00000 n -0001602083 00000 n -0001602231 00000 n -0001602381 00000 n -0001602499 00000 n -0001602634 00000 n -0001602785 00000 n -0001602915 00000 n -0001603038 00000 n -0001603147 00000 n -0001603282 00000 n -0001607473 00000 n -0001616363 00000 n -0001623297 00000 n -0001630433 00000 n -0001639809 00000 n -0001652294 00000 n -0001659564 00000 n -0001665719 00000 n -0001674911 00000 n -0001680039 00000 n -0001680742 00000 n -0001680880 00000 n -0001680914 00000 n -0001680948 00000 n -0001680982 00000 n -0001681016 00000 n -0001681050 00000 n -0001681084 00000 n -0001681118 00000 n -0001681152 00000 n -0001681186 00000 n -0001681221 00000 n +0001538119 00000 n +0001597095 00000 n +0001597405 00000 n +0001597723 00000 n +0001597829 00000 n +0001598084 00000 n +0001598159 00000 n +0001598309 00000 n +0001598419 00000 n +0001598584 00000 n +0001598779 00000 n +0001598896 00000 n +0001599014 00000 n +0001599156 00000 n +0001599356 00000 n +0001599491 00000 n +0001599627 00000 n +0001599797 00000 n +0001599921 00000 n +0001600052 00000 n +0001600174 00000 n +0001600370 00000 n +0001600487 00000 n +0001600614 00000 n +0001600744 00000 n +0001600936 00000 n +0001601055 00000 n +0001601189 00000 n +0001601327 00000 n +0001601472 00000 n +0001601655 00000 n +0001601773 00000 n +0001601930 00000 n +0001602068 00000 n +0001602216 00000 n +0001602366 00000 n +0001602504 00000 n +0001602639 00000 n +0001602790 00000 n +0001602920 00000 n +0001603043 00000 n +0001603152 00000 n +0001603287 00000 n +0001607478 00000 n +0001616368 00000 n +0001623302 00000 n +0001630438 00000 n +0001639814 00000 n +0001652299 00000 n +0001659569 00000 n +0001665724 00000 n +0001676005 00000 n +0001683780 00000 n +0001684725 00000 n +0001684863 00000 n +0001684897 00000 n +0001684931 00000 n +0001684965 00000 n +0001684999 00000 n +0001685033 00000 n +0001685067 00000 n +0001685101 00000 n +0001685135 00000 n +0001685169 00000 n +0001685204 00000 n trailer << /ID -[<1901de7d5bde6fbe13354188e649766a><1901de7d5bde6fbe13354188e649766a>] +[<044456556cbd64cb0139e1a926fb6fa3><044456556cbd64cb0139e1a926fb6fa3>] % ReportLab generated PDF document -- digest (opensource) /Info 25 0 R @@ -4037,5 +4185,5 @@ trailer /Size 86 >> startxref -1681256 +1685239 %%EOF diff --git a/whitepaper/uncommonlisp-whitepaper.rst b/whitepaper/uncommonlisp-whitepaper.rst index f692056..35733c4 100644 --- a/whitepaper/uncommonlisp-whitepaper.rst +++ b/whitepaper/uncommonlisp-whitepaper.rst @@ -472,10 +472,27 @@ The key insight: ``ln`` of a negative number enters the complex plane. Since we All trigonometric functions follow from complex exponentials, which follow from ``exp``, which follows from ``eml``. -8.6 Verification -^^^^^^^^^^^^^^^^^ +8.6 Verification & Friction Analysis +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -The proof is verified at three levels: +The proof is verified at three levels, with dramatically different friction: + +.. table:: + :widths: 30 12 25 33 + + ============================== ======== ========================= ================================= + Approach Time Guarantee Friction + ============================== ======== ========================= ================================= + Python (numerical) 0.04s 1e-10 tolerance Low: evaluate & compare + uncommonlisp (numerical) 59s 1e-10 tolerance High: O(N²) brute-force search + Lean 4 (formal proof) 1.5s kernel-verified certainty Medium: 5 rewrites, type-check + ============================== ======== ========================= ================================= + +**The formal proof is 40x faster than the brute-force search & provides mathematical certainty instead of floating-point tolerance.** This is MOAD-0001 (the sedimentary defect) at the proof methodology layer: O(N²) search friction where O(1) algebraic reasoning suffices. + +The numerical approaches enumerate all pairwise EML compositions at each depth, comparing results against target functions. This grows quadratically with the number of known values. The Lean proof does 5 algebraic rewrites, each applying an axiom (``exp(ln(x)) = x``, ``ln(exp(x)) = x``, ``ln(1) = 0``). The type checker confirms each rewrite in microseconds. No search. No tolerance. No conjecture dependency. + +**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 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. 1. **Numerical verification** (``proof/eml_proof.py``): Python script using ``cmath`` at high precision. Verifies every derivation step with tolerance ``1e-10``. Includes brute-force tree search at depth ≤ 4 confirming that eml compositions reach the expected targets.