$n=19$$n=19$

Bounds

Results in the register

• T-007 S3 V0 C1 Nagamochi · 2026-08-31 · 321 cases

  s(n)≥min(⌈n​⌉,n−2⌊n​⌋+1​+1)$s(n)\ge min(\lceil \sqrt{n}\rceil ,\sqrt{n-2\lfloor \sqrt{n}\rfloor +1}+1)$ for $4\le n\le 324$$4\le n\le 324$

• T-016 S3 V3 C3 Massaccesi after Burns · 2026-09-03 · n = 18, 19

  $s(n)\ge 22529/5000$$s(n)\ge 22529/5000$ for $n=18,19$$n=18,19$, by monotonicity from T-015

  Claim and records

  Claim

  $s(18)\ge 22529/5000$$s(18)\ge 22529/5000$ and $s(19)\ge 22529/5000$$s(19)\ge 22529/5000$, by monotonicity from T-015 (a packing of n >= 17 unit squares contains a packing of 17). At $n=19$$n=19$ this replaces Nagamochi's 1 + sqrt(12) = 4.4641... since (22529/5000 - 1)^2 = 307265841/25000000 > 12; at $n=20$$n=20$ the certificate does not improve 1 + sqrt(13) = 4.6055... since that square is below 13, and nothing changes.

  Significance

  The same movement carried to $n=18$$n=18$ (+0.079587 over T-002) and $n=19$$n=19$ (+0.0416984 over Nagamochi's 1 + sqrt(12), the first movement of that case's verified lower bound since 2005); the derivation adds one line beyond T-015 and inherits its source and credit.

  Novelty

  previously-published Present in an identified source

  Records

  n = 18n = 19registerevidence 1evidence 2

  n = 18n = 19registerevidence 1evidence 2

• T-019 S4 V3 C3 Levy after Burns, Massaccesi · 2026-09-04 · n = 17–19

  $s(n)\ge 459/100=4.59$$s(n)\ge 459/100=4.59$ for $n=17,18,19$$n=17,18,19$

  Claim and records

  Claim

  $s(17)\ge 459/100$$s(17)\ge 459/100$, and $s(18)\ge 459/100$$s(18)\ge 459/100$ and $s(19)\ge 459/100$$s(19)\ge 459/100$, from this project's weighted fractional unavoidable-set certificate at container side 459/100 = 4.59.
  
  This displaces Massaccesi's 22529/5000 = 4.5058 (T-015) and the two cases T-016 carried from it, all three of which had held that value until 2026-09-04. The movement past the published value is +0.0842 at each of the three sizes.
  
  A stronger public candidate, anabologyco-maker's side 4.5705 (nine thousand one hundred forty-one two-thousandths) of 16 August 2026 (GitHub; not replayed here), was outside the record's search corpus when this was registered and was found on 2026-09-07; it lies 0.0195 below this result. Two rungs are retained below it, 451/100 and 229/50.
  
  The September 2026 DS7 audit identifies a stronger reported n19 bound from Theorem 10 at k=4, approximately 4.6172815, with an unresolved theorem/table discrepancy and missing proof. T-019 does not improve that report; its public source displacement is supported at n17 and n18, while all three certified inequalities and their movements from the prior register remain valid.
  
  The three sizes do not need a monotonicity step. Only Condition 2 mentions n among the five conditions, so an atom set of mass 423327/25000 certifies the side for every integer above it, which is 17 and upward; monotonicity would give the same thing and is not what is used.
  
  It does not improve $n=20$$n=20$, where Nagamochi's 1 + sqrt(13) = 4.6055... is larger -- the certificate does prove $s(20)\ge 459/100$$s(20)\ge 459/100$, but that is the weaker statement.

  Significance

  Scored against the rubric's anchor for S4, "a reusable technique, bound family, or resolved disputed value". One certificate moves three registered cases, and it replaces a published value rather than an inherited or closed-form one -- the only bound this project has displaced that someone else had put in print.
  
  A stronger public candidate found afterwards, anabologyco-maker's 9141/2000 = 4.5705 of 16 August 2026 (GitHub; not replayed here), was outside the search corpus at scoring time, so the displacement at n17 and n18 is 0.0195 over that public report and 0.0842 over the one this record had adopted. At n19, the DS7 audit now retains a stronger source-reported bound than T-019; its 0.0842 movement refers to the prior register. The family-level score is unchanged.
  
  Held below S5 because none of $n=17$$n=17$, 18, 19 is a central open case, the movement is 0.0842 rather than a qualitative change, weighted resource counting predates this project, the recent pure-atomic rational direction-net architecture follows Burns, the LP parameter line follows Massaccesi, and the case does not change character at the new value.

  Novelty

  apparently-novel Not found in the recorded search, subject to its stated gaps

  Records

  n = 17n = 18n = 19registerevidence 1evidence 2

  n = 17n = 18n = 19registerevidence 1evidence 2

