Machine-Checked Anytime-Valid Monitoring of Online Predictors under Prefix-Dependent Finite Dynamics

When a learned dynamics predictor is monitored as data arrive, the user may stop at any time and report whichever predictor, or mixture of predictors, currently looks best; a fixed-horizon guarantee does not survive that choice. We give a Lean 4 machine-checked certificate that does. A finite catalog of one-step prediction rules, declared before monitoring, is scored along one trajectory of a finite-state process whose transitions may depend on the whole observed prefix. No Markov, stationarity, or mixing assumption is used, and the rules may update online as long as each prediction is fixed before the next state is seen. Outside one event of probability at most delta, simultaneously at every time and for every weighting of the catalog chosen from the observed path, the certificate upper-bounds the observed-prefix average conditional risk. This is the average, over the steps actually seen, of the expected one-step loss given the past. It is not a bound on future or stationary risk. The bound adapts to the observed variance of the scores, and at an explicit tilt schedule it is checked to shrink to zero along the path. On a checked two-state example with an online rule, the certified risk at n = 512 is below 0.28 at the scheduled tilt and 0.029 when the smallest of the bounds over the tilts allowed at that time is reported, against a true value of 0.0015. The statistical ingredients are known; the contribution is the machine-checked composition, including the path law and the timing of predictions.