← All Papers · Formal Verification

Frequency-Domain Theory of Financial Economics: Thirteen Fundamental Results from One Decomposition

Tamás Nagy, Ph.D. Updated 2026-03-03 Working Paper Formal Verification Lean-Verified
Download PDF View in Graph BibTeX

Abstract

A market is a spectrum. We show that thirteen fundamental results in financial economics --- seven core classical theorems and six domain extensions --- all follow from a single structural assumption: the return density of any portfolio can be decomposed into \(N\) independent Fourier modes \(A_k(t)\), each evolving as an Ornstein--Uhlenbeck process with mode-dependent autocorrelation time \(\tau_k \sim k^{-\alpha}\).

The seven core results are: (1) the risk-return trade-off, with efficient frontier \(\sigma^2_{\min}(\mu) = \mu^2 / \sum SR_k^2\); (2) the Capital Market Line, with slope \(\sqrt{\sum SR_k^2}\); (3) the Sharpe ratio maximum, via the Pythagorean theorem in risk space; (4) the Kelly criterion, with optimal log-growth \(g^* = \frac{1}{2}\sum SR_k^2\); (5) the diversification principle, where independent modes add Sharpe in quadrature \(SR_{\text{total}} = \sqrt{N} \cdot \overline{SR}\); (6) the Efficient Market Hypothesis, which holds in aggregate (\(\sum w_k SR_k = 0\) at equilibrium) while individual modes carry temporary alpha; and (7) the unification of momentum with mean reversion as the low- and high-frequency limits of the same dynamics.

The six extensions apply the same framework to: the CAPM and spectral beta, Fama--French factors as spectral modes, the volatility smile as the spectral state of the risk-neutral density, the yield curve as three Fourier modes, bubbles and crashes as mode displacement, and behavioral finance as asymmetric mean reversion.

All thirteen results are formally verified in Lean 4 with zero sorry. The proofs are elementary --- linear algebra and calculus of the OU process --- and all compile under lake build with Lean v4.28.0 and Mathlib.

Length
7,009 words
Claims
8 theorems
Status
Working Paper

Connects To

Universal Foundations: A Verified Library of Core Mathematic...

Browse all Formal Verification papers →