Fin Markowitz

We present two results. Part I is the first machine-checked formalization of Markowitz (1952) mean-variance optimization in Lean 4, covering the Merton (1972) closed-form solution, two-fund separation, the efficient frontier, and the Capital Market Line. The formalization comprises 29 Lean 4 statements (0 sorry, 0 axioms) across 6 files: 10 substantive algebraic verifications (Merton constraint satisfaction, GMV optimality, frontier parabola, two-fund combination), 8 structural lemmas (KKT rearrangements, Euler decomposition identities), and 11 definitional identities confirming type-level consistency.

Part II extends the framework from mean-variance to mean-CVaR using the Spectral Fenton Distribution (Nagy, 2026a). Classical mean-variance optimization minimizes \(w^T \Sigma w\), a symmetric measure that penalizes upside and downside equally. We replace variance with Conditional Value-at-Risk (CVaR), a coherent risk measure that captures tail risk. The key obstacle --- that CVaR has no closed form for correlated lognormal portfolios --- is resolved by the Spectral Fenton Distribution, which provides an analytic CVaR from 128 Fourier coefficients. We derive the analytic gradient \(\partial \text{CVaR}_\alpha / \partial w_i\) via the chain rule through the characteristic function, enabling gradient-based mean-CVaR optimization without Monte Carlo simulation. For a 5-asset portfolio, the analytic gradient is \(\sim\)21\(\times\) faster than finite-difference Monte Carlo; for larger portfolios, the speedup grows linearly with \(n\) due to the \(O(n)\) analytic gradient versus \(O(n)\) Monte Carlo reruns. The mean-CVaR efficient frontier is non-parabolic and asymmetric, reflecting the lognormal tail structure that mean-variance optimization ignores. The ES kernel underlying the gradient is Lean-verified; the chain rule through the product characteristic function is an analytic derivation whose algebraic structure (linearity, scale invariance) is formalized but whose full measure-theoretic content is not machine-checked.