Spectral Insurance: Aggregate Loss Distribution Without Monte Carlo

The insurance industry computes aggregate loss distributions — the foundation of Solvency II internal models, Own Risk and Solvency Assessment (ORSA), and reserve adequacy testing — almost exclusively through Monte Carlo simulation. This paper presents an alternative: a deterministic spectral method that replaces simulation with exact computation from 130 Fourier-cosine coefficients.

The Spectral Fenton framework represents the aggregate loss distribution of a multi-line insurance portfolio as a sum of correlated lognormal claim severities. The eigenvalue decomposition of the inter-line correlation matrix reduces the high-dimensional integration to a sequence of one-dimensional quadratures, yielding closed-form expressions for the cumulative distribution function, Value-at-Risk, Expected Shortfall, and the Solvency Capital Requirement. The mathematical core — Mixture Collapse, subadditivity of spectral risk measures, exponential convergence in the conditioning dimension, and the six-component error decomposition — is formally verified in Lean 4 with Mathlib across 112 files and zero sorry (unproved assertions).

Under the correlated lognormal model, the method is deterministic (no sampling noise), achieves empirical precision \(\varepsilon < 5.2 \times 10^{-9}\) (see Section 11), auditable (the entire risk profile fits in 1.04 KB), and fast (a 2,500-scenario stress grid completes in 162 seconds versus 27.5 minutes for Monte Carlo at assumed per-query timings). For Solvency II internal model approval, it eliminates both computational error (MC noise) and model risk (unverified formulas), offering regulators a formally verified, reproducible alternative to simulation.

Keywords: aggregate loss distribution, Solvency II, spectral methods, Fourier-cosine expansion, Monte Carlo replacement, formal verification, Lean 4, Expected Shortfall, insurance risk