1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
;;; Copyright (c) 2026 Nicholas Vermeulen
;;; SPDX-License-Identifier: AGPL-3.0-or-later
;; root.lisp — 1-D root finding with CERTIFICATES as data, and exhaustive
;; localization proofs. Pure Lisp, zero interpreter changes.
;;
;; Bisection / Newton return a tagged record (an alist of (key value) pairs)
;; describing what was found — status, bracket, iteration count, width, the
;; residual f at the estimate — never a bare number and never a raise. The
;; search uses only `+ - * /` (no libm), so every value is IEEE-deterministic
;; and the golden is portable: a given f64 bit pattern prints identically on
;; every platform, so certificate floats are bit-stable across machines. (Only
;; a libm call like exp/sin could drift by a ULP — there is none here.)
;;
;; CLAIM DISCIPLINE — the caveat is the crack. A returned root is a NUMERICAL
;; ESTIMATE with a stated bracket/residual, not a proof that a real root
;; exists. Bisection assumes f is CONTINUOUS on the bracket (declared, not
;; proven): the intermediate-value guarantee is only as good as that
;; assumption. What IS proven, exhaustively, is localization: "for every root
;; position in the declared grid, bisection returns an estimate within the
;; requested tolerance." Newton reports only "converged: |f|<eps in ≤K steps"
;; or "max-iters" / "derivative-zero" — NEVER "global root".
;; ── Certificate records (alist of (key value)) ───────────────────────────
;; ── Bisection ─────────────────────────────────────────────────────────────
;; Requires a STRICT sign change on [a,b] (f(a)·f(b) < 0); otherwise returns a
;; 'no-bracket certificate rather than guessing. Runs until the bracket width
;; ≤ eps OR max-iter steps are taken; the estimate is the final midpoint.
;; ── Newton ────────────────────────────────────────────────────────────────
;; Caller supplies f AND its derivative df (from `grad` or by hand). Stops on
;; |f(x)| < eps ('converged), K steps ('max-iters), or df(x)=0 ('derivative-zero).
;; ── Bracket inventory ─────────────────────────────────────────────────────
;; Scan [a,b] in n equal sub-intervals; return every sub-bracket (lo hi) across
;; which f changes sign — a complete inventory of the sign-change brackets on
;; that grid (it can MISS a root pair inside one sub-interval; the claim is
;; "every sign change on this grid", not "every real root").
;; ── Exhaustive localization proof ─────────────────────────────────────────
;; For the linear family f_c(x) = x - c (root at c), bisection on the ASYMMETRIC
;; bracket [c-1, c+2] must return an estimate within `eps` of c, for EVERY
;; integer root position c in the grid. Ample max-iter → 'verified; too few
;; steps to reach eps → REFUSED with the witness c that couldn't be localized.
;; The bracket is deliberately asymmetric: a symmetric one would put the linear
;; root exactly at the first midpoint (instant exact hit), hiding the width→eps
;; dependence the refutation is meant to exercise.