Add formally verified natural logarithm - #585

Open

duncancmt wants to merge 94 commits into

dcmt/codex-prove-sqrt-cbrtfrom

dcmt/ln-atarpara

Commits on Jun 8, 2026

Add optimized `lnWad` implementation from @atarpara for formal verification
duncancmt
committed
d505ba0

Commits on Jun 9, 2026

Update @atarpara's `lnWad` implementation
duncancmt
committed
9b77b6f

Commits on Jun 11, 2026

Rewrite `lnWad` to guarantee floor semantics

committed
ed58a7b
Make `lnWad` return a ray-basis result with mixed fixed-point bases

duncancmt
and
claude
committed
61fb0a4
Fix `lnWad(1e18)`, add `lnWadToWad`, certify monotonicity

committed
b09c801

Commits on Jun 12, 2026

Prove `lnWad` monotonicity in Lean over its entire domain

committed
d0168b3
Widen `lnWad` bias margin to 0.500 ulp

committed
5c8b675
Add exponential partial-sum toolkit for the `lnWad` floor specification

duncancmt
and
claude
committed
859b0ef
Add recentered certificate checker, constant caps, and model bracket

duncancmt
and
claude
committed
d4df3aa
Add floor-spec bracket polynomials, cell certificates, and division brackets

duncancmt
and
claude
committed
5166d4d
Add homogenized-form unfoldings and difference-factoring helpers

duncancmt
and
claude
committed
d526940
Split floor-cert cells and add interval-product helpers

committed
8a16ecc
Prove divided-difference monotonicity of the bracket stage polynomials

duncancmt
and
claude
committed
2910887
Widen the divided-difference box bound past the w* corner

duncancmt
and
claude
committed
253b991
Prove the first bracket cross-theorem: X1 below the upper certificate rational

duncancmt
and
claude
committed
ea44107
Prove bracket_ge_lo: pipeline X1 sits above the lower certificate rational

duncancmt
and
claude
committed
35affc1
Prove bracket_lt_up: pipeline magnitude below upper certificate on m < S

duncancmt
and
claude
committed
ab781dd
Prove bracket_lt_lo: pipeline magnitude above lower certificate on m < S

duncancmt
and
claude
committed
1369a54
Tighten H-certificates to the K=22 tail-bound requirement

duncancmt
and
claude
committed
c54a359
Add cert-to-cap conversion layer (FloorCaps)

duncancmt
and
claude
committed
b66afe6
Add per-exponent budget inequalities and capLB_cancel

duncancmt
and
claude
committed
9951008
Add floor-spec assembly V-scale decomposition lemmas

committed
1da72b0
Literal-based certificate decides with sharing-fixed shift checker

committed
1b3b4b8
Add Kronecker identity-testing layer for polynomial equalities

duncancmt
and
claude
committed
dcb83cf
Packed divide-and-conquer Taylor shifts for the certificate cell walks

committed
9eb3594
Assembly: upper master chain on the m >= S branch, k >= 0

duncancmt
and
claude
committed
626c336
Assembly: lower master chain on the m >= S branch, k >= 0

duncancmt
and
claude
committed
ec968c8
Assembly: upper master chain, m >= S branch, negative binade shift

duncancmt
and
claude
committed
e405872
Assembly: lower master chain, m >= S branch, negative binade shift

duncancmt
and
claude
committed
a26251f
Assembly: upper master chain, m < S branch, nonnegative binade shift

duncancmt
and
claude
committed
c782a33
Assembly: lower master chain, m < S branch, nonnegative binade shift

duncancmt
and
claude
committed
5e3a983
Assembly: upper master chain, m < S branch, negative binade shift

duncancmt
and
claude
committed
3e0dd70
Assembly: lower master chain, m < S branch, negative binade shift

duncancmt
and
claude
committed
3e94077
Add reciprocal-side strict budgets for the r + 2 <= 0 B-atom

duncancmt
and
claude
committed
da4b697
Assembly: A-atom master for negative outputs, m < S branch, k >= 0

duncancmt
and
claude
committed
2d54ff3
Assembly: A-atom master for negative outputs, m >= S branch, k < 0

duncancmt
and
claude
committed
80c2023
Assembly: A-atom master for negative outputs, m < S branch, k < 0

duncancmt
and
claude
committed
889a519
Assembly: B-atom master for r + 2 <= 0, m < S branch, k >= 0

duncancmt
and
claude
committed
5e986fb
Assembly: B-atom master for r + 2 <= 0, m >= S branch, k < 0

duncancmt
and
claude
committed
5b0e8ad
Assembly: B-atom master for r + 2 <= 0, m < S branch, k < 0

duncancmt
and
claude
committed
0f9afda
Assembly: relax the lower masters to r >= -1

duncancmt
and
claude
committed
e8de1c3
Full-branch X1 caps via pointwise window checks

