driftbound
Forward-error bounds for the matrix profile's streaming inner product — machine-checked in Lean and Coq, validated to a real earthquake record.
driftbound
Read the whole series as one page- 01
- 02
The accumulator that never moved
An adversarial input where round-to-nearest throws away every increment in the same direction while the true sum climbs — and the coin flip that breaks the adversary's one weapon, measured across 20,000 seeds. - 03
The error analysis everyone cites is for a kernel nobody runs
SCAMP and STUMPY accumulate a mean-centred covariance, not the textbook inner product — and the centred case is structurally different floating-point mathematics, not a special case at mu = 0. - 04
Green is not evidence
An experiment can validate the wrong quantity against the wrong envelope and pass, a self-test canary can fail identically whether the gate works or not, and an audit command can print nothing and exit 0 — three gate designs that read green while checking nothing. - 05
Three axioms and one disclosed seam
Four verification tools, one certificate: every machine-checked theorem mechanically reduced to three classical axioms with zero unfinished proofs — and the one place two provers cannot talk to each other, named right in the theorem statements. - 06
One earthquake pinned my error bound forever
A seismic stream, a global magnitude bound wrecked by a single mainshock, a windowed bound that heals — and a scoreboard where the headline empirical legs of two papers report zero violations.