v0.1.2：Zenodo 归档版本

本版本用于 Zenodo 归档。内容与 v0.1.1 基本一致，包含 Lean4 形式化证明代码、中文论文 PDF、LaTeX 源文件、许可证与项目 README。

v0.1.1：补充许可证的发布版本

本版本在 v0.1.0 基础上补充项目许可证说明。

• Lean4 源代码采用 MIT License；
• 论文文本、图示与 PDF 采用 CC BY 4.0；
• README 中补充许可证信息。

项目内容与主要形式化结论保持不变。

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

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