Spectral Interest Rate Pricing: COS-Based Derivatives from Yield Curve Coefficients

We present the first formally verified interest rate derivatives pricing engine. The Nagy spectral yield curve represents yields as a finite cosine series \(y(\tau) = A_0 + \sum_{k=1}^K A_k \cos(k\pi\tau/\tau_{\max})\) with each mode following independent Ornstein-Uhlenbeck dynamics. When the COS method (Fang-Oosterlee, 2008) is applied to this spectral model, the density coefficients \(F_n\) are determined algebraically by the yield curve coefficients \(\{A_k\}\) and their dynamics \(\{\kappa_k, \sigma_k\}\), giving caplet prices as finite cosine sums with exponential convergence \(O(\rho^{-N})\). We formally prove: (a) COS caplet pricing converges exponentially for analytic densities; (b) cap-floor parity holds exactly in the COS framework; (c) spectral Greeks \(\partial\text{Caplet}/\partial A_k\) have the same COS structure as pricing, enabling analytical computation via the chain rule through the OU characteristic function; (d) pricing is deterministic by construction. The complete framework — discount factors, forward LIBOR, COS caplet/cap pricing, Jamshidian swaption decomposition, and spectral Greeks — comprises 55 formally verified theorems with 68 verified declarations (zero sorry) in the Platonic kernel, with Lean export available through the L4 sealing pipeline. A companion Rust implementation validates the framework in a lognormal special case (see Section 4.4 for scope of verification).