duncancmt
and
claude
committed
172922b
Assembly: masters cover full branches via the windowed caps

duncancmt
and
claude
committed
44b1317
Prove the floor specification of the lnWad model

duncancmt
and
claude
committed
7563c62
Wire the floor specification into the library root and CI

duncancmt
and
claude
committed
b2781ec
Document the proven floor specification in lnWad's NatSpec

duncancmt
and
claude
committed
99440fd

Commits on Jun 14, 2026

Deep-unfold the sub-literal equality decides in the cert branches

duncancmt
and
claude
committed
f7ab0db
Rename lnWad -> lnWadToRay and lnWadToWad -> lnWad

committed
9ce285c
Trim trailing-zero coefficients from the cert literals

duncancmt
and
claude
committed
06eb58f
Remove unused simp arguments flagged by the linter

duncancmt
and
claude
committed
a2ae9d4
Add lnWad wad-floor proof endpoints

duncancmt
and
codex
committed
7589941
Finish the lint cleanup: assembly/spec simp args and unused binders

duncancmt
and
claude
committed
3b1e807
Remove archaeology phrasing from ln proof comments

duncancmt
and
codex
committed
4a9c35f
Unify the Kronecker digit width at B = 38000

duncancmt
and
claude
committed
a0bf535
Name the Kronecker digit width as kB instead of repeating 38000

duncancmt
and
claude
committed
ca8146f
WIP: clean up slop
duncancmt
committed
1e4d54d
WIP: clean up slop
duncancmt
committed
836af51
WIP: clean up slop
duncancmt
committed
9a9b257
WIP: clean up slop
duncancmt
committed
a4da511
WIP: clean up slop
duncancmt
committed
be647c3
WIP: clean up slop
duncancmt
committed
1819456
Tighten ln floor-correction margin to 0.362 ulp (cert ε 0.36)

duncancmt
and
claude
committed
270c0fc
Merge claude/ln-atarpara into dcmt/ln-atarpara
duncancmt
committed
d812a0d
WIP: clean up slop
duncancmt
committed
6e4b821
Finished: clean up slop
duncancmt
committed
0db61a9
Make formal ln Python pass the translator-unit lint gate

duncancmt
and
claude
committed
390ab59
Merge claude/ln-atarpara into dcmt/ln-atarpara
duncancmt
committed
74c077e
Match the model generator to the Panic(0x12) input guard

duncancmt
and
claude
committed
f935655
Comments
duncancmt
committed
addcb5f
Launder constant-first model operands in model_eq_tail

duncancmt
and
claude
committed
1511123
Walk the ln floor margin to the 0.34-ulp error floor (M=0.3403)

duncancmt
and
claude
committed
a8f3ca4
Merge claude/ln-atarpara into dcmt/ln-atarpara
duncancmt
committed
a9e109d
Resolve the repo root from __file__ in gen_cert_literals.py

duncancmt
and
claude
committed
8f76323
Correct Ln comments

duncancmt
and
codex
committed
8921c92
Silence large-exponent elaboration warnings in the ln proof

duncancmt
and
claude
committed
3c7686e
Fix tests

duncancmt
and
claude
committed
90467f6
Speed up Ln certificate-branch proofs ~80×

duncancmt
and
claude
committed
76c68be
Style
duncancmt
committed
8acd5b7
Style
duncancmt
committed
8d0cce8
Style
duncancmt
committed
fdf141a
Add explicit ln cut specification

duncancmt
and
codex
committed
855a301
Merge branch dcmt/ln-atarpara into codex/lnwad-exp-log-cut
duncancmt
committed
ec3acff
Fix ln formal CI after style merge

duncancmt
and
codex
committed
f6417b0

Commits on Jun 15, 2026

Style
duncancmt
committed
12f832e
Ln: shrink the rational coefficients to byte-minimal staircase bases

duncancmt
and
claude
committed
c66f10b
Ln: shrink the mantissa basis to Q95, saving a byte on s

duncancmt
and
claude
committed
1c21729
Formatting
duncancmt
committed
c3cb2c6
Ln: limit coefficient bases to the monotonicity-positive minimum

duncancmt
and
claude
committed
94177f6
Resync lnWad floor + monotonicity proofs to the corrected implementation

duncancmt
and
claude
committed
0a07547
Remove sandwich/div lemmas orphaned by the Q95 stage shifts

duncancmt
and
claude
committed
612689f
Ln: use the exact continuous-minimax c0/Q4/Q1; resync the proof

duncancmt
and
claude
committed
9515eb2

Commits on Jun 16, 2026

Golf
duncancmt
committed
876fc37
Track lnWadToRay's output-based zero correction in the proof

duncancmt
and
claude
committed
de5df3a
Lint
duncancmt
committed
5074a40