Correlation Is Not a Number — It's a Spectrum: Frequency-Domain Dependence for Portfolio Risk

The Pearson correlation \(\rho_{ij}\) between two assets is a single number. It is blind to frequency: it cannot distinguish whether two assets co-move in long-term trends or in daily noise. We introduce Spectral Correlation, a frequency-domain decomposition where the dependence between assets is a function \(\rho_{ij}(k)\), one value per Fourier mode \(k\). In normal markets, correlation concentrates in low frequencies (trends move together, noise is independent). In crisis, the frequency structure of dependence restructures: during the stress phase preceding a crisis, correlation energy spreads to higher frequencies --- a detectable early warning signal. The Spectral Flatness, defined as the normalized entropy of \(|\rho_{ij}(k)|^2\), provides a single-number crisis indicator that detects regime changes from the frequency structure of dependence. We formalize key properties in Lean 4: each spectral correlation is bounded in \([-1, 1]\) (derived from Cauchy--Schwarz), the weighted-sum structure relating spectral and Pearson correlation is verified as a structural identity, and the flatness metric (formalized via a min/max ratio characterization) is bounded in \([0, 1]\). The spectral correlation forms a 3-tensor \(C_{ijk}\) (asset \(\times\) asset \(\times\) frequency) that unifies the Spectral Fenton framework with higher-order dependence structures.