Finite-Cadence Refresh Equilibria for Streaming Prior-Anchored Ridge: A Closed-Form Forgetting Window and Spectral Correction
Mrigank Shekhar Singh
stat.ML
Nov 10, 2026 · v1
cs.AI cs.GT cs.LG
TL;DR
The algebraic core, refresh-chain recursion, OGD/Hedge regret bounds, and coupled contraction are formalized in Lean 4 with Mathlib: 85 declarations, no sorry.
Abstract
Recursive estimators on drifting streams must forget stale data fast enough to track the target, yet slowly enough to average out noise. In prior-anchored ridge regression, this trade-off admits a closed-form spectral decomposition in which each eigen-direction interpolates between the data solution and the prior with pull weight $s_i = ρ/ (μ_i + ρ)$. When the anchor is refreshed every $k$ steps, we show that the moving-frame offset converges to a finite-cadence equilibrium that lags the pure-leaky path by an explicit $Δ_k(s)$ while reducing estimation variance by a factor $Ψ(s, r_k)$. Minimizing the cycle-averaged risk gives $ω^* = (4ν^2 Σ/ c')^{1/3}$, $c' = σ^2 d_{\mathrm{eff}}(ρ)$, and the plug-in strength $ρ^* = σ^2 / (nδ^2)$. A random-matrix deterministic equivalent extends both laws to finite dimension, renormalizing the anchor to $ρ_{\mathrm{eff}} = ρ(e^{ζq} - 1) / (ζq)$; it matches simulation within 5% at fixed operating points and within 13% at the method's own, and rank-deficient populations reduce exactly to their active subspace. The resulting method, SPAR, calibrates window and strength online from residuals. On a 27-configuration grid the calibrated window opens on drift without divergence, and the grid defaults transfer to an hourly electricity stream and to BCI IV 2b. The core algebra, refresh chain, and regret bounds are formalized in Lean 4.
Problem
Streaming estimators on drifting data must forget stale data quickly enough to track the target and slowly enough to average out noise. The goal is a principled, closed-form way to set the forgetting window and anchor strength for prior-anchored ridge regression when the anchor is refreshed periodically.
Approach
A per-direction pull identity with weight s_i = ρ/(μ_i+ρ) decomposes the anchored solution spectrally. The moving-frame anchor offset under refresh cadence k is analyzed as an affine recursion, giving the lag and variance factors. Minimizing the cycle-averaged risk yields a closed-form window, and a random-matrix deterministic equivalent extends the result to finite dimension. The algebraic core, refresh chain, regret bounds, and contraction are machine-checked in Lean 4 with Mathlib.
Results
The finite-cadence equilibrium gives an explicit lag Δ_k(s), the optimal window ω* = (4ν²_Σ/c')^{1/3}, and plug-in strength ρ* = σ²/(nδ²). The deterministic equivalent matches simulation within 4–5% at fixed operating points and within 13% at the method's own operating points. The SPAR method transfers to electricity and BCI IV 2b streams. The Lean artifact has 85 declarations with no sorry and only the standard axioms.