标题： 量化有限理性：通过灵活随机优势对西蒙的满意化进行形式化验证 显示英文标题

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

摘要： 本文介绍了灵活的一阶随机优势（FFSD），这是一个数学严谨的框架，使用Lean 4定理证明器形式化了赫伯特·西蒙的有限理性概念。 我们开发了机器验证的证明，表明FFSD通过参数化容差阈值将经典期望效用理论与西蒙的满足行为联系起来。 我们的方法得出几个关键结果：(1) 一个临界阈值$\varepsilon < 1/2$，保证参考点的唯一性， (2) 一个等价定理将FFSD与近似指示函数的期望效用最大化联系起来，以及(3) 对多维决策设置的扩展。 通过在Lean 4的依赖类型理论中编码这些概念，我们提供了西蒙有限理性的第一个机器检查的形式化，为在认知限制下关于经济决策的机械化推理奠定了基础。 这项工作促进了形式数学与经济理论日益增长的交叉领域，展示了交互式定理证明如何推进我们对行为经济学概念的理解，这些概念传统上仅以定性方式表达。 显示英文摘要

摘要： 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.