T-087: and , by optimal piercing
V3 C1 lower bound reviewed superseded by T-063 and T-069
Bašić and Slivková 2018, Theorem 7 with Proposition 8: no more than B(x) unit squares fit in a square of side x, where B(x) counts the points of an equilateral-lattice piercing set, floor(x)(m + 2) plus floor((m + 2)/2) when frac(x) >= 1/2, with m = floor((2/sqrt 3)(x + 1 - 2 sqrt 2)). Just below 7 sqrt(3)/2 + 2 sqrt(2) - 1 it is 60, so sqrt(3)/2 + 2 sqrt(2) - 1, about 7.8906 (their Theorem 10); just below 5 sqrt(3)/2 + 2 sqrt(2) - 1 it is 36, so sqrt(3)/2 + 2 sqrt(2) - 1, about 6.1586, which the paper does not state.
Both are above Karakuş's general floor, T-083; at every other case the theorem is weaker than the verified floor already held. The proof uses nothing of Nagamochi 2005. It was read and re-derived here and is not machine-checked; its arithmetic is replayed exactly for every case by devtools/check_piercing_lower_bounds.py. Bašić and Slivková, Discrete Applied Mathematics 247 (2018).
Significance, composition and next rung
- Significance
- Registered as the verified lower bound at and , the only two cases where the piercing bound beat the floor its line of the register held; the merge of 3 October 2026 brought stronger replayed bounds to both, so it holds neither now. S3 by the anchor "a substantive case result or machine audit"; the score is the theorem's, not ours.
- Next rung
- C2 and above need a replay of the geometry, not only the arithmetic: a machine check that the lattice of Theorem 7 pierces every unit square in the square of side x, or a formalization of the three-case reduction in Theorem 3's proof.
- Unfinished confirmations
- C2: a replay of the geometry: a machine check that the lattice of Theorem 7 pierces every unit square in the square of side x, or a formalization of the three-case reduction in Theorem 3's proof. Not priced.
- Novelty
- previously-published Present in an identified source
The cases
Proven
- exact
Citation record n-037
lowerwand125 after Tokoharu, Levy et al. 2026, GitHub (confirmed T-069)
upperCantrell 2002, Squares in Squares (confirmed T-101)
Open
- optimality
The case record
Results on these cases
12 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 these cases, superseded by T-063 and T-069
Nagamochi · Nagamochi 2005 · source · register
2018 published T-087 this result ·
and , by optimal piercing
V3 C1 lower bound reviewed superseded by T-063 and T-069
Bašić, Slivková · Basic-Slivkova 2018 · 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-27 published T-045 ·
Rectangle-density lower bounds replayed at 15 counts in
V3 C3 lower bound confirmed superseded by T-063
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · packet · packet · source · review · register
2026-09-27 published T-046 ·
Rectangle-density lower bounds reported for 48 counts in
V0 C0 lower bound recorded superseded by T-063 and T-069
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · wand125 rectangle bounds 2026-09-28 · packet · packet · register
2026-09-28 published T-063 ·
, by monotonicity from T-062
V3 C3 optimality confirmed
Daniel after Burns, Massaccesi · evand square-packing 2026-10-01 · packet · packet · packet · source 1 · source 2 · review 1 · review 2 · 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 these cases, superseded by T-063 and T-069
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 these cases, 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-01 published T-069 ·
Mixed rectangle-measure lower bounds replayed at
V3 C3 lower bound confirmed
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds 2026-10-01 · packet · source · review · register
2026-10-05 published T-101 ·
Exact certificates of 77 catalogue packings:
s(n) ≤ S',1.2e-16to9.8e-15above each sideV3 C3 upper bound confirmed
Daniel after Couzo, de Winter, Ellsworth, Levy · evand exact optima 2026-10-05 · packet · 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, · Case record, · Frontier row, · T-087 in the results table
On GitHub, at main
- Register
- T-087 in
results.yaml, line 8430 - Evidence
E-basic-slivkova-piercing-lower- Proofs and certificates
- proof
basic-slivkova-2018-optimal-piercing-square.pdf - Sources
- Basic-Slivkova 2018 (its own site, retained copy)
- Artifacts
resources/papers/basic-slivkova-2018-optimal-piercing-square.pdf·devtools/check_piercing_lower_bounds.py·campaign/series/series-000-smoke-and-calibration/results/piercing-lower-bounds.json·tests/test_piercing_lower_bounds.py- Case file
frontier/n-037.md(verified lower, verified upper, reported lower, reported upper) ·frontier/n-061.md(verified lower, verified upper, reported lower, reported upper)