6 Main theorem
Combining the envelope domination from Chapter 5 with the extremal witness from Chapter 4 yields the sharp comparison theorem.
The sharp admissible Gaussian scale is \(c_\star = c_0\). Equivalently:
Every centered real random variable satisfying \(\mathbb {P}(|X|{\gt}t)\le 2e^{-t^2/2}\) for all \(t \ge 0\) is convex-dominated by the centered Gaussian law of scale \(c_0\).
For every \(c {\lt} c_0\), convex domination by the Gaussian law of scale \(c\) fails, already for the canonical witness \(\mu ^\star \) and an explicit hinge test function.
For domination: Theorem 15 shows that the Gaussian stop-loss transform at scale \(c_0\) dominates the sharp envelope \(J_G\). Theorem 8 then upgrades this stop-loss comparison to full convex domination.
For sharpness: Theorem 11 identifies the stop-loss of the canonical witness \(\mu ^\star \) with the envelope itself. At the threshold \(u = cz\), the Gaussian stop-loss of scale \(c\) evaluates to \(c\varphi (z) - up_0\), while the envelope is at least \(B - up_0\). If \(c {\lt} c_0 = B/\varphi (z)\), then the witness stop-loss is strictly larger. The hinge function \(x \mapsto (x-u)_+\) therefore exhibits a convex test function for which the comparison fails.
For code navigation, the two halves also appear separately in GaussianAsymptotics.lean as gaussianDomination_c0 and gaussianSharpness_below_c0.