Full-Tail Backtesting: Beyond Pointwise Validation for Expected Shortfall

Every existing Expected Shortfall backtest evaluates a risk model at a single confidence level. This paper introduces four backtesting methods that test the entire tail distribution simultaneously — methods that are structurally impossible without exact closed-form computation of the CDF and density. Using the exact distribution of the sum of correlated lognormals (Nagy, 2026), which provides both in closed form from 128 Fourier coefficients, we construct: (1) a full-tail backtest that evaluates \(\text{ES}_\alpha\) for all \(\alpha\) simultaneously using a sup-norm statistic, strictly dominating any single-\(\alpha\) test for tail-shape alternatives; (2) an eigenmode backtest that decomposes portfolio loss into orthogonal factor contributions and tests each independently, diagnosing which component of the model is wrong; (3) a sequential probability ratio test (SPRT) for tail losses that rejects miscalibrated models in days rather than the year required by fixed-sample tests, using pointwise density values that Monte Carlo simulation cannot provide; and (4) a conditional full-tail backtest that tests not only marginal correctness but temporal independence of probability integral transform residuals, formalizing Rosenblatt's (1952) theorem for operational use. We prove a power hierarchy across alternative classes: each method detects a category of misspecification invisible to all lower-level tests. All four methods require exact CDF and density evaluation, which no Monte Carlo approach can deliver. All results are formally verified in Lean 4 across 12 files with zero unresolved proof obligations, though the proofs verify logical architecture rather than measure-theoretic foundations (see Section 8 for a transparent categorization). To our knowledge, this is the first suite of machine-checked backtesting methods for financial risk.

Keywords: Expected Shortfall, backtesting, spectral risk measures, sequential testing, formal verification, Lean 4, FRTB, eigenvalue decomposition

JEL Classification: G32, C12, C46