n = 22 provedO=
Proven
- optimal
- exact
Citation record n-022
lowerBentz 2016, arXiv:1606.03746
Bounds
- Found by
- Wolfram Bentz 2018
- Construction
- hand
- Source
- [Kingbird]
- Evidence
E-kingbird-upper-register
5
- Proved by
- Wolfram Bentz 2016
- Kind
- unavoidable points
- Source
- [Bentz 2016]
- Evidence
E-bentz-2016-proof
0
Solved: the verified bounds meet.
Results in the register
T-007 V0 C1 Nagamochi · 2026-08-31 · 321 cases
for
T-058 V3 C3 wand125 after Tokoharu, Daniel · 2026-09-29 · 100 cases
Rectangle-certificate ceiling
α·UB(n)proved for ..100;B·UB(n)on 64 grid rowsT-083 V3 C3 Karakuş · 2026-10-02 · 301 cases
for every nonsquare
T-085 V3 C3 Karakuş; chelokot · 2026-10-02 · 315 cases
Nagamochi 2005, Lemma 1 is false for every container with and
upper: replayed here; lower: external proof (not read here)
—
not rigid, numerically checked, numerical multiprecision
Evidence: E-translation-escape-not-rigid
Scope
Square 17 of the retained witness (witness id 18) translates 1 along (0, 1) with the packing still valid, so the configuration admits a non-trivial feasible motion; 4 of its 22 squares do. Every constraint is exactly affine in the slide parameter, so the arithmetic carries no linearization error, but the coordinates are the witness's own finite-precision transcription: this settles the retained configuration, not the true optimum. Rigidity and optimality are independent, and this bears only on the former.
4 evidence entries
E-kingbird-upper-register, E-basic-grid-upper, E-nagamochi-lower, E-bentz-2016-proof
- [Kingbird] record catalogue
- [Bentz 2016] lower bound proof
- [Friedman DS7] survey
— solved
, proved by Wolfram Bentz (arXiv 2016; the catalogue dates the proof to
October 2018), together with . When this record was first written, on 22
August 2026, these were the most recent new exact values of proved for any
non-trivial case, and the lower-bound frontier had not moved since.
It has moved many times since then; STATUS.md lists every case solved
now. The verified lower bound rests on Bentz’s proof alone: nobody here has worked
through it, and no second route to has been replayed here.
What the paper contributes beyond two values
The 2016 paper is where the field’s own name for its method appears in print. Bentz states it plainly: optimality proofs for square packing use arguments based on resource starvation — subsets of the container are associated with numerical resources such that each packed box must consume a quantum, and the total available limits how many boxes fit.
That is the correct level of generality, and it organizes the entire lower-bound inventory as one idea being progressively de-discretised: points worth 1, points with a slider, segments measured by intersection length, weighted combinations, and finally the continuously varying families this paper introduces.
The open methodological question it raises
Bentz’s families reach an integer target (). Whether the same machinery can reach an irrational target of high degree — which is what would require — is, as far as this research found, untested. That question is the most useful single thing to know about the state of the lower-bound art, and it gates .
Verification Code
The programs behind this case’s verified bounds, by their evidence.
The code column says how the code that ran stands to the code its producer used.
VERIFIERS.md says what each program is and whose it is.
| bound | evidence | run | code | programs |
|---|---|---|---|---|
| verified lower | E-bentz-2016-proof |
a published proof | no code | no verification code |
| verified upper | E-basic-grid-upper |
replayed here | independent | V-check-basic-bounds (first-party) |