driftbound
Forward-error bounds for the matrix profile's streaming inner product — machine-checked in Lean and Coq, validated to a real earthquake record.
- 01 Thirty-one papers, zero error analyses A sliding-window inner product updated one product at a time is the streaming similarity engine under motif and anomaly mining — its rounding error grows linearly in stream length, and across thirty-one matrix-profile papers nobody had ever done the forward-error math, or turned the fix into a config knob.
- 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.