# P95 前七个实例的全局最优推导

## 1 问题与结论

记 `D_k` 为边长 `2k` 与 `k` 的闭矩形。所有矩形可以独立平移、以任意实数角度旋转；要求位于边长为 S 的闭正方形内，内部两两不交，允许接触。记最小可行边长为 `S*(n)`。

本包证明：

`S*(1),…,S*(7) = 2,4,6,8,11,14,17`。

证明分成两部分：七个完整、精确可行构造给出上界；前四例用单块投影给出同值下界，后三例用连续角度区间树及近轴解析引理给出同值严格下界。严格排除 `S<T`，而不是排除 `S≤T`，才能与边长恰好 T 的可行构造相容。

## 2 前四例的解析下界

最大矩形 `D_n` 在角度 θ 下的水平、竖直投影长分别是

`n(2|cos θ|+|sin θ|)`，`n(2|sin θ|+|cos θ|)`。

利用正方形的反射和四分之一转对称性，可以令 `0≤θ≤π/4`。较大投影为 `n f(θ)`，其中 `f(θ)=2cos θ+sin θ`。在该区间，`f''=-f<0`，所以 f 是凹函数，其最小值位于端点。端点值是 `2` 与 `3/√2>2`，故任何容纳 `D_n` 的正方形都有 `S≥2n`。这不依赖坐标为整数，也不要求矩形轴对齐。

`witnesses/n01.json` 至 `n04.json` 分别在 `S=2,4,6,8` 给出完整构造。逐顶点包含性和逐对分离轴精确检验通过，因此前四个等式成立。

作为额外的一致性检查，面积给出

`S² ≥ Σ(k=1,…,n) 2k² = n(n+1)(2n+1)/3`。

本包没有对任意角情形把面积平方根向上取整；这种取整本身不能作为连续问题的下界。

## 3 后三例只需排除三个最大矩形

对 n=5、6、7，取 `p=n−2`，子集为 `D_p,D_(p+1),D_(p+2)`，目标 `T=3p+2`，即 11、14、17。若这个子集在 `S<T` 时已不可能放入，则完整 n 块也不可能。另一方面，上界必须验证完整 n 块；本包的七个见证均为完整实例。

用长轴方向描述每块矩形，角度模 π。设

`t=tan(θ/2)`，`c(t)=(1−t²)/(1+t²)`，`s(t)=2t/(1+t²)`。

每个方向都能表示为 `−π/2≤θ≤π/2`，即 `−1≤t≤1`。通过正方形 D4 对称性，将第三块长轴折叠到 `0≤θ_3≤π/4`。相应半角参数属于 `[0,√2−1]`，证书使用更大的有理区间 `[0,1/2]`，因此只会扩大可行域，不会漏掉任何实际摆放。再作必要的半周转动，可以令第三块中心的水平坐标位于正方形中心左侧，且各长轴模 π 方向不变。

中心以正方形中心为原点，记 `z=(x_1,y_1,x_2,y_2,x_3,y_3)`。完整根角度盒为

`[-1,1] × [-1,1] × [0,1/2]`，另有 `x_3≤0`。

两个凸矩形内部不交，当且仅当存在沿其中一块边法向的分离轴，使两个闭投影区间不发生内部重叠。每对矩形有“轴属于哪块、长轴或短轴、正负号”共 8 个有向选择。三对的所有 `8³=512` 个选择都在根节点中列入。边界接触用非严格分离不等式保留。

## 4 整个角度盒上的精确几何界

当 `t∈[a,b]⊆[-1,1]` 时，s(t) 单调递增，c(t) 随 |t| 增大而递减。因此两者的范围由有理端点值和区间是否包含 0 精确确定。

对正数 A、B，考虑

`f(δ)=A|cos δ|+B|sin δ|`。

每个开象限内 `f''=-f<0`，故角度区间上的最小值只能出现在区间端点，或其中跨过的 `π/2` 整数倍。差角 `δ=θ_i−θ_j` 的端点由 `(t_i.low,t_j.high)` 与 `(t_i.high,t_j.low)` 给出，其正弦余弦仍为有理数；跨象限轴的判定可由半角参数顺序及这些端点正弦、余弦的符号完成。所以校验器无需调用浮点三角函数，就能获得支持函数的精确最小值。

`D_k` 的水平、竖直半投影长分别是

`h_x=k|cos θ|+(k/2)|sin θ|`，

`h_y=(k/2)|cos θ|+k|sin θ|`。

