Prove error bounds on formally-verified natural logarithm - #589

Open

duncancmt wants to merge 18 commits into

dcmt/ln-atarparafrom

Commits on Jun 21, 2026

Quantify maximum `lnWadToRay` error
duncancmt
committed
ce5671f
More precision
duncancmt
committed
d0a235e
Refine maximum error comment

duncancmt
and
codex
committed
c3428d3

Commits on Jun 23, 2026

Ln: prove lnWadToRay error bound < 1.7035 ulp at bias margin 0.3387

duncancmt
and
claude
committed
e0de997

Commits on Jun 24, 2026

Ln: add curved degree-22 capUB cap for the LT branch (lt_x1_cap_d22)

duncancmt
and
claude
committed
9915741
Ln: add LT capUB-direction reduction (lt_pos_cut_reduced)

duncancmt
and
claude
committed
8bf87c6
Ln: complete LT error-bound cell route; LT cell cap = 1.698944562 ulp

duncancmt
and
claude
committed
4856130
Ln: tighten lnWadToRay error bound to < 1.6990 ulp (wire LT cell route)

duncancmt
and
claude
committed
2355752

Commits on Jun 25, 2026

Ln: tighten lnWadToRay error bound to < 1.6986 ulp (raise bias 4 slop-units)

duncancmt
and
claude
committed
02f249d
Ln: derive errLtW/errGeW as formulas instead of tracked literals

duncancmt
and
claude
committed
ae24c38
Ln: generate error-bound cert literals + cell covers at CI time (untrack)

duncancmt
and
claude
committed
d7a2962
docs: record 1.6986 ulp result + never-overshoot/not-too-low cert lesson

duncancmt
and
claude
committed
bac19d3
Ln: CI-generate all derived cert artifacts (floor cells + BIASCAPNUM); clean lint

duncancmt
and
claude
committed
cc69798
Ln: drop remaining unused simp arguments (warning-free build)

duncancmt
and
claude
committed
ef29786
Merge claude/ln-bounds into dcmt/ln-bounds
duncancmt
committed
6d75537
Clean up AI slop
duncancmt
committed
39d5eb1
Fix merge artifact
duncancmt
committed
17a898d
Ln: drop demonstrative Python checks; self-contain cert-literal generator

duncancmt
and
claude
committed
10832ec