7.2 Proof internals
ConvexSubgaussian/Internal/GaussianProof.lean: the analytic proof body. Contains the layer-cake lemmas, envelope construction, Gaussian closed-form calculations, monotone ratio argument, construction of the extremal measure, and the reduction from stop-loss comparison to convex domination.