• T-020 S4 V3 C3 Levy after Burns, Massaccesi · 2026-09-04 · n = 19–21

  $s(n)\ge 24/5=4.80$$s(n)\ge 24/5=4.80$ for $n=19,20,21$$n=19,20,21$

  Claim and records

  Claim

  $s(19)\ge 24/5$$s(19)\ge 24/5$, $s(20)\ge 24/5$$s(20)\ge 24/5$ and $s(21)\ge 24/5$$s(21)\ge 24/5$, from this project's weighted fractional unavoidable-set certificate at container side 24/5 = 4.80.
  
  Two of the three cases previously held Nagamochi's 2005 general closed form in this register's independently verified lower fields -- min(ceil(sqrt(N)), sqrt(N - 2*floor(sqrt(N)) + 1) + 1), which gives 1 + sqrt(13) = 4.6055... at $n=20$$n=20$ and 1 + sqrt(14) = 4.7416... at $n=21$$n=21$ -- and the third held the 459/100 = 4.59 this project certified earlier the same day as T-019. The movement is +0.21 at $n=19$$n=19$, +0.194449 at $n=20$$n=20$ and +0.058343 at $n=21$$n=21$, relative to those verified fields.
  
  The September 2026 DS7 audit records stronger external reports below 4.80 separately, with missing source proofs and table discrepancies explicit; no claim of historical priority follows from the earlier source omissions.
  
  The three sizes take no monotonicity step. Only Condition 2 mentions n among the five conditions, so an atom set of mass 946131/50000 certifies the side for every integer strictly above that mass, which is 19 and upward. From $n=22$$n=22$ on the register already holds 5, so the certificate is true there and weaker; these three are where it moves anything.
  
  One rung is retained rather than a ladder. The side was reached in a single resumed column-generation run, not climbed to, so there is no weaker certificate at this size to compare it against.

  Significance

  Scored against the rubric's anchor for S4, "a reusable technique, bound family, or resolved disputed value", and by parity with T-019, which has the same shape: one certificate moving three registered cases and displacing a published value.
  
  This one displaces more. The movement is +0.21 at $n=19$$n=19$ against T-019's +0.0842, the largest single-case movement in the register; and at $n=20$$n=20$ and $n=21$$n=21$ it displaces the peer-reviewed 2005 closed form previously used in the verified register. The September 2026 source audit corrects the earlier claim that no size-specific bounds had been reported; it does not change these measured displacements of the verified fields.
  
  Held below S5 for the reasons T-019 was: none of the three is a central open case, the weighted-resource lineage predates this project, the pure-atomic rational direction-net architecture follows Burns, the LP parameter line follows Massaccesi, and no case changes character at the new value.
  
  A calibration note for whoever scores the next one. This is the fourth result from one instrument in a day, and the S4 anchor is being carried here by the displacement rather than by the technique, which T-017 already banked. Further sizes from the same generator, absent a new technique or a case that changes character, belong at S3.

  Novelty

  apparently-novel Not found in the recorded search, subject to its stated gaps

  Records

  n = 19n = 20n = 21registerevidence 1evidence 2

  n = 19n = 20n = 21registerevidence 1evidence 2

• T-045 S3 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-09-29 · 15 cases

  Rectangle-density lower bounds replayed at 15 counts in $n=18\dots 78$$n=18\dots 78$

• T-046 S3 V0 C0 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-09-29 · 48 cases

  Rectangle-density lower bounds reported for 48 counts in $n=18\dots 95$$n=18\dots 95$

• T-058 S2 V3 C3 Hosono after Tokoharu, Daniel · 2026-09-29 · 100 cases

  Rectangle-certificate ceiling α·UB(n) proved for $n=1$$n=1$..100; B·UB(n) on 64 grid rows

• T-068 S3 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-01 · 34 cases

  Rectangle-density lower bounds verified at 34 counts in $n=19\dots 95$$n=19\dots 95$

