n = 19 open ★=

19340≤s(19)≤3+432

The best packing known for 19 squares, side 3+432, Robert Wainwright 1979
4.8254.886
456
4.3595.359
nn+1

Proven

4.825000≤s(19)≤4.885619

  • new result
  • exact

Citation record n-019

lowerwand125 after Tokoharu, Levy et al. 2026, GitHub (confirmed T-103)

upperWainwright 1979, Squares in Squares

Open

  • optimality

Bounds

Best known packing

3+432

4.88561808316412
Found by
Robert Wainwright 1979
Construction
hand
Source
[Kingbird]
Evidence
E-kingbird-upper-register, E-lifted-q2-upper
Verified upper bound

3+432

4.88561808316412673173558496561293

The reported value, verified here.

Evidence
E-lifted-q2-upper
Reported lower bound

19340

Proved by
wand125 2026
Kind
counting
Scope
Unrestricted unit-square packing with independent rotations and disjoint interiors.
Note
wand125's square-packing-bounds (6 October 2026) reports s(19)≥193/40 from a density of 341 uniform rectangles of total mass 1899999/100000, on a net the certificate declares: core side 4999/5000 and 2073 half-angle tangents of step 1/5002, accepted there at every direction by sqverify-proof-net, the source's copy of this repository's sqverify_fast changed to read a declared net (a check2 bundle, with no C++ record). It is above the 48229/10000 the record reported (T-100). sqverify-fast, this repository's clean-room measure verifier, decided it here at all 2073 directions on 6 October 2026.
Source
[wand125 mixed bounds check2 2026-10-06]
Evidence
E-n019-wand125-mixed-4825-report
Verified lower bound

19340

The reported value, verified here.

Evidence
E-n019-wand125-mixed-4825-sqverify-fast-replay
Gap

423−7340≈ 0.06061808…

Verified upper minus verified lower.

Results in the register

Verification

upper: replayed here; lower: replayed here

—

Rigidity

not rigid, numerically checked, numerical multiprecision

Evidence: E-translation-escape-not-rigid

Scope

Square 11 of the retained witness (witness id 12) translates 0.028595 along (0, 1) with the packing still valid, so the configuration admits a non-trivial feasible motion; 4 of its 19 squares do. Every constraint is exactly affine in the slide parameter, so the arithmetic carries no linearization error, but the coordinates are the witness's own finite-precision transcription: this settles the retained configuration, not the true optimum. Rigidity and optimality are independent, and this bears only on the former.

Open questions
  • Blocker (source evidence): Green's reported lower-bound proof, cited as private communication by Friedman, has not been recovered or independently replayed. E-green-ds7-theorem10-reported-lower

s(19) — open

External intake, 2026-10-06. wand125’s check2 source reports s(19)≥193/40=4.825 (T-103), from a density of 341 rectangles of total mass 1899999/100000<19, on a net the certificate declares: core side 4999/5000 and 2073 half-angle tangents of step 1/5002. Since 4999/5000·(1+1/5002)<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 48229/10000 (T-100) by 0.0021. This repository’s clean-room verifier sqverify-fast decided it here on 6 October 2026 at all 2073 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-06. wand125’s finer-net source reports s(19)≥48229/10000=4.8229 (T-100), since superseded (T-103), from a density of 313 rectangles of total mass 1899999/100000<19, on a net the certificate declares: core side 999/1000 and 416 half-angle tangents of step 1/1001, the net of its 5 October certificate at n=18. Since 999/1000·(1+1/1001)<1, every unit square contains a core at a net angle strictly in its interior. The source accepts it at every net angle by its research copy of Tokoharu’s checker at threshold one. It is above the rectangle certificate’s 1927/400 below by 0.0054, and above (7+7)/2=4.82287566, the side of Hämäläinen’s packing of 18 squares and the verified upper bound at n=18, by about 2.43×10−5, so s(18)<s(19), as the source notes. This repository’s clean-room verifier sqverify-fast decided it here on 6 October 2026 at all 416 directions of its net, and refused two mutants scaled below coverage one: confirmed, independently re-implemented, so it was also the verified lower bound until later that day, when the check2 certificate above superseded it in both lanes. The source’s own checker was replayed here at 10 of the 416 directions, each returning the certificate’s own record, and not in full. 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(19)≥1927/400=4.8175, with total mass 1899/100=18.99<19, 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 963/200=4.815 certificate for this case, whose reported bound the 2026-10-01 intake above raises, with total mass 1899/100=18.99<19, accepted by Tokoharu’s unchanged interval checker. This repository’s exact audit checks that the regenerated checker input is the published one, and checks the mass and net premises; the complete coverage replay has not yet run here, so the verified lower bound is unchanged. wand125’s README says parts of the work were produced with AI assistance under human direction.

Open. The best known packing gives s(19)≤4.88561809. The verified lower bound is s(19)≥193/40=4.825, from wand125’s check2 certificate on its finest declared net (T-103, 2026-10-06, V3/C3), leaving a gap of 0.0606 to the reported record. It is above n=18’s verified upper bound (7+7)/2, so s(18)<s(19), as was its predecessor at 48229/10000=4.8229 (T-100, 2026-10-06), the verified lower bound until later that day. That one superseded wand125’s rectangle-density certificate of 1 October at 1927/400=4.8175 (T-074, replayed here on 2026-10-02), which was the verified lower bound until 2026-10-06. That one’s predecessor of 27 September, 963/200=4.815 (T-045), held the field earlier that day, and had superseded this repository’s weighted fractional unavoidable-set certificate at 24/5=4.8 (T-020, 2026-09-04). On 2026-09-04 this case moved twice in one day, from 22529/5000=4.5058 to 459/100=4.59 (T-019) and then to 24/5, a total of 0.294200. Nagamochi’s general 1+12≈4.464102 had held it before that, and was already weaker than the first of the two. Corrected 2 October 2026: Nagamochi’s value is now a reported bound, his Lemma 1 being false (Karakuş 2026; review). This register had recorded that proof as verified, its own error, logged as defect D-516.

The packing

Wainwright’s diagonal strip of width two (1979), for which the survey states no generating rule — only the figure. cases/lifted_q2 lifts the retained witness’s every coordinate into Q(sqrt 2) at small height and verifies the lifted pose exactly, which is what moved verified_upper_bound from the grid ceiling onto the published exact side. The lift is a candidate generator and the exact verifier is the proof; the certificate is the witness’s own geometry, made exact (D-398, and the operation D-402 does not foreclose).

The lower bound

The earlier external report, [Friedman DS7], gives the lower-bound expression 45/5+22 for s(19) (approximately 4.617281506746). Friedman’s DS7 survey, Theorem 10, k=4, reports this bound at n=19; reference [8] is Green’s private communication (2000). The source proof has not been recovered. This is the literal specialization of the printed general theorem; Table 2 lists the weaker 6*sqrt(2)-4 at n=19-20. The source does not explain that tension. wand125’s rectangle-density certificate above has since replaced it in the reported field, and from its replay here on 2026-10-02 it was also the verified lower bound until wand125’s mixed certificate on a declared net (T-100) replaced it in both on 2026-10-06. The source audit compares the exact theorem expressions separately from opaque table decimals.

Until 2026-10-02 the operative bound was a weighted fractional unavoidable-set certificate at side 24/5: 2260 rationally weighted atoms on a D4-symmetric site set, total mass 946131/50000<19, every closed B-square at every net direction capturing mass at least one, the least being 50007/50000. It is decided from its own bytes by an exact event-cell sweep and by an interval branch and bound over centre boxes, which agree on that least value to the digit. Nothing is inherited by monotonicity. Of the five conditions only Condition 2 mentions n, so this atom set certifies its side for every integer strictly above its own mass — 19 and upward — which is why the same certificate also carries n=20 and n=21. Its predecessor, T-019, reaches this case the same way from a lighter set, and before either of them the case was held by the n=17 Massaccesi certificate carried across by monotonicity, a 2026 blog-post result whose author marks the value “(?)” and which is replayed here twice (H-052, BC-150, BC-151). 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). Nagamochi’s general closed form remains the external published baseline and applies to every N≥4:

s(N)≥min{⌈N⌉,N−2⌊N⌋+1+1}

Here it gives 1+12≈4.4641, now weaker by 0.335898; the first movement of this case’s verified lower bound since 2005 came on 2026-09-03.

What the method can still add here

A certificate for n cannot exist above ⌈n⌉·B, which at B=9977/10000 is 4.9885 — but no certificate can exceed a side an actual packing achieves either, and Wainwright’s packing achieves 4.88561808. So the packing binds first and the runway above 24/5 was 0.0856, not 0.1885; above 963/200 it was 0.0706, above 48229/10000 it was 0.0627, and above the current 193/40 it is 0.0606. A run that certified a side above 4.88561808 would contradict the retained witness; that is a refutation to go looking for, not a rung to expect.

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-n019-wand125-mixed-4825-sqverify-fast-replay replayed here shared components V-sqverify-fast (first-party)
verified upper E-lifted-q2-upper replayed here independent V-sqpack-verify (first-party)