Fin American Basket

We prove the first quantitative convergence guarantees for a deterministic American basket pricer with dimension-free cost. The Eigen-COS backward induction method decomposes an \(n\)-asset correlated basket into eigenvalue modes, integrates the dominant modes via Gauss-Hermite quadrature, applies Fenton-Wilkinson lognormal approximation per conditioning scenario, and prices via COS-expansion backward induction with early exercise in Fourier space.

We establish a three-source error decomposition: COS truncation \(O(\rho^{-N})\), FW approximation \(O(\text{CV}^3)\), and GH quadrature \(O((2Q)!^{-1})\), yielding total error \(\varepsilon \leq M \cdot B \rho^{-N} + M \cdot C \cdot \text{CV}^3 + D/(2Q)!\) over \(M\) exercise dates. The computational cost is \(O(Q^{K_{\text{eff}}} \cdot N \cdot M)\), where \(K_{\text{eff}} \leq n\) is the effective rank of the correlation matrix — dimension-free when correlation is high. We prove COS dominance over tree methods (cost ratio \(\to \infty\) as \(\varepsilon \to 0\)) and over Longstaff-Schwartz (deterministic vs stochastic convergence, exponential vs algebraic rate).

The proof architecture comprises 10 Lean 4-verified results (zero sorry) organized in a five-tier dependency DAG, building on four independently verified proof libraries (45+ theorems across SpectralTransfer, SpectralFenton, AmericanBasket, and TreeVsSpectral). Of the 10 results, 5 contain non-trivial proof reasoning (calc chains, monotonicity composition, barrier inheritance); the remaining 5 are definitional instantiations that compose imported results into the Eigen-COS American setting. We complement the formal theory with numerical experiments on a 5-asset GBM basket, confirming exponential convergence in \(N\) and super-exponential convergence in \(Q\), and demonstrating order-of-magnitude speedups over Longstaff-Schwartz at matched accuracy.