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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
;;; Copyright (c) 2026 Nicholas Vermeulen
;;; SPDX-License-Identifier: AGPL-3.0-or-later
;; linalg.lisp — dense LU-style Gaussian elimination: determinant, linear
;; solve, and residual, on small matrices. Pure Lisp, zero interpreter
;; changes. No BLAS, no external anything.
;;
;; Matrices are lists-of-rows (row-major); vectors are lists. Elimination uses
;; PARTIAL PIVOTING (largest-magnitude pivot in the column). A zero pivot is a
;; NAMED certificate `(status pivot-failure) (row k)` — never a silent NaN.
;; Results are alist certificates: `(status ok) (det D)` / `(status ok) (x V)`.
;;
;; DETERMINISM / PORTABILITY — `/` is float division (not rational), so choose
;; fixtures whose elimination stays on EXACT dyadic values (pivots ±1/±2,
;; triangular systems) — then dets/residuals are exact and the golden is
;; bit-portable. The exhaustive det check runs over entries in {-1,0,1,2}
;; precisely because every pivot there is ±1 or ±2, so `/` is exact and the
;; float det equals the integer formula exactly. Off that domain (e.g. a pivot
;; of 3 → 1/3) results are still IEEE-deterministic but no longer integer-exact,
;; so residual checks would need an epsilon — never print such a float.
;;
;; CLAIM DISCIPLINE — the caveat is the crack:
;; "det matches the 2×2 formula for EVERY entry grid in {-1,0,1,2}"
;; "residual ‖Ax−b‖ = 0 for every b in the declared grid, for this A"
;; NEVER "numerically stable", NEVER "correct for ill-conditioned systems".
;; Everything proven is on tiny finite grids with exact arithmetic.
;; ── List / matrix helpers ─────────────────────────────────────────────────
;; row + s*other, elementwise (works on augmented rows of any length).
;; Index of the largest-|value| entry in column k among rows k..n-1.
;; Zero out column k below the pivot row: for each i>k, row_i += -(M[i][k]/piv)·row_k.
;; Operates on all columns present (so it also transforms an augmented b column).
;; ── Certificate accessors ─────────────────────────────────────────────────
;; ── Determinant (partial-pivot Gaussian elimination) ──────────────────────
;; det = det-sign · Π pivots. Zero pivot ⇒ pivot-failure (matrix is singular).
;; ── Linear solve A x = b (augmented elimination + back-substitution) ────
;; ── Residual ‖Ax−b‖₁ ──────────────────────────────────────────────────────
;; ── Exhaustive verification ───────────────────────────────────────────────
;; (1) LU determinant equals the 2×2 closed form for EVERY matrix over the grid.
;; Singular matrices (pivot-failure) must have formula 0 — the honest match.
;; Exact over {-1,0,1,2} (pivots ±1/±2 → `/` exact). Real 4-D domain.
;; A deliberately wrong formula ("det is always 1") must be refused with a witness.
;; (2) Solve consistency: for a FIXED invertible A whose elimination stays exact,
;; every b in the grid solves with residual EXACTLY 0. Real 2-D domain over b.