Arbitrage-Free Term Structure via Spectral Coefficient Constraints

We propose a yield curve model that combines three properties rarely found together: (i) arbitrage-free dynamics by construction, (ii) strong empirical fit with interpretable factors, and (iii) partial formal verification in Lean 4. The model represents the yield curve as a spectral decomposition \(y(\tau) = \sum_{k=0}^{K} A_k(t) \cdot \psi_k(\tau)\) where \(\psi_k\) are Fourier-cosine basis functions on the maturity domain and \(A_k(t)\) follow independent Ornstein--Uhlenbeck processes with autocorrelation times \(\tau_k = C \cdot k^{-\alpha}\). The Fejér bound on the coefficients guarantees yield non-negativity (Lean-verified) and, under a weighted extension, forward-rate positivity --- without requiring the Heath--Jarrow--Morton drift condition. Applied to US Treasury data (2004--2025), the first three cosine modes align with the Nelson--Siegel level, slope, and curvature interpretation, PCA explains 99.9\% of yield variance with 3 factors, and the power law \(\tau_k \sim k^{-1.3}\) fits with \(R^2 = 0.76\) across 6 modes in normal regimes. The power law breaks down during crises. The term premium decomposes naturally into mode risk premia. Core structural results (yield non-negativity, OU dynamics, power-law monotonicity) are machine-verified in Lean 4 with zero sorry.