T-014: Goebel's $n = 5$ optimum is rigid at fixed side: its pose is an isolated feasible point

V3 C3 rigidity confirmed

2026-09-03 established · Levy · $n = 5$

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.

Significance, composition and next rung

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.
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.
Novelty: apparently-novel Not found in the recorded search, subject to its stated gaps

The case

Case record

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

The case record

LowerUpper

Verified

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

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

Reported2.70710678…

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

Gap0 solved: the verified bounds meet

Results on the case

4 results in the register on $n = 5$ , oldest first, each with what it established and how it stands now.

2005 published T-007
$s (n) \geq min (⌈ \sqrt{n} ⌉, \sqrt{n - 2 ⌊ \sqrt{n} ⌋ + 1} + 1)$ for $4 \leq n \leq 324$
V0 C1 lower bound incomplete on this case, superseded
Nagamochi · Nagamochi 2005 · source · register
2026-08-30 established T-012
Goebel's $n = 5$ packing is second-order rigid at fixed side
V3 C3 rigidity confirmed
Levy · register
2026-09-03 established T-014 this result
Goebel's $n = 5$ optimum is rigid at fixed side: its pose is an isolated feasible point
V3 C3 rigidity confirmed
Levy · register
2026-09-29 published T-058
Rectangle-certificate ceiling α·UB(n) proved for $n = 1$ ..100; B·UB(n) on 64 grid rows
V3 C3 method limit confirmed
wand125 after Tokoharu, Daniel · wand125 tools 2026 · packet · register

Links

On this site: Case record, $n = 5$ · Frontier row, $n = 5$ · T-014 in the results table

On GitHub, at main

Register: T-014 in results.yaml, line 657
Evidence: E-n005-fixed-side-local-rigidity · E-n005-second-order-rigidity
Proofs and certificates: certificate bc-049-n5-rigidity-certificates.json
Artifacts: 7 artifacts and controls
campaign/explorations/X-012-one-chart-four-hundred-inequalities-and-an-order-2m-contradiction.md campaign/series/series-000-smoke-and-calibration/results/exp-058-h-060-n5-chart-and-proof.json campaign/series/series-000-smoke-and-calibration/results/bc-049-n5-rigidity-certificates.json src/sqpack/local_rigidity/instrument.py devtools/assess_n5_rigidity.py tests/test_n5_local_rigidity.py tests/test_n5_rigidity.py
Case file: frontier/n-005.md (verified lower, verified upper, reported lower, reported upper)

T-014: Goebel's n=5n=5 optimum is rigid at fixed side: its pose is an isolated feasible point

The case

Results on the case

Links

T-014: Goebel's $n = 5$ optimum is rigid at fixed side: its pose is an isolated feasible point