Lean 中的十一方形堆积
完整的最优性证明通过了验证，并附有原生数值证书。已完成的EvolvingPrograms 验证运行接受了全部7,920 个本地 Lean 模块，其最终审计报告零。此仓库从提交1bf942a7af1ea330e95489d8997deebd4227ca71导入这些确切的证明源和固定构建配置。验证报告以获取证据和范围。
选定的高成本、精确数值证书检查使用native_decide。几何、检查器可靠性和证明组装保留普通的 Lean 证明。因此最终定理信任Lean 的内核和原生编译器；这不是仅内核验证的声明。已批准的数值声明及其精确源哈希记录在verification/native-certificates.json中。
最优边长为
[ T = \frac{6u+4}{1+2u-u^2}, ]
其中u是(9/25,37/100)中唯一的根
[ 5u^8-10u^7-2u^6+14u^5+12u^4-6u^3+2u^2+2u-1=0. ]
该构造达到约3.8770835900228141773。该模型允许任意朝向、合法的边界接触以及不相交的开内部。ElevenSquare/Optimality.lean中的公开声明以及完整的 T03 源代码树与此仓库之前的主分支相比未发生变化。
入口点
| 文件 | 用途 |
|---|---|
ElevenSquare/Foundations.lean |
几何、精确端点、达到最优的构造、闭胞覆盖以及有限情况归约。 |
ElevenSquare/Pending/ |
原始公开接口，现由集成证明完成。目录名称为历史遗留。 |
ElevenSquare/Interop/Wand125/ |
与所纳入的上游证书结果的联系。 |
ElevenSquare/Tasks/ |
几何论证、检查器、证书数据以及本地解析证明。 |
Sqpack/ |
纳入的证书检查器、生成的证明以及简化。 |
ElevenSquare/Optimality.lean |
无条件最优性以及边长下界定理。 |
ElevenSquare/Verification.lean |
针对公开证明目标的公理查询。 |
复现验证
该项目固定Lean 4.34.1以及 Mathlib 修订版d13f23b723b8a846827a245b89c10fc7d3f11612。保持lake-manifest.json不变。
在 Linux 上，使用 Python 3、Git、curl 和 tar：
bash scripts/run_verification.sh --bootstrap --jobs 2
在 macOS 上，首先安装elan启动器，然后使用相同的命令。当elan已安装时，引导程序可以准备固定的工具链和依赖缓存。根据机器选择合适的 worker 数量；模块按顺序编译。现有的有效回执可复用。添加--fresh以强制进行完整重放；Ctrl-C 可干净地停止运行器。
该命令检查每个本地模块，并执行最终的源、receipt、依赖和公理审计。要求OPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES，trust_model: lean_kernel_and_native_compiler零准入，以及
在最终结果中。仅达到 100% 的已编译模块是不够的。
python3 scripts/check_sources.py
仅源检查（不使用 Lean）为：手动工作流和 Ubuntu 说明也支持可恢复的验证。推送不会启动工作流。成功的源运行使用了 EvolvingPrograms 更大的 runner；它并不能确立冷构建运行时间或 2–3 小时的 macOS 保证。
不要在此快照上运行历史物化命令或verify.py --setup：它们会恢复已被取代的生成源。构建对象和日志应放在被忽略的.lake/和.verification/目录中。
致谢与来源
我们感谢EvolvingPrograms、@ctjlewis，以及每一位项目贡献者在形式化和验证工作上的付出。参见ACKNOWLEDGEMENTS.md了解个人和上游致谢，PROVENANCE.md了解源历史，以及integrations/wand125了解保留的声明。历史简化说明和部分审计记录被保留；其旧的未完成状态声明已被完成运行报告取代。