Add symbolic theorem-proof verifiers for Claims 1-3 (VERIFIED via independently reconstructed symbolic derivations using SymPy)

Reproduce ATC change-point regret: log-linear regret R^2=0.985 (O(sigma^2(S+1)log T)), stable ratio 6.4 to minimax LB, bounded endogenous confounding