记它们在角度盒上的下界为 `h̲_x,h̲_y`。若任一半投影下界大于 `T/2`，该角度盒中的矩形不可能放入目标正方形，可整盒排除。否则中心坐标必须满足

`−(T/2−h̲_a) ≤ z_a ≤ T/2−h̲_a`。

第三块水平坐标的上界还可以收紧到 0。这些中心盒只用于必要条件；所有不确定性都向扩大可行域的一侧处理。

选定分离法向 q 时，其所属矩形在该方向的支持半径恰为 k 或 k/2；另一块支持半径是上面的 f(差角)。正负法向的支持半径相同。由此得到分离行的系数区间与右端上界。若整个盒上允许的最大投影中心距离仍小于支持半径和的下界，则该有向分离选择在整个盒上都不可能。

## 5 带残差的有理区间矛盾

固定某个角度盒和三对分离选择。必要不等式可以写为

`A(θ)z ≤ b(θ)`。

它们包含 12 个墙约束、`x_3≤0`，以及 3 个有向分离约束。证书为某些分离组合提供非负有理乘子 `μ≥0`。校验器逐一检查乘子非负并重新计算

`r(θ)=μᵀA(θ)`，`β(θ)=μᵀb(θ)`。

不要求 r 在角度盒中恒为零。分别用有理区间 `R_a` 包住每个残差系数，用 B 包住 β 的上界，用 `Z_a` 包住每个可行中心坐标。于是所有可行点都必须满足

`Σ_a min(R_a Z_a) ≤ r(θ)·z ≤ β(θ) ≤ B`。

如果精确算出

`B−Σ_a min(R_a Z_a)<0`，

就得到矛盾。区间乘积取四个端点乘积的最小值，没有浮点舍入容差。证书中记录的负上界也会与重算结果比较；只提供“求解器不可行”状态或中点对偶不能通过这一检验。

## 6 近轴解析引理

以下引理只在靠近轴对齐的角度盒使用，它本身不是全角度证明。

令 `p∈{3,4,5}`、`m=p+2`、`T=3p+2`、`η=1/100`。设 `D_p` 的长轴为 `π/2+a`（模 π），`D_m` 的长轴为 b，且 `|a|,|b|≤η`。则这两块矩形不可能在 `S<T` 的正方形中内部不交。

证明如下。记 `u=|a|`、`v=|b|`、`W=u+v`、`R=u²+v²`、`w=|a−b|≤W`。两块矩形水平和竖直半投影之和为

`X=p|sin a|+(p/2)cos a+m cos b+(m/2)|sin b|`，

`Y=p cos a+(p/2)|sin a|+m|sin b|+(m/2)cos b`。

写成 `X=X₀+X₁+E_x`、`Y=Y₀+Y₁+E_y`，其中

`X₀=3p/2+2`，`X₁=p u+(m/2)v`，

`Y₀=3p/2+1=T/2`，`Y₁=(p/2)u+m v`。

由 `|sin x−x|≤|x|³/6` 和 `0≤1−cos x≤x²/2`，统一得到

`|E_x|≤(p/6)u³+(p/4)u²+(m/2)v²+(m/12)v³≤4R`，

`|E_y|≤(p/2)u²+(p/12)u³+(m/4)v²+(m/6)v³≤4R`。

同时 `R≤ηW`、`X₁≤5W`、`Y₁≤7W`。若任何单块中心盒为空，则已无法容纳；否则对任意单位法向 q，单块包含性所允许的最大中心投影距离为

`|q_x|(S−X)+|q_y|(S−Y)`。

先考虑两个近竖直法向，它们的偏角分别是 r=a 或 r=b。令 `A₀=T−X₀=3p/2`，在边长 T 处，最大投影距离是

`M_r=(T−X)|sin r|+(T−Y)cos r`

`   =Y₀+A₀|r|−Y₁+E_M`。

精确余项表达式为

`E_M=(A₀−X₁−E_x)(|sin r|−|r|)−(X₁+E_x)|r|`

`    +(Y₀−Y₁−E_y)(cos r−1)−E_y`。

利用 `|A₀−X₁−E_x|<8`、`|Y₀−Y₁−E_y|<9`，四项绝对值之和不超过

`[(27/2)η+(16/3)η²]W < 14ηW`。

对应的投影支持半径和为

`Q_b=m/2+p cos(a−b)+(p/2)|sin(a−b)|=Y₀+(p/2)w+E_b`，

`Q_a=p+(m/2)cos(a−b)+m|sin(a−b)|=Y₀+m w+E_a`。

