34.8. Assurance — and what a green status does not mean
The last group is about the document's own evidence.
-
M23 — Claims linked to declarations. Every load-bearing definition and theorem links to the declaration realizing it and carries that declaration's machine-checked status, so a reader can follow any equation to the source the deployed code is built from.
-
M24 — Graph and ledger from the same nodes. A dependency graph and an assurance ledger generated from those same nodes — generated from the same nodes specifically, so that neither view can omit a claim the chapters cite.
-
M25 — The limits of a green status. The rubric that keeps the other twenty-five honest. A green status means a particular thing, and the two ways it is over-read are both worth stating in the document rather than leaving to the reader: a theorem proved at the real-number carrier is not a statement about the floating-point kernel that runs, and a measured quantity is not a proved one. A document that states both limits plainly is stronger than one that does not, not weaker.
-
M26 — What a measurement must name. The measurement half of that, made concrete. A speedup is a curve and not a number; a best-of-
nis biased byn; a threshold below the dispersion of the measurement it is compared against decides nothing. The rubric is discharged by naming, for each reported measurement, the parameter it was swept over, the denominator it is relative to, and the statistic it reports.