T-004: Bentz 2010, Theorem 8 () is correct as printed, machine-audited in full
V3 C3 audit confirmed
Bentz 2010, Theorem 8: the printed 45-point unavoidable-set argument for is correct as printed, machine-audited in full.
Significance, composition and next rung
- Significance
- As far as the archived corpus shows, the first machine verification of a published unavoidable-set proof in this literature; the theorem is Bentz's, the audit is the contribution.
- Next rung
- V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained. A second independent mechanism, such as the pose-space interval audit generalized to Q(sqrt 2, sqrt 3) sides, would be shown beside the rung as a second machine method. Rung 5 needs a proof-assistant formalization reviewed by human experts.
- Novelty
- previously-published Present in an identified source
The case
Results on the case
8 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-008
Nagamochi · Nagamochi 2005 · source · register
2010-09-13 published T-004 this result
Bentz 2010, Theorem 8 () is correct as printed, machine-audited in full
V3 C3 audit confirmed
Bentz · Bentz 2010 · source · register
2010-09-13 published T-008
V3 C3 optimality confirmed
Bentz · Bentz 2010 · source · register
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-008
Karakuş · Karakuş 2026 · source · register
2026-09-30 published T-064
for every integer from 6 up; are the cases held here
V3 C3 optimality confirmed on this case, second certificate
Daniel after Burns, Massaccesi · evand square-packing 2026-10-01 · packet · packet · packet · packet · source 1 · source 2 · review 1 · review 2 · 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-004 in the results table
On GitHub, at main
- Register
- T-004 in
results.yaml, line 154 - Evidence
E-bentz46-theorem8-audit·E-bentz-2010-proof- Proofs and certificates
- certificate
verify_cover.py· proofbentz-2010-optimal-packings-13-and-46.pdf - Sources
- Bentz 2010 (its own site, retained copy)
- Artifacts
cases/bentz46/verify_cover.py·cases/bentz46/packing.py·tests/test_bentz46.py- Case file
frontier/n-046.md(verified lower, verified upper, reported lower, reported upper)