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

ArXiv ID: 2505.12840 “View on arXiv”

Authors: Jingyuan Li

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.

Keywords: first-order stochastic dominance, geometric framework, formal verification, Lean 4 theorem prover, survival probabilities, Multi-asset (Portfolio Selection)

Complexity vs Empirical Score

• Math Complexity: 8.0/10
• Empirical Rigor: 1.5/10
• Quadrant: Lab Rats
• Why: The paper relies heavily on advanced mathematical formalization using the Lean 4 theorem prover and measure-theoretic concepts, but focuses on theoretical equivalence proofs and does not involve backtesting, real data, or implementation-ready strategies.

  flowchart TD
    G["Research Goal: Formalize N-Dim FSD"] --> M["Geometric Framework via Survival Probabilities"]
    M --> I["Input: Random Vectors & Orthants"]
    I --> C["Computation: Lean 4 Theorem Prover"]
    C --> F1["Equivalence Proven"]
    C --> F2["Tractable Integration Bypassed"]
    F1 & F2 --> O["Outcomes: Verified Framework & Economic Applications"]
    O --> O1["Portfolio Selection"]
    O --> O2["Risk Management"]