| n | 最优边长（精确） | 构型发现 | 最优性证明 |
|---|---|---|---|
| 5 | 11 | Erich Friedman · 1998 | zzzcy #308 · 2026 |
| 6 | 14 | Erich Friedman · 1998 | zzzcy #308 · 2026 |
| 7 | 17 | Erich Friedman · 1998 | zzzcy #308 · 2026 |
Friedman 的表早已列出这三个构型及其数值。本次采纳的是不能再缩小容器的证明，不是新的数值纪录。n = 1–4 的最优值 2、4、6、8 本站已有初等证明，投稿也作了复核；n ≥ 8 不在本次结论内。
证明方法
对 n = 5、6、7，只需证明最大的三块矩形不能装入边长小于目标值的正方形。令 p = n−2，三块为 p、p+1、p+2，目标边长为 T = 3p+2。上界另由包含全部 n 块的精确构型给出。
用 t = tan(θ/2) 表示长轴角度，则 cos θ = (1−t²)/(1+t²)、sin θ = 2t/(1+t²)。经正方形对称归约，完整根域为 [−1,1] × [−1,1] × [0,1/2]，第三块中心可取在左半平面。每对矩形有 8 个有向分离轴选择，根节点覆盖全部 512 种组合。
在每个角度区间上，以有理数计算墙约束、支持函数和分离轴约束的保守界。非负对偶乘子及残差区间给出严格矛盾；尚未排除的分支必须传到覆盖父区间的两个子节点。所有计算使用精确分数，既没有角度网格，也没有浮点容差。
靠近轴对齐的少数区间使用解析引理：当 p 块近竖直、p+2 块近水平，两个偏角的绝对值均不超过 1/100 弧度时，它们不能在 S < 3p+2 的正方形中共存。Taylor 余项不超过两个偏角绝对值之和的 1/5，严格小于分离间隙的一次项损失；偏角均为零时由 S < T 给出严格矛盾。引理只覆盖近轴区域，其余角度由完整证书树排除。
因此下界严格排除 S < T，完整构型在 S = T 取等，合起来得到连续全局最优。见证为整数坐标且无需附加旋转，所以也精确满足本站九位小数提交格式。
复核与附件
极值竞技场审阅了解析推导与校验代码，运行原包完整入口，并另外编写不导入投稿代码的校验器。三棵树共 5,767 个节点、47,370 条精确对偶矛盾、51 个近轴解析叶，两份重放均通过。七个完整构型全部通过本站现有验证器；删节点、复制节点、清零乘子与伪造近轴叶的四个破坏样本均被独立校验器拒绝。
这是经过审查的计算机辅助数学证明，不是 Lean 或 Coq 形式化证明。分离轴定理与近轴解析引理仍是人工审阅的数学部分。
SHA-256: 25237c2a5a8ec4754d4c63c81a178abed4c839363db819dd96db9eac443757bd
解压原包，在其目录中运行普通 Python 3.8 或更高版本，不要使用 -O 或 -OO：
python -B verify_all.py将本站校验器与 ZIP 放在同一目录后，可独立重放：
python -B independent-checker.py p95-n1-n7-proof.zip audit.json构型来源：Erich Friedman · Consecutive Dominoes in Squares
zzzcy 获一次 +2 证明分。n = 5–7 按现有“已证明最优”机制归档，保留历史提交与纪录持有人；证明附件不替换玩家纪录。n ≥ 8 继续竞赛。