Rough Volatility: The Exponent Architecture of Options Markets

We present a complete formal derivation of the ATM implied volatility skew power law ψ(T) ∼ C · T^{H−1/2} from the rBergomi model definition through an explicit chain of verified lemmas. The Volterra kernel K(t,s) = c_H · (t−s)^{H−1/2} generates an integral whose exponent shift (H−1/2)+1 = H+1/2 is proved via ring arithmetic; the Alòs-León-Vives normalization then subtracts 1, recovering the skew exponent H−1/2. For H < 1/2 (the rough regime), this exponent is negative, explaining the observed skew explosion at short maturities. We prove 122 theorems covering the complete exponent atlas: skew, curvature, hedging error, vega correction, forward variance slope, optimal rebalancing frequency, and VaR scaling. All exponents are shown to be affine functions of the single parameter H. The formalization includes 51 typed hypotheses encoding the rBergomi model structure and stochastic calculus facts from El Euch-Rosenbaum (2019) and Alòs-León-Vives (2007). The derivation is verified in Lean 4 with 197 kernel checks and 0 errors.

Keywords: Rough volatility, rBergomi model, ATM skew, Volterra kernel, Hurst parameter, hedging error, power laws, formal verification

MSC 2020: 91G20 (Derivative securities), 60G22 (Fractional processes), 60H30 (Stochastic integral equations)

JEL: G13, C63