BAPR: Bayesian amnesic piecewise-robust reinforcement learning for non-stationary continuous control

Real-world control systems frequently operate under piecewise stationary conditions, where dynamics remain stable for extended periods before undergoing abrupt regime changes. Standard robust RL methods face a fundamental dilemma: a globally conservative policy wastes performance during stable periods, while a locally adaptive policy risks catastrophic failure when the regime changes undetected. We propose BAPR (Bayesian Amnesic Piecewise-Robust SAC), which unifies Bayesian Online Change Detection (BOCD) with robust ensemble RL. The BAPR operator -- a convex combination of mode-conditional Bellman operators weighted by a frozen belief distribution -- is a γ-contraction. A complementary counterexample, machine-verified in Lean 4, establishes a sharp boundary: when beliefs depend on the Q-function, the contraction factor becomes γ+ λΔ (where Δ is the mode reward gap), and contraction fails exactly when γ+ λΔ at least 1. We derive a component-wise formal error budget for the abstract operator -- every component machine-verified -- bounding post-switch recovery; the budget applies to the abstract mode-mixture operator and inherits to the implemented shared-critic algorithm only through the frozen-parameter design intuition. All results are formally verified with no sorry (1,145 lines across 3 Lean 4 files, 22 machine-verified theorems). BOCD drives an adaptive conservatism mechanism: the policy becomes maximally conservative after detected change-points and smoothly relaxes as confidence grows, with detection delay O((1/δ)). A context-conditioning module trained via RMDM loss provides mode-aware representations from simulator-provided mode IDs at training time and requires no mode labels at deployment.