Geometric Formalization of First-Order Stochastic Dominance in $N$ Dimensions: A Tractable Path to Multi-Dimensional Economic Decision Analysis

TL;DR

This paper presents a new geometric framework for multi-dimensional first-order stochastic dominance, formalized in Lean 4, simplifying verification and enabling rigorous economic decision analysis.

Contribution

It introduces a geometric approach to FSD in N dimensions, formalized in Lean 4, bypassing complex measure theory and facilitating formal verification in economics.

Findings

Formalized N-dimensional FSD in Lean 4.

Proved equivalence with traditional FSD definitions.

Enabled formal analysis in economic decision-making.

Abstract

This paper introduces and formally verifies a novel geometric framework for first-order stochastic dominance (FSD) in $N$ dimensions using the Lean 4 theorem prover. Traditional analytical approaches to multi-dimensional stochastic dominance rely heavily on complex measure theory and multivariate calculus, creating significant barriers to formalization in proof assistants. Our geometric approach characterizes $N$-dimensional FSD through direct comparison of survival probabilities in upper-right orthants, bypassing the need for complex integration theory. We formalize key definitions and prove the equivalence between traditional FSD requirements and our geometric characterization. This approach achieves a more tractable and intuitive path to formal verification while maintaining mathematical rigor. We demonstrate how this framework directly enables formal analysis of multi-dimensional economic problems in portfolio selection, risk management, and welfare analysis. The work establishes a foundation for further development of verified decision-making tools in economics and finance, particularly for high-stakes domains requiring rigorous guarantees.