Een nieuwe, betere ondergrens voor n=17 vierkantpakking
Het doel is om een recent resultaat te verbeteren en aan te tonen dat $4,5058(?) \le s(17)$ met behulp van specifieke gewichten.
Definitie van $s(17)$
Om te beginnen definiëren we $s(17)$. Geciteerd uit een ouder artikel over dit onderwerp:
Laat $s(n)$ de zijde zijn van het kleinste vierkant waarin we $n$ eenheidsvierkanten kunnen passen (pakken).
- Voor $n=16$ is de beste oplossing overduidelijk een $4 \times 4$ array, dus $s(16)=4$.
- Voor $n=15$ kunnen de 15 eenheidsvierkanten overduidelijk worden omsloten door een $4 \times 4$ vierkant, dus $s(15) \le 4$. Het bewijzen dat dit het kleinste vierkant is, is echter minder triviaal. Erich Friedman bewees in 1999 dat $s(15)=4$.
- Voor $n=17$ is het voor de hand liggende omsluitende vierkant een $5 \times 5$, maar in 1998 vond John Bidwell een voorbeeld dat aantoont dat een vierkant van $4,6756\dots$ voldoende is, dus $s(17) \le 4,6756\dots$. Dit is een zeer interessante schikking van de vierkanten.
Aan de andere kant bewees Trevor Green in 2000 dat $4,4452\dots \le s(17)$. Hierdoor ontstond er een aanzienlijke kloof: $4,4452\dots \le s(17) \le 4,6756\dots$
Een paar weken geleden heeft Sam Burns, met behulp van ChatGPT 5.6 Sol, de ondergrens verbeterd(?). Deze nieuwe grens is nog niet door de gemeenschap beoordeeld. Na bestudering lijkt het correct, hoewel ik mogelijk een klein detail in het bewijs of het bijbehorende programma over het hoofd zie. Ik voeg daarom een vraagteken (?) toe aan het getal. De huidige stand van zaken is dus: $4,4452\dots \le 4,4811(?) \le s(17) \le 4,6756\dots$
Mijn belangrijkste bezwaar tegen het werk van Sam Burns is dat het een mooie grafische weergave verdiende. Naast het toevoegen van een grafiek heb ik enkele verbeteringen aan het programma aangebracht, waarmee ik een nieuwe ondergrens heb gevonden van $4,5058$. De reeks is nu: $4,4452\dots \le 4,4811(?) \le 4,5058(?) \le s(17) \le 4,6756\dots$
De technische details over het vinden van deze nieuwe grens worden besproken in een tweede bericht.
De ondergrens van Trevor Green
Het idee achter het oude bewijs van Trevor Green $(19+40\cdot\sqrt{2})/17 \cong 4,4452\dots \le s(17)$ is om 16 zeer interessante "onvermijdelijke" punten te kiezen in een vierkant met zijde $4,4452\dots$. Met behulp van meetkunde bewijst hij dat elk eenheidsvierkant ten minste één van deze punten moet bevatten. Als we proberen 17 eenheidsvierkanten in dit vlak te passen, moeten minstens twee eenheidsvierkanten één van de 16 interessante punten delen. De constructie kiest 16 punten uit een $4 \times 6$ raster.
Ik heb enkel een afbeelding van de punten gevonden in het oude artikel, maar niet de analytische definitie. Kijkend naar de formule voor de zijde van het vierkant, en gebruikmakend van een liniaal en wat gissen, vermoed ik dat de lege linker/rechter marge $0,5$ is en de lege boven/onder marge $\sqrt{2}-1/2 \cong 0,9142\dots$ Met deze keuzes heeft het diagonale segment in de originele grafiek een lengte van 1, wat zeer nuttig is voor het maken van driehoeken met hoekpunten die onvermijdelijke punten zijn.
De constructie gebruikt een $6 \times 4$ raster met een lege marge van $0,9142\dots$ en $0,5000$, waarbij de totale grootte van het raster $2,6168\dots$ bij $2,4452\dots$ is. Om deze constructie te vergelijken met nieuwere constructies, is het beter om deze te symmetriseren. In deze gesymmetriseerde versie bevat elk eenheidsvierkant ten minste 4 punten, hoewel sommige punten "dikker" zijn en tellen als dubbele punten.
De ondergrens van Sam Burns
De methode om $4,4811(?) \le s(17)$ te bewijzen, zoals gepost door Sam Burns via ChatGPT, kiest 268 interessante punten in een vierkant met zijde $4,4811$. De punten hebben verschillende gewichten, en het totale gewicht is slechts $16,9476$. Na enkele reducties is het voldoende om een eindig aantal richtingen te testen. Met een Python-programma worden alle mogelijke "bijna-eenheidsvierkanten" (eigenlijk $0,9973$) getest om te verifiëren dat de som van de gewichten binnen elk vierkant ten minste 1 is (eigenlijk $1,0003$). Als we 17 eenheidsvierkanten proberen te passen, moeten er dus minstens twee een van de 268 punten delen.
Deze methode heeft false negatives. Als het programma een oplossing verifieert, is deze zeker correct; maar als het programma faalt, is er een kleine kans dat dit een fout is. Dit is acceptabel om aan te tonen dat het gewicht een ondergrens bewijst.
Het is onduidelijk hoe de gewichten zijn geselecteerd. Vergeleken met voorbeelden in het oude artikel is de marge van $0,5$ te smal, aangezien de meeste voorbeelden $\sim 1,0$ of $\sim 9,1$ gebruiken. De gewichtselectie komt overeen met mijn eigen bevindingen, en alle gewichten in de eerste/laatste rij/kolom van het raster zijn nul. Naar mijn mening zouden de tweede en voorlaatste rij/kolom ook leeg moeten zijn, maar er is een niet-nul gewicht in $(1, 11)$ van het raster en de symmetrische beelden. De derde en voorlaatste rij/kolom zijn vrij vol. Dit ligt dichter bij de rand dan in de oude voorbeelden, wat suggereert dat het toevoegen van meer punten nabij de rand een goed idee is om de grens te verbeteren.
Ik teken de afbeeldingen met Racket en het Metapict-pakket. De straal van elke cirkel wordt berekend uit het gewicht als: $r = \sqrt{\text{gewicht}^{1/\gamma}} \cdot \text{schaal}$
Met $\gamma = 1,0$ is het oppervlak proportioneel aan het gewicht, maar kleine gewichten zijn dan te klein in de afbeelding. Met $\gamma = 2,0$ zijn de kleinere gewichten beter zichtbaar. Een schaal van $0,07$ ziet er goed uit op mijn machine. De cirkels zijn semi-transparant om overlap zichtbaar te maken. De code onderaan divideert het gewicht door $1,0003$, wat de werkelijke minimale som is.
De nieuwe ondergrens
Mijn idee was om verschillende combinaties van de marge en de interne rastergrootte te proberen. Omdat onduidelijk was hoe de gewichten bij Sam Burns waren geselecteerd, besloot ik voor elke vaste grootte lineaire programmering te gebruiken om deze te vinden.
Vervolgens gebruikte ik een combinatie van brute force zoeken en geluk om het beste raster te vinden. Daarna heb ik de gewichten afgerond zodat ze mooie breuken zijn.
Na veel tijd is het beste resultaat $4,5058(?) \le s(17)$. De nieuwe oplossing gebruikt 168 interessante punten in een vierkant met zijde $4,5058$ in een $29 \times 29$ raster. Deze punten hebben een totale som van slechts $16,9166\dots$. Elk eenheidsvierkant bevat een totaal gewicht van ten minste 1. Er is een lege marge van $0,77565$ en het interne raster heeft een totale zijde van $3,9545$.
De gewichten liggen dichter bij de rand dan ik op basis van oude voorbeelden verwachtte. Het gebruikt ook minder gewichten, waardoor ik hoop dat het makkelijker is om de correctheid zonder computer te bewijzen. Ik wil graag een niet-symmetrische versie maken, die mogelijk nog beter is.
Het programma van Sam Burns gaat uit van een lege marge van $0,5$, dus ik heb dit aangepast met een variabele $M$ (het dubbele van de marge). De versie met deze modificatie, de nieuwe maten en de nieuwe gewichtetabel staat onderaan. Het uitvoeren van dit programma bewijst(?) de nieuwe grens.
Conclusie en toekomstig werk
De distributies zien er in de hoeken vrij discreet uit, maar er zijn vreemde balken nabij het centrum. Het zou interessant zijn om de rastergrootte te vergroten. Ook lijken de smalle lege marges nuttig te zijn.
Mijn zoekprogramma is te traag (ongeveer 1 uur), dus ik heb de rastergrootte niet veranderd. Het zou nuttig kunnen zijn om andere rastergroottes te verkennen voor interessante covarianties. Het toevoegen van meer decimalen kost slechts enkele minuten, maar het verfijnen van het raster of het gebruiken van meer rotatierichtingen zou waarschijnlijk een grotere impact hebben.
Dit resultaat verbetert automatisch ook de ondergrens voor $s(18)$, $s(19)$ en $s(20)$. Een diepere zoektocht naar deze waarden zou echter nog betere grenzen moeten opleveren. Er is iets interessants aan het getal 18; ik heb te vaak gezien dat de totale som van het gewicht 18 is.
Ik wil een niet-symmetrische versie vinden. Ik heb een paar ideeën en hoop dat deze versie ongeveer $1/8$ van het gewicht heeft, bijna gelijkzijdige driehoeken laat zien en makkelijker te begrijpen is zonder computer.
***
Programma om de grens te verifiëren
from __future__ import annotations
from bisect import bisect_left, bisect_right
from fractions import Fraction as F
import numpy as np
# Original version posted by Sam Burns 2026
# Modified by Gustavo Massaccesi 2026
# Proposed exact lower-bound certificate for packing 17 unit squares in a square.
L = F(45058, 10000) # side of the square
M = F(15513, 10000) # both empty borders
B = F(9973, 10000)
T = F(207107, 500000)
KMAX = 180
D = T / KMAX
WEIGHT_SCALE = 576 # min weight
NGRID = 29
LAST = NGRID - 1
# (i, j, w): every distinct D4 image of grid point (i,j) receives weight w/WEIGHT_SCALE.
CERT = [
(0, 2, 165),
(0, 11, 129),
(1, 8, 36),
(1, 10, 21),
(1, 11, 15),
(2, 2, 246),
(2, 8, 129),
(2, 9, 105),
(2, 10, 36),
(2, 11, 105),
(5, 10, 36),
(6, 10, 63),
(6, 11, 12),
(7, 10, 21),
(8, 9, 33),
(8, 11, 15),
(9, 11, 75),
(9, 14, 39),
(10, 11, 25),
(10, 12, 21),
(10, 13, 24),
(10, 14, 3),
(11, 11, 16)
]
def orbit(i: int, j: int) -> set[tuple[int, int]]:
n = LAST
return {
(i, j), (n - i, j), (i, n - j), (n - i, n - j),
(j, i), (n - j, i), (j, n - i), (n - j, n - i),
}
def build_atoms() -> list[tuple[F, F, int]]:
step = (L - M) / LAST
coord = [M / 2 + step * i for i in range(NGRID)]
by_index: dict[tuple[int, int], int] = {}
for i, j, w in CERT:
for ij in orbit(i, j):
if ij in by_index:
raise ValueError(f"duplicate orbit assignment at {ij}")
by_index[ij] = w
return [
(coord[i], coord[j], w)
for (i, j), w in sorted(by_index.items())
]
def clip_u(
poly: list[tuple[F, F]],
bound: F,
keep_ge: bool,
) -> list[tuple[F, F]]:
if not poly:
return []
out: list[tuple[F, F]] = []
def inside(p: tuple[F, F]) -> bool:
return p[0] >= bound if keep_ge else p[0] <= bound
prev = poly[-1]
prev_in = inside(prev)
for cur in poly:
cur_in = inside(cur)
if cur_in != prev_in:
u1, v1 = prev
u2, v2 = cur
if u2 == u1:
v = v1
else:
lam = (bound - u1) / (u2 - u1)
v = v1 + lam * (v2 - v1)
out.append((bound, v))
if cur_in:
out.append(cur)
prev, prev_in = cur, cur_in
return out
def center_domain(c: F, s: F) -> list[tuple[F, F]]:
h = B * (c + s) / 2
lo, hi = h, L - h
corners_xy = [(lo, lo), (hi, lo), (hi, hi), (lo, hi)]
return [(c * x + s * y, -s * x + c * y) for x, y in corners_xy]
def verify_orientation(
c: F,
s: F,
atoms: list[tuple[F, F, int]],
) -> int:
half = B / 2
dom = center_domain(c, s)
u_dom_min = min(u for u, _ in dom)
u_dom_max = max(u for u, _ in dom)
v_dom_min = min(v for _, v in dom)
v_dom_max = max(v for _, v in dom)
rects: list[tuple[F, F, F, F, int]] = []
u_events = {u_dom_min, u_dom_max}
v_events = {v_dom_min, v_dom_max}
for x, y, w in atoms:
pu = c * x + s * y
pv = -s * x + c * y
u1, u2 = pu - half, pu + half
v1, v2 = pv - half, pv + half
rects.append((u1, u2, v1, v2, w))
u_events.add(u1)
u_events.add(u2)
v_events.add(v1)
v_events.add(v2)
ue = sorted(u_events)
ve = sorted(v_events)
ui = {x: i for i, x in enumerate(ue)}
vi = {x: i for i, x in enumerate(ve)}
diff = np.zeros((len(ue), len(ve)), dtype=np.int64)
for u1, u2, v1, v2, w in rects:
a, b = ui[u1], ui[u2]
p, q = vi[v1], vi[v2]
diff[a, p] += w
diff[b, p] -= w
diff[a, q] -= w
diff[b, q] += w
scores = diff.cumsum(axis=0).cumsum(axis=1)
nu, nv = len(ue) - 1, len(ve) - 1
best = 10**18
for i in range(nu):
u0, u1 = ue[i], ue[i + 1]
if u1 <= u_dom_min or u0 >= u_dom_max:
continue
slab = clip_u(dom, u0, True)
slab = clip_u(slab, u1, False)
if not slab:
continue
vlo = min(v for _, v in slab)
vhi = max(v for _, v in slab)
if vhi <= vlo:
continue
j0 = max(0, bisect_right(ve, vlo) - 1)
j1 = min(nv - 1, bisect_left(ve, vhi) - 1)
if j0 <= j1:
row_min = int(scores[i, j0:j1 + 1].min())
best = min(best, row_min)
if best == 10**18:
raise RuntimeError("center domain was not enumerated")
return best
def angle_net() -> list[tuple[F, F]]:
out: list[tuple[F, F]] = []
for k in range(KMAX + 1):
t = T * k / KMAX
den = 1 + t * t
c = (1 - t * t) / den
s = 2 * t / den
out.append((c, s))
return out
def main() -> None:
atoms = build_atoms()
total = sum(w for _, _, w in atoms)
print(f"atoms = {len(atoms)}")
print(f"total_weight = {total}/{WEIGHT_SCALE} = {total / WEIGHT_SCALE:.4f}")
assert total < 17 * WEIGHT_SCALE
net = angle_net()
contain = B * (1 + D)
print(f"angle_net_size = {len(net)}")
print(f"b*(1+d) = {contain} = {float(contain):.12f} < 1")
assert contain < 1
global_min = 10**18
argmin = -1
for k, (c, s) in enumerate(net):
m = verify_orientation(c, s, atoms)
if m < global_min:
global_min, argmin = m, k
if k % 30 == 0 or k == KMAX:
print(f"orientation {k:3d}/{KMAX}: min={m}/{WEIGHT_SCALE}, global={global_min}/{WEIGHT_SCALE}")
print(f"minimum_score = {global_min}/{WEIGHT_SCALE} = {global_min / WEIGHT_SCALE:.4f} at k={argmin}")
assert global_min >= WEIGHT_SCALE
print("CERTIFICATE CONDITIONS VERIFIED.")
print(f"By the scaling argument: s(17) >= {L} = {L:.4f}.")
if __name__ == "__main__":
main()Programma om de afbeeldingen te tekenen
#lang racket
(require racket/list)
(require metapict)
(define-syntax-rule (for/append clauses body ...)
(append* (for/list clauses (begin body ...))))
(define (mirror-x N atoms)
(for/append ([a (in-list atoms)])
(match a
[(list x y w)
(list (list x y w) (list (- N 1 x) y w))])) )
(define (mirror-y N atoms)
(for/append ([a (in-list atoms)])
(match a
[(list x y w)
(list (list x y w) (list x (- N 1 y) w))])) )
(define (mirror-d atoms)
(for/append ([a (in-list atoms)])
(match a
[(list x y w)
(list (list x y w) (list y x w))])) )
(define-values (L-Green atoms-Green)
(let ()
(define grid-nx 6)
(define grid-ny 4)
(define border-size-y (- (sqrt 2) 1/2))
(define grid-size-y (/ (+ 12 (sqrt 8)) 17))
(define border-size-x 1)
(define L (+ (* border-size-y 2) (* grid-size-y 3)))
(define grid-size-x (/ (- L (* border-size-x 2)) 5))
(define atoms/int '((0 3 1) (1 3 1) (3 3 1) (5 3 1)
(0 2 1) (2 2 1) (4 2 1) (5 2 1)
(0 1 1) (1 1 1) (3 1 1) (5 1 1)
(0 0 1) (2 0 1) (4 0 1) (5 0 1)))
(define min-weight 1)
(define atoms (for/list ([a (in-list atoms/int)])
(match a
[(list x y w)
(list (+ border-size-x (* grid-size-x x))
(+ border-size-y (* grid-size-y y))
(/ w min-weight))])) )
(values L atoms))))
(define-values (L-Green/S atoms-Green/S)
(let ()
(define grid-nx 6)
(define grid-ny 4)
(define border-size-y (- (sqrt 2) 1/2))
(define grid-size-y (/ (+ 12 (sqrt 8)) 17))
(define border-size-x 1)
(define L (+ (* border-size-y 2) (* grid-size-y (- grid-ny 1))))
(define grid-size-x (/ (- L (* border-size-x 2)) (- grid-nx 1)))
(define atoms/gen '((0 1 2) (1 1 1) (2 1 1)
(0 0 2) (1 0 1) (2 0 1)))
(define min-weight 4)
(define atoms/int (remove-duplicates
(mirror-x grid-nx
(mirror-y grid-ny
atoms/gen))))
(define atoms/one-dir (for/list ([a (in-list atoms/int)])
(match a
[(list x y w)
(list (+ border-size-x (* grid-size-x x))
(+ border-size-y (* grid-size-y y))
(/ w min-weight))])) )
(define atoms (mirror-d atoms/one-dir))
(values L atoms))))
(define-values (L-Burns atoms-Burns)
(let ()
(define grid-n 29)
(define L 44811/10000)
(define M 1)
(define grid-size (/ (- L M) grid-n))
(define border-size (/ M 2))
(define min-weight 10003)
(define atoms/gen '((1 11 107) (2 4 137) (2 9 214) (2 11 107) (2 12 137)
(3 4 3884) (3 7 214) (3 8 913) (3 9 214)
(3 10 214) (3 11 1234) (3 12 2189) (3 14 384)
(4 4 1961) (4 7 520) (4 8 214) (4 9 1413) (4 10 1234)
(4 11 1083) (4 13 137) (4 14 292)
(7 11 529) (7 12 33) (8 10 906) (8 11 384) (8 12 351)
(9 9 340) (9 10 180) (9 11 204) (9 12 549)
(10 12 879) (10 13 201) (10 14 378)
(11 11 396) (11 12 622) (11 13 204) (11 14 204)))
(define atoms/int (remove-duplicates
(mirror-x grid-n
(mirror-y grid-n
(mirror-d atoms/gen)))))
(define atoms (for/list ([a (in-list atoms/int)])
(match a
[(list x y w)
(list (+ border-size (* grid-size x))
(+ border-size (* grid-size y))
(/ w min-weight))])) )
(values L atoms))))
(define-values (L-Massaccesi atoms-Massaccesi)
(let ()
(define grid-n 29)
(define L 45058/10000)
(define M 15513/10000)
(define grid-size (/ (- L M) grid-n))
(define border-size (/ M 2))
(define min-weight 576)
(define atoms/gen '((0 2 165) (0 11 129) (1 8 36) (1 10 21) (1 11 15)
(2 2 246) (2 8 129) (2 9 105) (2 10 36) (2 11 105)
(5 10 36) (6 10 63) (6 11 12) (7 10 21)
(8 9 33) (8 11 15) (9 11 75) (9 14 39)
(10 11 25) (10 12 21) (10 13 24) (10 14 3) (11 11 16)))
(define atoms/int (remove-duplicates
(mirror-x grid-n
(mirror-y grid-n
(mirror-d atoms/gen)))))
(define atoms (for/list ([a (in-list atoms/int)])
(match a
[(list x y w)
(list (+ border-size (* grid-size x))
(+ border-size (* grid-size y))
(/ w min-weight))])) )
(values L atoms))))
(define (draw-example L atoms #:gamma [gamma 2.0] #:scale [scale 0.07])
[with-window (window -.1 (+ L .1) -.1 (+ L .1))
(define big-fill-color "whitesmoke")
(define big-border-color "black")
(define dots-color (change-alpha "darkred" 0.75))
(define big-square (curve (pt 0 0) -- (pt 0 L) -- (pt L L) -- (pt L 0) -- cycle))
(draw (color big-fill-color (fill big-square))
(penscale .1 (color big-border-color (draw big-square)))
(draw* (for/list ([a (in-list atoms)])
(match a
[(list x y w)
(define s (* (sqrt (expt w (/ 1. gamma))) scale))
(penstyle 'transparent (color dots-color (filldraw (circle (pt x y) s))))]))))])
(scale 4 (draw-example L-Green atoms-Green #:gamma 2.0 #:scale .07))
(scale 4 (draw-example L-Green/S atoms-Green/S #:gamma 2.0 #:scale .07))
(scale 4 (draw-example L-Burns atoms-Burns #:gamma 2.0 #:scale .07))
(scale 4 (draw-example L-Massaccesi atoms-Massaccesi #:gamma 2.0 #:scale .07))
Groetjes,