n = 5 · Case Records · The Squares Project

n = 5 provedO=R

$s (5) = 2 + \frac{1}{2} \sqrt{2}$

The best packing known for 5 squares, side

2 + \frac{1}{2} \sqrt{2}

, Frits Göbel 1979

2.707

234

2.2363.236

\sqrt{n}

\sqrt{n} + 1

Proven

$s (5) = 2.707107$

optimal
exact
rigid

Citation record n-005

lowerGöbel 1979, Math. Centre Tracts 106

upperGöbel 1979, Squares in Squares

Bounds

Best known packing

$2 + \frac{1}{2} \sqrt{2}$

2.70710678118654

Found by: Frits Göbel 1979
Construction: hand, catalogue rigid
Tilt angles: $0^{\circ}$ , $45^{\circ}$
Source: [Kingbird]
Evidence: E-kingbird-upper-register, E-n005-gobel-upper

Verified upper bound

$2 + \frac{1}{2} \sqrt{2}$

2.70710678118654752440084436210485

The reported value, verified here.

Evidence: E-n005-gobel-upper

Reported lower bound

2.70710678…

2.707106781187

Proved by: Frits Göbel 1979
Kind: unavoidable points
Source: [Friedman DS7]
Evidence: E-n005-gobel-proof

Verified lower bound

$2 + \frac{1}{2} \sqrt{2}$

2.70710678118654752440084436210485

The reported value, verified here.

Evidence: E-n005-gobel-proof

Gap

Solved: the verified bounds meet.

Results in the register

T-007 V0 C1 Nagamochi · 2026-08-31 · 321 cases
$s (n) \geq min (⌈ \sqrt{n} ⌉, \sqrt{n - 2 ⌊ \sqrt{n} ⌋ + 1} + 1)$ for $4 \leq n \leq 324$
T-012 V3 C3 Levy · 2026-08-31 · n = 5
Goebel's $n = 5$ packing is second-order rigid at fixed side
Claim and records
Claim
Goebel's $n = 5$ optimal packing is not infinitesimally rigid but is second-order rigid at fixed side: the cone of infinitesimal motions is exactly the middle square's rotation about its own centre, and that one direction is refused at second order by a verified non-negative self-stress, all exactly over Q(sqrt 2).
Next rung
Local rigidity is discharged, not open: X-007's curve-selection argument was written out in full as X-012, checked against a complete exact accounting of the 400 local inequalities, independently reviewed by BC-153 and registered as T-014, which is where the $n = 5$ frontier property now rests. What remains here is the review record: two adversarial AI reviews and a human oversight record for rung 4, and for rung 5 a proof-assistant formalization reviewed by human experts.
Significance
A structural theorem at the smallest nontrivial case, proved exactly where the catalogue asserts 'Rigid.' with no definition or argument and the corpus contains none of the machinery for deciding it.
Novelty
apparently-novel Not found in the recorded search, subject to its stated gaps
Records
n = 5 register evidence 1
n = 5 register evidence 1
T-014 V3 C3 Levy · 2026-09-03 · n = 5
Goebel's $n = 5$ optimum is rigid at fixed side: its pose is an isolated feasible point
Claim and records
Claim
For s = 2 + sqrt(2)/2 and Goebel's labeled pose P0 in C = (R^2 x S^1)^5, P0 is an isolated point of Feas(s) -- closed unit squares in [0, s]^2, pairwise disjoint interiors -- equivalently there is no nonconstant continuous feasible path from P0 and no sequence of distinct feasible poses converging to it; hence the $n = 5$ optimum is rigid at fixed side in the catalogue's sense.

Proved exactly over Q(sqrt 2) in one intrinsic half-angle chart, from a complete exact accounting of all 400 elementary inequalities, by semialgebraic curve selection on the punctured feasible set and an induction on a putative arc's Taylor coefficients through order 2m that T-012's non-negative self-stress contradicts.
Composition
Compound, and the minimum is set by the part no machine checks. The exact local system -- the injective chart, all 400 base margins, the 20 active rows, the 128 strict conditions that cut out the neighbourhood, T-012's first-order cone and its non-negative self-stress with w . q < 0 -- is machine-confirmed here with the producer's code, devtools.assess_n5_rigidity, and independently rebuilt by the reviewer (machine-checked fragments, replayed here).

The two steps that close the argument, the cited Nash curve-selection lemma and the order-2m coefficient induction, are an audited proof rather than a computation, and no instrument decides isolation, so the whole claim declares V3.

