SPAR: Streaming Prior-Anchored Ridge — reference implementation, result artifacts, and Lean 4 formalization

This repository goes with the paper "Finite-Cadence Refresh Equilibria for Streaming Prior-Anchored Ridge: A Closed-Form Forgetting Window and Spectral Correction" by Mrigank Shekhar Singh (DLDAV Model School, Shalimar Bagh). The idea is simple. When a model learns from data that keeps changing, it has to balance two things: how much to trust what it already knows, and how much old data to forget. SPAR sets both of these automatically, from the model's own prediction errors, so nothing has to be tuned by hand. Everything needed to check the paper is here: the Python code, the results behind every table and figure, the LaTeX source with the compiled PDF, and the Lean 4 proofs of the main algebra. To reproduce, install the requirements and run `python scripts/run_all.py --steps quick`. The full study takes hours and can be resumed if interrupted. The paper builds with `bash paper/build.sh` (or `paper/build.cmd` on Windows), and the Lean proofs with `bash theory/lean/build_ogd.sh`. The EEG data is included; the electricity and other time-series datasets are free downloads, with instructions in the README. Code is also on GitHub: https://github.com/mrigank-script/spar-streaming-prior-anchored-ridge Version 1.0.0. Code under MIT; paper and figures under CC BY 4.0.