AI 中文总结
研究离散盒子{0,1,2}^d双覆盖最小规模\(f(d)\)，通过奇偶性、切片、线刚性论证得下界，维度提升构造得上界，解决\(d = 4,5\)问题，给出\(f(6)\)范围，分离构造障碍。
AI 中文摘要
集合\(A = \{0,1,2\}^d\)的一个真子盒子是一个乘积\(S_1\times\dots\times S_d\)，其中每个\(\varnothing\neq S_i\subsetneq\{0,1,2\}\)。双覆盖是一个有限多重集，由真子盒子组成，它恰好覆盖\(A\)的每个点两次；记\(f(d)\)为双覆盖的最小规模。Leader、Milicevic和Tan提出问题：对于所有\(d\)，是否有\(f(d)\geq 2^d\)。此前对于任何\(d\geq 2\)，所知结果都不比平凡的体积界更好。我们证明了第一个非平凡的下界。通过奇偶性论证的模块化细化得到\(f(d)\geq 2^{d + 1}/(d + 一 1)\)；切片论证得出\(f(4)\geq 19\)，\(f(5)\geq 33\)，解决了\(d = 4,5\)的问题。更精细的“线刚性”论证得出\(f(6)\geq 60\)。在给出上界方面，一个维度提升构造给出\(f(6)\leq 81\)且渐近地\(f(d)\leq(\frac{6}{5}+o(1))2^d\)。最后我们分离出构造方面的障碍——一种“S + c = 2^j + 1”现象。
英文摘要
A proper sub-box of $A=\{0,1,2\}^d$ is a product $S_1\times\dots\times S_d$ with each $\varnothing\neq S_i\subsetneq\{0,1,2\}$. A double cover is a finite multiset of proper sub-boxes covering every point of $A$ exactly twice; write $f(d)$ for the minimum size of a double cover. Leader, Milicevic and Tan asked whether $f(d)\ge 2^d$ for all $d$ (Question 4.1 of the PatternBoost paper of Charton-Ellenberg-Wagner-Williamson), analogous to the Alon-Bohman-Holzman-Kleitman partition bound $2^d$. No better than the trivial volume bound was previously known, for any $d\ge 2$. We prove the first nontrivial lower bounds. A modular refinement of the parity argument gives $f(d)\ge 2^{d+1}/(d+1)$; a slicing argument gives $f(4)\ge 19$, $f(5)\ge 33$, both above $2^d$, resolving the question for $d=4,5$ -- the first cases beyond the trivially known $d\le 3$. A finer "line rigidity" argument yields $f(6)\ge 60$, breaking the profile-statistic barrier (capped at $57$, shown here). This is formally verified in Lean 4: $f(6)\ge 60$ is machine-checked on the three standard Mathlib axioms alone. On the upper-bound side, a dimension-lifting construction $f(r+3)\le 6\cdot 2^r+3f(r)$ gives $f(6)\le 81$ (improving the known $82$) and $f(d)\le(\tfrac65+o(1))2^d$ asymptotically; a refinement improves the constant to $\tfrac87$. This makes partial progress on PatternBoost's problem of reducing their constant $1.28$, and refutes the closed-form guess $f(d)=5\cdot 2^{d-2}+1$ from $d=7$ on. Together, $60\le f(6)\le 81$. Finally we isolate the construction-side obstruction -- an "S+c=2^j+1" phenomenon, every skeleton sitting exactly one box past the partition bound -- and show it is of a piece with the Leader-Milicevic-Tan question itself.
Comments11 pages. The lower bound f(6)>=60 is formally verified in Lean 4 (Mathlib). Verification code and certificates: https://github.com/pw/box-double-covers
