Quantifying Bounded Rationality: Formal Verification of Simon's Satisficing Through Flexible Stochastic Dominance

Paper: arXiv 2507.07052

Authors: Jingyuan Li, Zhou Lin

Abstract

This paper introduces Flexible First-Order Stochastic Dominance (FFSD), a mathematically rigorous framework that formalizes Herbert Simon’s concept of bounded rationality using the Lean 4 theorem prover. We develop machine-verified proofs demonstrating that FFSD bridges classical expected utility theory with Simon’s satisficing behavior through parameterized tolerance thresholds. Our approach yields several key results: (1) a critical threshold $\varepsilon < 1/2$ that guarantees uniqueness of reference points, (2) an equivalence theorem linking FFSD to expected utility maximization for approximate indicator functions, and (3) extensions to multi-dimensional decision settings. By encoding these concepts in Lean 4’s dependent type theory, we provide the first machine-checked formalization of Simon’s bounded rationality, creating a foundation for mechanized reasoning about economic decision-making under uncertainty with cognitive limitations. This work contributes to the growing intersection between formal mathematics and economic theory, demonstrating how interactive theorem proving can advance our understanding of behavioral economics concepts that have traditionally been expressed only qualitatively.

Complexity vs Empirical Score

• Math Complexity: 8.5/10
• Empirical Rigor: 1.5/10
• Quadrant: Lab Rats — theoretically deep, empirically untested

Why this score: The paper presents a highly rigorous mathematical formalization of Simon’s satisficing model using the Lean 4 interactive theorem prover, backed by solid theoretical derivations. However, as a purely theoretical and formal verification study, it completely lacks empirical backtesting or real-world financial data validation.

Research Flowchart

  flowchart TD
    A["Research Goal: Formalize Simon's Bounded Rationality via Lean 4"] --> B["Input: Classical Expected Utility & Satisficing Concepts"]
    B --> C["Develop Flexible First-Order Stochastic Dominance (FFSD) Framework"]
    C --> D["Machine-Checked Verification in Lean 4 Theorem Prover"]
    D --> E1["Outcome 1: Unique Reference Point Threshold (ε < 1/2)"]
    D --> E2["Outcome 2: Equivalence Theorem to Expected Utility"]
    D --> E3["Outcome 3: Extension to Multi-Dimensional Settings"]