The ATM Skew Power Law: A Machine-Verified Derivation from the rBergomi Model

We derive the ATM implied volatility skew power law \(\psi(T) \sim C \cdot T^{H-1/2}\) from the rough Bergomi (rBergomi) model through a machine-verified chain of 125 theorems. The derivation proceeds in seven stages: (i) the Volterra kernel \(K(t,s) = c_H (t-s)^{H-1/2}\) is analyzed for singularity and integrability; (ii) the power integral \(\int_0^T u^{H-1/2} \, du = T^{H+1/2}/(H+1/2)\) is formalized with typed rpow expressions; (iii) the Alòs–León–Vives normalization by \(T\) yields the skew exponent identity; (iv) delta-hedging error under model misspecification scales as \(T^{2H-1}\), diverging at short maturities; (v) the vega correction shares the same exponent, proving that delta-vega hedging cannot reduce model error; (vi) the optimal rebalancing count scales as \(T^{2(1-H)}\); (vii) the observed smile curvature provides a lower bound on the hedging error coefficient. A complete exponent hierarchy is established: forward slope \(<\) hedge error \(<\) skew \(<\) \(0\). The formalization extends to variance swap term structure, calendar spread no-arbitrage constraints, VaR scaling, a complete exponent atlas showing all observables are affine functions of a single parameter \(\alpha = H - 1/2\), the short-time smile expansion geometry, pricing error bounds under \(H\) misspecification, cross-model divergence rates, and the fractional Riccati structure of the rough Heston characteristic function. Empirical validation on real SPX/VIX data (2021--2026) yields \(H = 0.35\) (variogram) and \(H = 0.30\) (skew fit), and confirms that the ATM skew predicts 75% of cross-maturity hedge error variance. Rolling \(H\) estimation over 16 quarterly windows shows remarkable stability (CV = 9.8%, range \([0.30, 0.42]\), always below \(1/2\)). Sub-period analysis separates regimes: in calm markets (VIX \(< 20\)), the model-misspecification scaling Var(P\&L) \(\sim T^{-0.26}\) is directly observed (\(R^2 = 0.76\)), while in volatile markets, discrete hedging error dominates. A practical risk capital formula shows short-maturity options require \(1.9\times\) more capital than the \(\sqrt{T}\) rule predicts. All 125 theorems are verified by the Lean 4 with zero axioms; stochastic calculus results are cited as published facts. The theoretical framework is implemented as a production computation engine: a Rust-native rough Heston pricer solving the fractional Riccati equation via Adams discretization with precomputed Volterra kernel weights, batch characteristic function evaluation, and COS-method pricing at 11,600 surface points/second. A three-stage calibration pipeline — compact differential evolution (global search), Nelder-Mead simplex, and Gauss-Newton Levenberg-Marquardt with parallel Jacobian computation — calibrates an 8-parameter model to a 60-quote surface in 1.2 seconds (cold-start) or 0.85 seconds (warm-start). In a controlled head-to-head comparison against SABR-style per-slice quadratic fits on a realistic 45-quote