• T-074 S3 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-02 · 31 cases

  Rectangle-density lower bounds replayed at 31 counts in $n=19\dots 95$$n=19\dots 95$

• T-083 S3 V3 C3 Karakuş · 2026-10-02 · 301 cases

  s(n)≥1/2+n−⌊n​⌋+1/4​$s(n)\ge 1/2+\sqrt{n-\lfloor \sqrt{n}\rfloor +1/4}$ for every nonsquare $8\le n\le 324$$8\le n\le 324$

• T-085 S3 V3 C3 Karakuş; Vlasenko · 2026-10-02 · 315 cases

  Nagamochi 2005, Lemma 1 is false for every container with $a>3$$a>3$ and $b>2$$b>2$

• T-100 S3 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-06 · n = 19

  Mixed rectangle-measure lower bound verified at $n=19$$n=19$, past the best 18-square packing

  Claim and records

  Claim

  A rectangle density of wand125/square-packing-bounds, checked at coverage one on a net it declares and published on 6 October 2026, proves $s(19)\ge 48229/10000$$s(19)\ge 48229/10000$ = 4.8229.
  
  The certificate is a density of 313 uniform rectangles in D4 orbits, and no point mass, of total mass 1899999/100000, on the net T-096's certificate declares: core side 999/1000 and 416 half-angle tangents of step 1/1001, with 999/1000 (1 + 1/1001) = 500499/500500 < 1. The source reports every core at a net angle capturing mass at least one: at all 415 oblique net angles by code/mixed_rotated_verify.cpp, its research copy of Tokoharu's verify.cpp at coverage threshold one, run by the same driver as T-096's certificate, and at the axis by exact integer tables.
  
  The value is above the 1927/400 = 4.8175 of the source's rectangle certificate rect_n19_L48175 (T-074), the reported and verified lower bound at $n=19$$n=19$ before it, by 0.0054. It is also above (7 + sqrt 7)/2 = 4.8228757..., the side of Hämäläinen's packing of 18 squares and the verified upper bound at $n=18$$n=18$, by about 2.43e-5, so $s(18)$$s(18)$ < $s(19)$$s(19)$, as the source notes.
  
  The certificate was decided here on 6 October 2026 by sqverify-fast, this repository's clean-room measure verifier, at all 416 directions of the net the candidate declares, and two mutants scaled below coverage one were refused: confirmed, independently re-implemented. The verifier shares no code with the source's checker and runs the same net-and-shrink method, so it is a second implementation and not a second method. The 6 October review of the certificate found no defect. 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.
  
  Hosono after Tokoharu and Levy, square-packing-bounds. Registration was requested in a comment of 6 October 2026 on jlevy/squares#366. The source says parts of the work were produced with AI assistance under human direction.

  Significance

  The strongest verified lower bound on record at $n=19$$n=19$, by 0.0054, and the first to pass the side of the best packing of 18 squares, which separates $s(18)$$s(18)$ from $s(19)$$s(19)$ (Daniel's question on jlevy/squares#281), by about 2.43e-5. The certificate kind and checker of T-069 and later on T-096's declared net; no new technique, at S3 as T-074 is, the separation a corollary of this bound and Hämäläinen's packing rather than a method or a family of bounds. The 6 October review confirmed the draft.

  Novelty

  previously-published Present in an identified source

  Records

  n = 19registerevidence 1evidence 2sourcereview

  n = 19registerevidence 1evidence 2sourcereview

• T-103 S3 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-06 · n = 19

  Mixed rectangle-measure lower bound verified at $n=19$$n=19$, on the finest declared net yet

  Claim and records

  Claim

  A rectangle density of wand125/square-packing-bounds, checked at coverage one on a net it declares and published on 6 October 2026, proves $s(19)\ge 193/40$$s(19)\ge 193/40$ = 4.825.
  
  The certificate is a density of 341 uniform rectangles in D4 orbits, and no point mass, of total mass 1899999/100000, on a net it declares itself, finer than any it declared before: core side 4999/5000 and 2073 half-angle tangents of step 1/5002. Since 4999/5000 (1 + 1/5002) = 25009997/25010000 < 1, and the last tangent 1036/2501 is past tan(pi/8), every unit square contains a concentric core at a net angle strictly in its interior.
  
  The source reports every such core capturing mass at least one at all 2073 directions, by sqverify-proof-net, its copy of this repository's sqverify_fast changed to read the declared net, and ships no record of its C++ checker for this certificate.
  
  The value is above the 48229/10000 = 4.8229 of T-100, the source's earlier certificate and the reported and verified lower bound at $n=19$$n=19$ before it, by 0.0021, and supersedes it.
  
  The certificate was decided here on 6 October 2026 by sqverify-fast, this repository's clean-room measure verifier, at all 2073 directions of the net the candidate declares, and two mutants scaled below coverage one were refused: confirmed, re-implemented sharing the producer's components. The source's check is a copy of the same crate with one change, so the two share the sqverify_fast crate; their records agree direction by direction, and their agreement is not a second implementation. The source's C++ checker, the producer's own code but sharing none with the crate, verified the candidate here at threshold one at nodes 1021 and 2072, the least-bound node of the source's run among them, and was not run in full: samples that decide those nodes only.
  
  Hosono after Tokoharu and Levy, square-packing-bounds. No registration was requested: an intake pass of the source found it. The source says parts of the work were produced with AI assistance under human direction.

  Significance

  The strongest verified lower bound on record at $n=19$$n=19$, by 0.0021 above T-100, and the strongest reported. The certificate kind of T-099 on a declared net, checked at the source by a copy of this repository's verifier rather than its C++ checker; no new technique, at S3 as T-096, T-099 and T-100 are.

  Novelty

  previously-published Present in an identified source

  Records

  n = 19registerevidence 1evidence 2sourcereview

  n = 19registerevidence 1evidence 2sourcereview

• T-194 S5 V0 C1 Fitzharding after Levy, Ahmed · 2026-10-16 · n = 19

  Fitzharding reports a Lean proof that Wainwright's packing is optimal, s(19)=3+42​/3$s(19)=3+4\sqrt{2}/3$

  Claim and records

  Claim

  Fitzharding reports a Lean 4 proof that Wainwright's 1979 packing of nineteen unit squares is optimal: $s(19)=3$$s(19)=3$ + (4/3)√2 = 4.885618083164126731735584965612…. Its theorem, Sq19.square19_optimality (L : ℝ) : Feasible19 L ↔ 3 + 4 * Real.sqrt 2 / 3 ≤ L, says that nineteen closed unit squares, each independently translated and rotated, with pairwise disjoint interiors, fit in the axis-aligned square [0, L]^2 exactly when L is at least that side; existence at the side is part of it, so the minimum is attained. The side is the case's exact upper bound, 3 + (4/3)sqrt(2).
  
  Its trust boundary, as the source states it: the geometric soundness arguments are checked by Lean's kernel, and 4,320 finite certificate facts are decided by native_decide, so Lean's compiler, native evaluator and the C toolchain are trusted, with the standard axioms propext, Classical.choice and Quot.sound and no sorryAx. The source reports a kernel replay of the theorem's 13,143-module import closure with no failure, which takes the native facts as axioms, and says that a complete rebuild from its published sources has not yet been run. Nothing here has built it.
  
  A mathematical review of 16 October, by an AI lane prompted separately and reading the source as data, found no blocking or major defect: it read the statement, the endpoint, the six-step chain to the final theorem and the trust boundary, decided the endpoint packing exactly, and with programs of its own re-established the property each of the 2,328 native facts whose modules are in the Git tree certifies; the 1,992 facts in the release archives, mostly half-plane propagation traces, were scanned but not re-run.
  
  Fitzharding, sq19, release v1.0.0 of 16 October 2026, announced on X the same day. Its README says it builds on his $s(17)$$s(17)$ formalization (T-154), whose checker modules it compiles from sq17-lean v1.0.0, and thanks the Squares Project and Ahmed; issue 640 also credits Wainwright's construction. It says it was "Developed with substantial assistance from Claude and Codex".

  Significance

  Scored as a claim, as T-153 and T-154 were while unverified, by the rubric's anchor, movement on a central open case: $n=19$$n=19$ is one of the five open cases below $n=21$$n=21$ (12, 17, 18, 19 and 20), and the claim settles it exactly at Wainwright's 1979 side, closing the 0.0606 gap between the verified floor 193/40 and the ceiling, in a proof assistant with a stated trust boundary. It is the first optimality claim the record holds at 19. Significance is separate from whether the proof is correct; the conservative reading is the same, since nothing less than the case's value is claimed. The review of 16 October found no reason to change it. Proposed for the owner's confirmation.

  Novelty

  previously-published Present in an identified source

  Records

  n = 19registerevidence 1sourcereview

  n = 19registerevidence 1sourcereview

In the frontier survey On GitHub