Confirmation is C3: every exact quantity the proof consumes carries a certificate and a passing replay in this repository, and no cited part rests on anything weaker. BC-153's independent review of the proof is retained and mapped; it is one adversarial AI review, by a reviewer whose model is unstated, and not a human oversight record.
Next rung
V4 needs the closing steps mechanised, rather than only the quantities they consume, and with C4 a second adversarial AI review by a distinct reviewer and a human oversight record. BC-153's review, installed as a mapped review document on 2026-09-03, is the one retained; the round record carries it as an amendment as well. Rung 5 needs a proof-assistant formalization reviewed by human experts. Reaching the printed BCR page, or citing the Basu-Pollack-Roy plus Puiseux derivation the review writes out, would close the one cited hypothesis this rests on.
Significance
The first exact proof of fixed-side local rigidity of Goebel's $n = 5$ optimum -- a property Kingbird asserts with no argument, Goebel does not state, and Friedman does not annotate -- at the smallest case where tilting beats the grid. A case result, S3 rather than S4: the closing principle is the classical second-order sufficient optimality condition and the induction has the shape of Connelly-Whiteley 1996 Theorem 4.3.1, neither claimed as new; what is new is the exact accounting that reduces the local feasible set to twenty inequalities on an explicit neighbourhood, which is what lets that principle reach corner-on-line and corner-on-wall contacts.
Novelty
apparently-novel Not found in the recorded search, subject to its stated gaps
Records
n = 5 register evidence 1 evidence 2
n = 5 register evidence 1 evidence 2
T-058 V3 C3 wand125 after Tokoharu, Daniel · 2026-09-29 · 100 cases
Rectangle-certificate ceiling α·UB(n) proved for $n = 1$ ..100; B·UB(n) on 64 grid rows

Verification

upper: replayed here; lower: external proof (not read here)

—

Rigidity

locally rigid, verified, proof audited

Evidence: E-n005-second-order-rigidity, E-n005-fixed-side-local-rigidity

Scope

Local isolation at fixed side, for the exact labeled pose, on a first-party proof independently reviewed here. At s = 2 + (1/2)sqrt(2), Goebel's labeled pose P0 is an isolated point of the feasible set in (R^2 x S^1)^5 -- closed unit squares inside [0, s]^2 with pairwise disjoint interiors -- so no nonconstant continuous feasible path starts at it and no sequence of distinct feasible poses converges to it, and the unlabeled packing is rigid in the catalogue's fixed-side sense by a covering-space lift. Established over Q(sqrt 2) in one intrinsic half-angle chart: all 400 elementary wall-corner and pair inequalities are classified by exact sign, a neighbourhood cut out by 128 strict sign conditions carries the local feasible set as exactly the 20 active rows, T-012's first-order cone (the middle square's rotation, the other fourteen coordinates pinned by 28 Farkas certificates) and its non-negative self-stress transfer to that chart with w . q < 0, and semialgebraic curve selection on the punctured feasible set plus an induction on a putative arc's Taylor coefficients through order 2m contradicts feasibility. The declared replay decides the cone and the self-stress, which is the part T-012 owns; the closing is a proof, not a computation, and no instrument decides isolation. Two limits of that instrument, non-blocking and graded so by the review: its binding check compares the second jet only along the flex direction e_{u4} rather than the full transported Hessian, which is sufficient because Lemma 8's order-2m induction and Theorem 11 consume only e^T H_j e, and the packet's own verify_chart.py does check the full transported Hessian on all 20 rows; and its reduction audit samples only the interior of the neighbourhood N, never near the boundary, which the proof does not need because N is cut out by sign persistence rather than by a radius. Registered as T-014. NOT established: any isolation radius; rigidity with the side free, which X-007 measured to be false; global uniqueness; any other n = 5 optimal packing; applicability of the Connelly-Whiteley tensegrity theorems as stated. Fixed side throughout. What a source says about this packing's rigidity is carried by reported_upper_bound.catalogue_rigid and is deliberately not restated here as a finding of ours.

Evidence and sources

5 evidence entries

E-kingbird-upper-register, E-basic-grid-upper, E-nagamochi-lower, E-n005-gobel-upper, E-n005-gobel-proof

[Kingbird] record catalogue
[Friedman DS7] lower bound proof

In the frontier survey On GitHub

$s (5)$ — solved

$s (5) = 2 + \frac{1}{2} \sqrt{2} \approx 2.70710678$ . The first case where tilting beats the grid: four squares sit in the corners and the fifth is rotated 45° in the middle. A 3×3 grid would need side 3, so the tilt buys $0.293$ .

The final frame of the certified exact five-square trajectory.

This export follows an exact feasible segment between two optimal poses. Its contact marks describe certified contacts at the final endpoint and appear only when the animation arrives there. The SVG falls back to that endpoint when animation is unsupported or reduced.

Why this case matters out of proportion to its size

It is the smallest instance of the phenomenon that makes the whole subject hard. Up to $n = 4$ the answer is the obvious grid; at $n = 5$ the optimum is irrational and the optimal packing is not axis-aligned. Everything downstream — Erdős–Graham’s asymptotic tilted constructions, Gardner’s conjecture, the difficulty at $n = 11$ — is this observation iterated.

Note the degree: $2 + \frac{1}{2} \sqrt{2}$ is algebraic of degree 2. Every solved case in this catalogue has $s (n)$ of degree ≤ 2. That contrast makes the degree-8 $n = 11$ construction a warning that familiar unavoidable-point arguments may need richer geometry; no degree ceiling for that proof method is established here.

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-n005-gobel-proof`	a published proof	no code	no verification code
verified upper	`E-n005-gobel-upper`	replayed here	independent	`V-sqpack-verify` (first-party)

Bounds

Results in the register

\(s (5)\)s(5) — solved

Why this case matters out of proportion to its size

Verification Code

$s (5)$ — solved