REVIEW 2 major objections 5 minor 4 references
New bounds for double covers of the discrete box {0,1,2}^d
T0 review · 2 major / 5 minor · reviewed 2026-07-13 · grok-4.5
Pith's one-line read Double covers of the discrete box {0,1,2}^d need more than 2^d boxes for d=4 and d=5, and at least 60 boxes when d=6.
desk verdict Solid first nontrivial lower bounds on double covers of {0,1,2}^d, settles the named question for d=4,5, and ships a Lean-checked f(6)≥60 with an improved constructive sandwich. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
Line rigidity: a two-dimensional crossing lemma on pair-only axis-lines that forces an inequality on the k-profile of any double cover of dimension 6, pushing the lower bound past the 57 ceiling that pure profile statistics cannot exceed.
What would settle it
An explicit double cover of {0,1,2}^6 that uses 59 or fewer proper sub-boxes, or a computer enumeration that produces a cover of {0,1,2}^3 with fewer than eleven boxes.
Extended reading notes
Core claim
The minimum size f(d) of a double cover of {0,1,2}^d satisfies f(4)≥19>2^4 and f(5)≥33>2^5, so the Leader–Milićević–Tan question holds for those dimensions; a line-rigidity argument further yields the unconditional, Lean-verified bound f(6)≥60, while new lifts give the matching sandwich 60≤f(6)≤81 and the asymptotic upper bound f(d)≤(8/7+o(1))2^d.
Load-bearing premise
The resolutions for dimensions 4 and 5 rest on the computer-verified base value that eleven is already the exact minimum for dimension 3; if that exhaustive search missed a smaller cover, those two corollaries would fall.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper studies f(d), the minimum number of proper sub-boxes of {0,1,2}^d that cover every point exactly twice. It proves the first nontrivial lower bounds: a modular refinement of the classical parity argument giving f(d) ≥ 2^{d+1}/(d+1); a slicing-plus-volume feasibility argument giving f(4) ≥ 19 and f(5) ≥ 33 (hence f(d) ≥ 2^d for d = 4, 5, the first cases beyond the trivial d ≤ 3); and a line-rigidity argument giving the unconditional bound f(6) ≥ 60, which exceeds the profile-statistic ceiling of 57 established in the paper. The f(6) ≥ 60 theorem is formalized in Lean 4 and depends only on the three standard Mathlib axioms. On the upper-bound side, a dimension-lifting “leapfrog” construction yields f(r+3) ≤ 6·2^r + 3f(r), hence f(6) ≤ 81 and the asymptotic f(d) ≤ (6/5 + o(1))2^d; a four-step refinement improves the constant to 8/7. The paper also isolates an S + c = 2^j + 1 wall for skeleton constructions and relates it to the Leader–Milićević–Tan question.
Significance. The work makes genuine progress on a clean open question of Leader–Milićević–Tan (restated as Question 4.1 of the PatternBoost paper): it settles the conjecture f(d) ≥ 2^d for d = 4 and d = 5, supplies the first lower bound for d = 6 that breaks the profile barrier, and improves both the concrete upper bound at d = 6 and the best asymptotic constant (from 1.28 down to 8/7). The machine-checked Lean formalization of f(6) ≥ 60, the explicit constructive lifts, and the clean isolation of the ABHK-derived construction wall are substantial strengths. The results are of clear interest in extremal combinatorics and discrete geometry, and the methodology (finite arithmetic reduced to omega, exhaustive base cases, formal verification) is reproducible and falsifiable.
major comments (2)
- The unconditional claim f(6) ≥ 60 rests on the Lean development of Section 10 (theorem f6_ge_60_unconditional). For a result whose novelty is partly the machine check, the formalization should be deposited in a public repository (with a fixed commit hash or DOI) and referenced from the paper so that referees and readers can rebuild it. The manuscript currently only describes the development; without the artifact the verification claim is not independently checkable from the text alone.
- Theorem 7.3 (four-step lift) and the associated (4,8,9) skeleton are only sketched: the 8-element word-set T ⊂ [3]^4, the 17-point hole-set, and the 9 masks are asserted to exist and to pass “finite checks,” but are not exhibited. Since this construction supplies the improved asymptotic constant 8/7 and the concrete bound f(9) ≤ 625, an explicit listing (or a short appendix/code pointer) is needed for the claim to be fully verifiable from the manuscript.
minor comments (5)
- Proposition 2.2 / Section 10: the base case f(3) ≥ 11 is an exhaustive integer-programming input used for the d = 4, 5 corollaries. A brief description of the encoding (variables, solver, and independent re-run) would help readers reproduce it; the paper already notes that only this base case is external to Lean.
- Lemma 5.1 proof sketch: the final sentence “R·S = 0 or (R, S ≤ 2 and A ≥ 2), so R·S ≤ 4 ≤ 2A” is slightly compressed; writing “hence R·S ≤ 4 and A ≥ 2, so R·S ≤ 2A” would make the arithmetic transparent without relying on the Lean decide.
- Appendix A table: the “rigidity” row for d ≥ 7 is the slicing bootstrap off f(6) ≥ 60; a footnote clarifying that these are not independent rigidity computations would avoid misreading.
- Notation: k(B) and the k-profile (x_0, …, x_d) are introduced cleanly, but the occasional use of “pair-only” without restating the 1-dimensional optimum (p_0, p_1, p_2, a_0, a_1, a_2) = (1,1,1,0,0,0) may slow a first reading of Section 5.
- References: the arXiv version of PatternBoost is cited; if a journal version has appeared by publication time it should be updated.
Circularity Check
No circularity: lower bounds are combinatorial inequalities and Lean-checked arithmetic; upper bounds are explicit constructive lifts; no fitted parameters or load-bearing self-citations.
full rationale
The derivation chain is self-contained and non-circular. The modular bound (Thm 3.1) refines the classical ABHK parity argument modulo 4 using only incidence counts over odd sub-boxes and the volume identity (Lemma 2.1). Slicing (Lemma 4.1 + convexity Lemma 4.2) bootstraps a lower bound L_{d-1} into a feasibility system on the k-profile; the d=4,5 resolutions take the independently verified computational input f(3)≥11 (exhaustive IP, matching published constructions of size 11) but do not redefine or fit to the target. Line rigidity (Thm 5.2) aggregates a 2-dimensional crossing lemma (Lemma 5.1, reduced to finite decidable cases) with volume and line counts into a single profile inequality whose omega-solved minimum is 60; the paper explicitly shows this exceeds the profile ceiling of 57 (Prop 6.1) and is machine-checked in Lean with only the three standard Mathlib axioms and no hypotheses. Upper bounds are dimension-lifting constructions (Thms 7.1, 7.3) that explicitly build covers of size 6·2^r + 3N or 8·2^r + 9N from a given cover of size N; they improve known constants without tautologically rewriting the conjecture. The S+c wall (Thm 8.1, Prop 8.2) is derived by applying the classical ABHK partition bound to support plus holes, not assumed. There are no self-citations of the author, no uniqueness theorems imported from prior work by the same author, no fitted parameters renamed as predictions, and no ansatz smuggled via citation. Base cases and the 2-d enumeration are external computational inputs kept outside the formal kernel. The paper is therefore free of the enumerated circularity patterns.
Assumptions & free parameters
assumptions (4)
- standard math Alon–Bohman–Holzman–Kleitman theorem: any partition of [3]^d into proper sub-boxes has size at least 2^d
- domain assumption f(3)≥11 (equivalently f(3)=11 with matching construction), established by exhaustive integer programming over proper sub-boxes
- standard math Lean/Mathlib kernel axioms propext, Classical.choice, Quot.sound
- standard math Volume identity: sum_j 2^{k(B_j)} = 2·3^d for any double cover
invented entities (2)
-
pair-only axis-lines and the crossing-rigidity invariant R·S≤2A on coordinate 2-planes
independent evidence
-
(j,S,c) skeleton constructions and the S+c=2^j+1 wall
independent evidence
Cite this review
Pith. "Pith review of New bounds for double covers of the discrete box {0,1,2}^d." pith.science (2026). https://pith.science/paper/KYH5E74E
@misc{pith2026260709014,
author = {Pith},
title = {Pith review of: New bounds for double covers of the discrete box 0,1,2^d},
year = {2026},
howpublished = {\url{https://pith.science/paper/KYH5E74E}},
note = {Machine review of arXiv:2607.09014}
}
abstract
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.
Reference graph
Works this paper leans on
-
[3]
Leader, L
I. Leader, L. Mili´ cevi´ c, and T. S. Tan,Decomposing the completer-graph, J. Combin. Theory Ser. A154 (2018), 21–31.(Question 4 of this paper poses the uniform-cover generalization of Question 1.2, of which the double cover is the case of covering multiplicity two.)
2018
-
[1]
N. Alon, T. Bohman, R. Holzman, and D. J. Kleitman,On partitions of discrete boxes, Discrete Math.257 (2002), 255–258
2002
-
[2]
M. Buci´ c, B. Lidick´ y, J. Long, and A. Z. Wagner,Partition problems in high dimensional boxes, J. Combin. Theory Ser. A166(2019), 315–336; arXiv:1805.11278
arXiv 2019
-
[4]
F. Charton, J. S. Ellenberg, A. Z. Wagner, and G. Williamson,PatternBoost: Constructions in Mathematics with a Little Help from AI, arXiv:2411.00566 (2024). Email address:p@pwhite.org
arXiv 2024
Reviewed July 13, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.