余项满足 `|E_b|,|E_a|≤3w²≤6ηW`，故每个投影间隙 `M−Q` 的总误差至多 `20ηW=W/5`。两个间隙的一次项分别为

`L_b=−(p/2)u+(p/2−2)v−(p/2)w`，

`L_a=p u−(p+2)(v+w)`。

三角不等式给出 `u+w≥v` 和 `v+w≥u`。当 p=3，`L_b≤−W/2`。当 p=4，`L_b=−2(u+w)≤−W`。当 p=5，若 u≥v，则 `L_b≤−(5/2)u+(1/2)v≤−2u≤−W`；若 v≥u，则 `u+w≥v` 给出 `L_b≤−2v≤−W`。对所有 p，若 u≥v，则 `L_a≤−2u≤−W`；若 v≥u，则 `L_a≤p u−(p+2)v≤−W`。

所以 W>0 时，两个近竖直间隙均严格为负。W=0 时，在 S=T 处它们等于 0；把边长降到 S<T，会再减去 `(T−S)(cos r+|sin r|)>0`，于是同样严格为负。

剩下两个近水平法向。由 `X≤X₀+5W+4R≤X₀+0.1008` 和 `A₀≥4.5`，有 `T−X>0`。最大中心投影距离至多

`A₀+(X₀/2)η²+Tη`。

两个支持半径和分别至少为 `X₀−pη²` 与 `X₀−2mη²`。利用 `T≤17`、`X₀≤19/2`、`m≤7`，两个间隙都不超过

`−2+17η+(75/4)η²=−1.828125<0`。

法向反号不改变最大中心距离和支持半径和，故四个轴的所有正负选择均已排除。引理得证。

证书中的充分半角条件是

`0≤t_m≤1/200` 且 `|t_p|≥199/201`。

因为 `2 arctan(1/200)≤1/100`，而靠近竖直轴的偏角半角正切等于 `(1−|t_p|)/(1+|t_p|)≤1/200`，这些有理端点保证引理的角度假设。n=5 的冻结校验器使用同一引理的 p=3 专门版本，误差界更紧；原文及其固定哈希随包提供。n=6、7 使用上面的统一版本。

## 7 完整树如何覆盖连续角度

每个节点继承父节点的闭角度盒和尚未排除的全部分离组合。可采用的结束方式只有三种：整盒墙约束矛盾；满足第 6 节近轴引理；或通过逐对整盒排除与有理区间对偶矛盾排除全部继承组合。

若仍有未排除组合，就必须选择某个坐标区间内的严格内部有理分点，把父盒分成两个闭子盒。两个子盒覆盖父盒，公共边界也保留；所有剩余分离组合原样传给两边。证书按前序遍历记录，校验器维护待处理栈，逐一核对节点编号、继承分支数、子盒与终止记录。

只有根域的全部分支都被处理、待处理栈为空、证书声明完整且没有多余记录，才通过全局检验。超时、截断文件、缺少一个子树或仅证明某个自定义角度盒，都不能推出全局下界。

本包三棵完整树分别有 1409、1927、2431 个节点；重放分别检查 11184、16068、20118 个有理对偶矛盾，以及 16、16、19 个近轴解析叶。三棵树给出 `S<11`、`S<14`、`S<17` 时相应三块子集不可能共存。

## 8 完整见证与上下界闭合

见证中第 k 项代表 `D_k`，`rotated=false` 时局部边为 `(2k,k)`，`rotated=true` 时为 `(k,2k)`。`x,y` 是局部左下顶点及附加旋转的支点，不是旋转后包围盒的左下角；`turn` 是半角参数 t。全部十进制字符串都作为有理数读取，再用第 3 节的公式构造四个顶点。

独立验证器明确指定 `expected_n=n`，拒绝缺块、重复键、非法字段、非法小数或越界顶点。对每一对矩形，使用四个候选分离轴的精确点积区间检查内部不交；等号允许接触，不设几何 epsilon。

七个完整见证分别在目标边长 2、4、6、8、11、14、17 通过检验，因此 `S*(n)≤T`。第 2 节和第 7 节分别给出对应的 `S*(n)≥T`。上下界相等，故七个值都是任意实数角度、任意实数边长模型中的全局最优值。

## 9 复核的边界

Python 校验器不导入证书生成器，不使用浮点线性规划状态作为证明。证书内算术与覆盖关系全部精确重放；支持函数凹性、分离轴定理和近轴余项估计仍属于需要阅读审查的数学部分，并非证明助手已形式化的定理。哈希链固定当前包的内容，不能替代对数学论证与校验代码的审阅。