The Risk Coding Theorem: Exponential Convergence of Spectral Expected Shortfall

Expected Shortfall (ES) replaced Value-at-Risk as the primary risk measure in Basel III's Fundamental Review of the Trading Book, yet its estimation by Monte Carlo simulation converges at rate \(O(1/\sqrt{M})\) — requiring \(10^6\) paths for three-digit accuracy. We prove that spectral ES, computed via eigenfunction expansion of the loss density, converges at rate \(O(\rho^{-N})\) where \(\rho > 1\) is the analyticity radius of the loss distribution and \(N\) is the number of spectral modes. This exponential rate is formalized as a Risk Coding Theorem: the number of modes sufficient for accuracy \(\varepsilon\) is \(N(\varepsilon) = H_{\text{risk}} \cdot \log(C/\varepsilon)\), where \(H_{\text{risk}} = 1/\log\rho\) is the risk entropy — a single scalar that characterizes how compressible a loss distribution is. Higher risk entropy (heavier tails, lower \(\rho\)) requires more modes; the rate is independent of portfolio dimension.

We verify 30 theorems across three layers: (1) ES coherence (Acerbi 2002 axioms), (2) convergence rate separation (MC polynomial vs spectral exponential), and (3) the Risk Coding Theorem with regulatory implications for capital charges, backtest power, and procyclicality. All results are machine-verified in the Lean 4 and exportable to Lean 4.