Erdős 883: an all-n first-question proof aligned with Lean

第一问 manuscript 与全 n 形式化；后续 Lean 补充含固定大小完全三部子图的渐近第二问与联合定理。

历史稿件、配套审计与研究说明按各自角色阅读；阶段与证据边界见交接说明。

为什么做

核对密集整数集的互素图是否包含规定的奇圈，并把有限范围和渐近构造连接到可检查的全 n 命题。

保存的原始陈述、公理及源码记录对应 6,831 个第一问模块和另 57 个第二问/联合模块；本次未重新运行 Lean。

形式化检查、数学优先权和外部认可属于不同问题。第一问继承 Della Pietra 渐近构造；第二问数学结果已有 Sárközy 1999 的先行工作。不能用定理名称或提交记录宣称历史首次、期刊接收或获奖。

从固定源码与原题量词开始独立重建，核对依赖缓存、显式原始陈述及归属；再让专家审查数学论证、历史范围和证书成本。

上述接续建议是待验证的研究问题，不是新增实验结果。原始稿件及来源、许可和阶段说明见归档。