Forward Error Analysis of Periodically Re-Anchored Sliding-Window Inner-Product Recurrences, with Application to the Matrix Profile

The streaming matrix profile—and the SCAMP/STUMPY kernels that compute it atscale -- maintains a sliding-window inner product by periodically re-anchoring it to a full-length reseed every few ticks. We give the first forward-error analysis of this periodically re-anchored streaming recurrence, the inner-product substrate of the deployed matrix profile, and show the reseed confines error accumulation to a carry chain of length the row index p, not the stream length N . Our central result is an unconditional, machine-certified stochastic-rounding forward-error bound, parametric in the storage, accumulator, and random-bit-budget unit round-offs, whose Azuma–Hoeffding envelope is kernel-checked in Lean 4 + Mathlib at the classical-axiom surface; it holds with no distributional (zero-mean / mean-independence) hypothesis on the input, in contrast to the round-to-nearest case, which we show stalls adversarially. A deterministic envelope uniform in N (under bounded retention)is complemented by two lower bounds for p ≤ w, where w is the subsequence length: a matching lower bound on the linear-in-p carry-chain growth rate, and a quadratic Θ(p(w − p)) stall (its magnitude factor shown necessary by an IEEE-754 absorption stall machine-checked in Coq/Flocq), which together certify that both the carry-chain length and the per-product magnitude are intrinsic structural factors rather than analysis slack. The prefactor T⋆ = M 2 (the global all-time bound on the element-product) can dominate under sign-mixing inputs that produce catastrophic cancellation. The bounds are validated against a 128-bit MPFR oracle past 107 ticks (in the convergence regime 4(p+w)uacc < 1) and a 20 000-seed stochastic-rounding ensemble at fp32, fp16, and bf16. The mean-centred covariance kernel deployed in SCAMP and STUMPY is treated in a companion paper.