Add friction benchmark to whitepaper: MOAD-0001 at the proof layer
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.
This commit is contained in:
parent
4d8cd9f1f8
commit
b81c8923c0
2 changed files with 348 additions and 183 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue