v0.1.0：红蓝选择问题理由结构的 Lean4 形式化

本版本发布红蓝选择问题理由结构的 Lean4 形式化证明项目。

主要内容：

• 给出红蓝选择问题的 Lean4 基础定义；
• 建立统一理由框架，包括 Claim、Derivable、StrongReason、FinalReason 与 ReasonableStrategies；
• 形式化验证三个命题：
  • 个人收益优先下，Red 是任意玩家唯一的最终合理策略；
  • 集体福利优先且存在非空、未独自过半的蓝色锚点集合时，Blue 是任意玩家唯一的最终合理策略；
  • 集体福利优先、无自足理由、无外部锚点、无焦点下，任意玩家没有最终合理策略；
• 提供中文论文 PDF 与 LaTeX 源文件。

Lean4 验证命令：

lake build

论文位置：

paper/red_blue_choice_reason_structure.pdf

说明：本项目验证的是给定形式化定义下的三个命题，不声称解决一般理性选择理论。