\(s (27)\)$s(27)$ — open

External intake, 2026-10-06. wand125’s check2 source reports \(s(27) \ge 11287/2000 = 5.6435\)$s(27)\ge 11287/2000=5.6435$ (T-106), from a density of 439 rectangles of total mass \(2699999/100000 < 27\)$2699999/100000<27$, on a net the certificate declares: core side \(1999/2000\)$1999/2000$ and 832 half-angle tangents of step \(1/2006\)$1/2006$. Since \(1999/2000 \cdot (1 + 1/2006) < 1\)$1999/2000·(1+1/2006)<1$, every unit square contains a core at a net angle strictly in its interior. The source ships no record of its C++ checker for it: it accepts it at every direction with its copy of this repository’s sqverify_fast, changed to read a declared net. It is above the reported \(1127/200\)$1127/200$ (T-068) by \(0.0085\)$0.0085$. This repository’s clean-room verifier sqverify-fast decided it here on 6 October 2026 at all 832 directions of its net, and refused two mutants scaled below coverage one: confirmed, re-implemented sharing the producer’s components (the source’s check is a copy of the same crate), so it is also the verified lower bound. wand125’s README says parts of the work were produced with AI assistance under human direction.

External intake, 2026-10-01. wand125’s rectangle-density source reports \(s (27) \ge 1127 / 200 = 5.635\)$s(27)\ge 1127/200=5.635$, since superseded (T-106), with total mass \(2699/100 = 26.99 < 27\)$2699/100=26.99<27$, accepted by Tokoharu’s unchanged interval checker. The complete 201-direction coverage replay here accepted it again, after this repository’s exact audit checked that the regenerated checker input is the published one and checked the mass and net premises, so it was also verified until 2026-10-06, when the certificate above superseded it in both lanes. wand125’s README says parts of the work were produced with AI assistance under human direction.

External intake, 2026-09-27. wand125’s rectangle-density source reports a direct \(28/5 = 5.6\)$28/5=5.6$ certificate for this case, whose reported bound the 2026-10-01 intake above raises, with total mass \(26999/1000 = 26.999 < 27\)$26999/1000=26.999<27$, accepted by Tokoharu’s unchanged interval checker. The complete 201-direction coverage replay here accepted it again, after this repository’s exact audit checked that the regenerated checker input is the published one and checked the mass and net premises, so it was also the verified lower bound until the 2026-10-01 intake above. wand125’s README says parts of the work were produced with AI assistance under human direction.

External intake, 2026-09-22. Tokoharu’s retained rectangle-density source reports \(s (26) \ge 1377 / 250 = 5.508\)$s(26)\ge 1377/250=5.508$; monotonicity carries the reported bound to \(n = 27\)$n=27$. The complete source replay verifies the source premise, so the same monotonicity argument verified that bound at \(n = 27\)$n=27$ until the direct certificate above superseded it. Tokoharu’s README says parts of the work were produced with AI assistance under human direction.

Open. The verified lower bound is \(11287/2000 = 5.6435\)$11287/2000=5.6435$, from wand125’s check2 certificate on a declared net (T-106, 2026-10-06, V3/C3), which superseded its rectangle-density certificate of 1 October at \(1127/200 = 5.635\)$1127/200=5.635$ (T-074), and the verified upper bound is approximately \(5.707106781\)$5.707106781$, exactly \(5 + \sqrt{2} / 2\)$5+\sqrt{2}/2$, leaving a gap of about \(0.0636\)$0.0636$. Friedman also reports Green’s older lower bound of approximately \(5.3918\)$5.3918$, whose proof has not been recovered.

The packing

Found by Frits Göbel in 1979, via a diagonal-strip construction — the strip family at \(a = 4\)$a=4$, whose side is \(5 + \sqrt{2} / 2\)$5+\sqrt{2}/2$ exactly. cases/gobel_strip builds it and verifies it exactly over Q(sqrt 2), which is what moved verified_upper_bound from the grid ceiling onto the exact side. The retained witness declares that side rounded down at its own digits — about \(4.85 \times 10^{-30}\)$4.85\times {10}^{-30}$ below the exact value — and a different slack choice for the strip, so the certificate carries the construction’s coordinates rather than the witness’s (D-398).

The lower bound

The verified lower bound is \(11287/2000 = 5.6435\)$11287/2000=5.6435$, from wand125’s check2 certificate of 6 October on a declared net (T-106), decided here by sqverify-fast at every direction of its net; before it, its rectangle-density certificate of 1 October at \(1127/200 = 5.635\)$1127/200=5.635$ (T-074). Earlier, wand125’s n27 rectangle-density certificate of 27 September, replayed here over all 201 directions, verified \(28/5\)$28/5$ directly: 168 rectangle orbits, total mass \(26999/1000\)$26999/1000$, below 27 by \(1/1000\)$1/1000$. Before it, the complete n26 interval replay verified \(1377/250\)$1377/250$, which deleting one square carried to n27. A method-distinct rectangle coverage implementation would add confidence and improve generalization, but it is not a missing premise of either bound.

Corrected 2 October 2026: Nagamochi’s Lemma 1 is false (Karakuş 2026), so his closed form below is now a reported bound whose published proof is incomplete (review). This register had recorded that proof as verified, its own error, logged as defect D-516. Nagamochi’s earlier general closed form remains part of the evidence history and applies to every \(N \ge 4\)$N\ge 4$:

Friedman’s survey, Table 2, reports Green’s \(2 \sqrt{2} + (27 + 2 \sqrt{10}) / 13 \approx 5.3918\)$2\sqrt{2}+(27+2\sqrt{10})/13\approx 5.3918$ for \(n = 26,27\)$n=26,27$. Its \(n = 26\)$n=26$ statement follows from Theorem 9 at \(k = 5\)$k=5$, and monotonicity gives \(n = 27\)$n=27$. Reference [8] is a private communication from 2000, with no proof or twenty-six-square point configuration supplied in the survey. The unavoidable-set argument DS7’s Figure 34 illustrates does not prove it: at \(k = 5\)$k=5$ that point pattern leaves a unit square empty (review). The n26 review records this reported bound separately from the verified one.

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.