T-006:
V3 C3 optimality confirmed
(Bentz 2010, Theorem 9). Proved again, without cases, by Evan Daniel's weighted closed cover of [0,4]^2.
The second proof was kernel-checked in Lean 4 here on 30 September 2026: SquarePacking.s13_eq_4 : minSide 13 = 4, depending only on propext, Classical.choice and Quot.sound, built from the retained source with Mathlib's official cache. The cover's zero-margin property was also certified here by the source's zmx2 over every root of its D4 region.
The theorem is Bentz's. The case-free proof is Evan Daniel's, evand/square-packing, building on Burns's and Massaccesi's method, with an AI agent under human direction as his CREDITS.md says.
Significance, composition and next rung
- Significance
- A published exact value in the m^2 - 3 family; the score is the theorem's, not ours.
- Composition
- Two independent proofs of one value. Bentz's is compound, with Sections 3.1-3.2's case analysis read rather than machine-checked. Evan Daniel's case-free proof is complete as it stands: the Lean kernel checked s13_eq_4 from the definitions, including every one of the 209 cover chunks (E-n013-evand-casefree-cover-lean-kernel). A kernel check is machine evidence at V3: V5 also needs a human expert's review of the formalization, and the retained review of s13_eq_4 was written by an AI lane. The confirmation rung comes from the machine-method replay E-n013-evand-casefree-cover-zmx2-replay (C3); whether a kernel check itself counts toward C is the owner's open question.
- Next rung
- One named human expert's review of the formalization restores V5; C5 needs two, with the open-review pointer, beside the rebuild already done here. V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained. A second machine method on the same cover, for example a complete zeromargin.py sweep (1 h 42 min on 8 processes at the source) beside the zmx2 replay, would be shown beside the rung. Bentz's own route would reach C3 by machine-checking Sections 3.1-3.2's staged sets (typed on think-1o1f), which would also make it the second fully audited theorem of the paper.
- Novelty
- previously-published Present in an identified source
The case
Results on the case
7 results in the register on , oldest first, each with what it established and how it stands now.
2005 published T-007
for
V0 C1 lower bound incomplete on this case, superseded by T-006
Nagamochi · Nagamochi 2005 · source · register
2010-09-13 published T-006 this result
V3 C3 optimality confirmed
Bentz; Daniel after Burns, Massaccesi · Bentz 2010 · evand square-packing 2026-09-28 · packet · source 1 · source 2 · review · register
2026-08-31 established T-005
Bentz 2010, Lemma 10 is false as printed and true as corrected to
V3 C3 correction confirmed
2026-09-04 published T-085
Nagamochi 2005, Lemma 1 is false for every container with and
V3 C3 correction confirmed
Karakuş; chelokot · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register
2026-09-29 published T-058
Rectangle-certificate ceiling
α·UB(n)proved for ..100;B·UB(n)on 64 grid rowsV3 C3 method limit confirmed
wand125 after Tokoharu, Daniel · wand125 tools 2026 · packet · register
2026-09-29 published T-083
for every nonsquare
V3 C3 lower bound confirmed on this case, superseded by T-006
Karakuş · Karakuş 2026 · source · register
2026-10-07 published T-124
Reported non-strict local minima for 178 source configurations
V0 C0 restricted optimality recorded
Daniel after Couzo · Daniel exact and local reports 2026 · packet · register
Links
- On this site
- Case record, · Frontier row, · T-006 in the results table
On GitHub, at main
- Register
- T-006 in
results.yaml, line 241 - Evidence
E-bentz-2010-proof·E-bentz13-figure2-audit·E-n013-evand-casefree-cover-zmx2-replay·E-n013-evand-casefree-cover-lean-kernel- Proofs and certificates
- proof
bentz-2010-optimal-packings-13-and-46.pdf· certificateverify_cover.py· certificates13_closed_cover_4.txt.gz· proofLADDER.md· auditreview-2026-09-30-lean-s13.md - Sources
- Bentz 2010 (its own site, retained copy) · evand square-packing 2026-09-28
- Source packet
resources/web/evand-square-packing-2026-09-28/README.md- Artifacts
7 artifacts and controls
cases/bentz13/verify_cover.pyresources/papers/bentz-2010-optimal-packings-13-and-46.mdresources/web/evand-square-packing-2026-09-28/receipts/lean/axioms_s13.logresources/web/evand-square-packing-2026-09-28/receipts/lean/s13_table.txtresources/web/evand-square-packing-2026-09-28/receipts/s13_zmx2_d4.logdocs/project/reviews/review-2026-09-30-lean-s13.mdtests/test_evand_mixed_covers.py- Case file
frontier/n-013.md(verified lower, verified upper, reported lower, reported upper)