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

Jingyuan Li

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 an…