T-233: Mixed rectangle-measure lower bounds reported at $n = 19, 20, 26, 27$ , on a 2,073-direction net

V0 C1 Lower bound reviewed

2026-10-08 published · Hosono after Tokoharu and Levy · $n = 19, 20, 26, 27$

Four rectangle measures of wand125/square-packing, published on 7 and 8 October 2026 and reported in jlevy/squares#446, are reported to prove $s (19) \geq 1931 / 400$ = 4.8275, $s (20) \geq 393 / 80$ = 4.9125, $s (26) \geq 1111 / 200$ = 5.555 and $s (27) \geq 1131 / 200$ = 5.655.

The certificates, mixed_n19_L48275, mixed_n20_L49125, mixed_n26_L5555 and mixed_n27_L5655, are densities of 347, 471, 615 and 714 uniform rectangles in D4 orbits, each of total mass n - 1/100000, on a net each candidate declares: core side 4999/5000 and 2,073 half-angle tangents of step 1/5002, the net of T-132, T-142 and T-143. 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 $n = 27$ certificate is the author's follow-up of 8 October on the issue, which supersedes the issue's 2261/400.

The source reports every such core centred in its per-bin domain capturing mass at least one at all 2,073 directions of each net, by sqverify-proof-net, its copy of this repository's sqverify_fast changed to read the declared net, and a control with every mass scaled by 197/200 refused at 32 sampled directions of each.

Each value is above its case's reported and verified lower bound: 193/40 at $n = 19$ (T-103) by 1/400, 981/200 at $n = 20$ (T-104) by 3/400, 1109/200 at $n = 26$ (T-105) by 1/100 and 11287/2000 at $n = 27$ (T-106) by 23/2000.

Here the maintained readers accepted each candidate's exact mass, declared-net and check2 premises from its release members, retained since 23 October. The stage 4 review of 23 October read all four certificates and accepted them: it re-derived the argument, recomputed every exact premise apart from the crate, decided each axis direction completely by an independent vertex argument, and evaluated the source's logs and 32 sampled directions per count exactly, finding no blocking or major defect.

Complete sqverify-fast replays ran here on 23 October, from the retained candidates: each capture passed at all 2,073 directions, with the source's node total, and the whole-net controls were refused at $n = 19$ , 20 and 27. At $n = 26$ the control failed closed: the 99/100 mutant was refused at every direction, but at the axis direction its exact capture sits 3.28e-9 above the sweep's certified bound, beyond the census's constant allowance of 1e-9. The receipts are in packing/benchmarks/measure-verifier/census-mixed/wand125-fine-net-lower-bounds-446-release-2026-10-08/, $n = 26$ 's kept as mixed_n26_L5555.control-failed-v2.json. The replays' evidence is held until that allowance is fixed (think-tcsl), so the values stand as reported.

Hosono after Tokoharu and Levy, square-packing and mixed_n27_L5655. The source says parts of the work were produced with AI assistance under human direction.

Significance, composition and next rung

Significance: Scored as a claim: once replayed, each raises its case's verified and reported lower lanes, by 1/400 at $n = 19$ , 3/400 at 20, 1/100 at 26 and 23/2000 at 27, over T-103 to T-106, by the certificate kind and declared net of T-142 with no new technique, at S3 as T-103 to T-106 and T-142 are. At $n = 19$ the record also holds a reported Lean proof of $s (19) = 3$ + 4√2/3 (T-194), which would supersede any lower bound if adopted.
Composition: Four reported certificates on two reported entries, one for $n = 19$ , 20 and 26 and one for $n = 27$ , each read by the stage 4 review. The source's check is a copy of this repository's sqverify_fast crate with one change, so a sqverify-fast replay here would be re-implemented sharing the producer's components, as T-104's is, and no second implementation stands beside it. The review's own runs are samples and premise checks, cited by the case records. The entry takes the least rung of its four counts.
Next rung: C3 needs think-tcsl: a reviewed fix that derives the census control's axis allowance from the sweep's enclosure rather than the constant 1e-9 (F-1 of the 14 October review), $n = 26$ 's whole-net control re-judged from its retained receipt or rerun under it and ending CONTROLS_REFUSED, and then the replay evidence of the four complete captures and controls of 23 October mapped, by the checklist of the 6 October declared-net soundness review, of which the stage 4 review of 23 October is each certificate's review. The captures and controls themselves are spent, about 7.8 CPU-hours on 23 October, and are not rerun.
Unfinished confirmations: C3 (think-tcsl): mixed_n26_L5555's whole-net control re-judged from its retained receipt, or rerun, under think-tcsl's reviewed fix to the axis allowance, ending CONTROLS_REFUSED; then the replay evidence of the four complete captures and controls of 23 October mapped, by the checklist of the 6 October declared-net soundness review. About 0.01 CPU-hours, up to about 0.4 (priced 2026-10-23).
Novelty: previously-published Present in an identified source

The cases

Case record

4.824.886

456

4.3595.359

\sqrt{n}

\sqrt{n} + 1

Proven

$4.82500$ $\leq s (19) \leq$ $4.885619$

exact

Citation record n-019

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

upperWainwright 1979, Squares in Squares

Open

optimality

The case record

LowerUpper

Verified

\frac{193}{40}

3 + \frac{4}{3} \sqrt{2}

Reported

\frac{193}{40}

3 + \frac{4}{3} \sqrt{2}

Gap

\frac{4 \sqrt{2}}{3} - \frac{73}{40}

≈ 0.06061808…

Case record

4.905

456

4.4725.472

\sqrt{n}

\sqrt{n} + 1

Proven

$4.90500$ $\leq s (20) \leq$ $5$

exact

Citation record n-020

lowerHosono after Tokoharu, Levy et al. 2026, GitHub (confirmed T-104)

Open

optimality

The case record

LowerUpper

Verified

\frac{981}{200}

Reported

\frac{981}{200}

Gap

\frac{19}{200}

= 0.095

Case record

Regularized by the Squares Project with Daniel's regularizer (evand/square-packing, MIT)

As published

The packing as published, in its source’s pose, Friedman 1997 [Kingbird]

5.545.621

567

5.0996.099

\sqrt{n}

\sqrt{n} + 1

Proven

$5.54500$ $\leq s (26) \leq$ $5.621321$

exact

Citation record n-026

lowerHosono after Tokoharu, Levy et al. 2026, GitHub (confirmed T-105)

upperFriedman 1997, Squares in Squares

Open

optimality

The case record

LowerUpper

Verified

\frac{1109}{200}

\frac{7}{2} + \frac{3}{2} \sqrt{2}

Reported

\frac{1109}{200}

\frac{7}{2} + \frac{3}{2} \sqrt{2}

Gap

\frac{3 \sqrt{2}}{2} - \frac{409}{200}

≈ 0.07632034…

Case record

5.645.707

567

5.1966.196

\sqrt{n}

\sqrt{n} + 1

Proven

$5.64350$ $\leq s (27) \leq$ $5.707107$

exact

Citation record n-027

lowerHosono after Tokoharu, Levy et al. 2026, GitHub (confirmed T-106)

upperGöbel 1979, Squares in Squares

Open

optimality

The case record

LowerUpper

Verified

\frac{11287}{2000}

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

Reported

\frac{11287}{2000}

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

Gap

\frac{\sqrt{2}}{2} - \frac{1287}{2000}

≈ 0.06360678…

Results on these cases

24 results in the register on $n = 19, 20, 26, 27$ , oldest first, each with what it established and how it stands now.

2005 published T-007 · $n = 19, 20, 26, 27$
$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 these cases, superseded by T-103, T-104, T-105 and T-106
Nagamochi · Nagamochi 2005 · source · register
2026-08-21 published T-016 · $n = 19$
$s (n) \geq 22529 / 5000$ for $n = 18, 19$ , by monotonicity from T-015
V3 C3 Lower bound confirmed superseded by T-103
Massaccesi after Burns · Burns–Massaccesi n17 · packet · register
2026-09-04 established T-019 · $n = 19$
$s (n) \geq 459 / 100 = 4.59$ for $n = 17, 18, 19$
V3 C3 Lower bound confirmed superseded by T-103
Levy after Burns, Massaccesi · register
2026-09-04 established T-020 · $n = 19, 20$
$s (n) \geq 24 / 5 = 4.80$ for $n = 19, 20, 21$
V3 C3 Lower bound confirmed superseded by T-103 and T-104
Levy after Burns, Massaccesi · register
2026-09-04 published T-085 · $n = 19, 20, 26, 27$
Nagamochi 2005, Lemma 1 is false for every container with $a > 3$ and $b > 2$
V3 C3 Correction confirmed
Karakuş; Vlasenko · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register
2026-09-05 established T-021 · $n = 20$
$s (n) \geq 97 / 20 = 4.85$ for $n = 20, 21$
V3 C3 Lower bound confirmed superseded by T-104
Levy after Burns, Massaccesi · register
2026-09-22 published T-044 · $n = 26$
Weighted point lower bounds for ten counts in $n = 26 \dots 72$ , plus seven from the same files
V3 C3 Lower bound confirmed superseded by T-105
Hosono after Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 point bounds 2026 · packet · source · review · register
2026-09-22 published T-047 · $n = 26, 27$
$s (11) \geq 381 / 100$ ; $s (n) \geq 1377 / 250$ for $n = 26 \dots 28$ ; $s (n) \geq 571 / 100$ for $n = 29 \dots 31$
V3 C3 Lower bound confirmed superseded by T-105 and T-106
Tokoharu after Levy, Hosono, Stromquist, Nagamochi, Burns, Massaccesi · Tokoharu density 2026 · packet · source · review · register
2026-09-27 published T-045 · $n = 19, 20, 26, 27$
Rectangle-density lower bounds replayed at 15 counts in $n = 18 \dots 78$
V3 C3 Lower bound confirmed superseded by T-103, T-104, T-105 and T-106
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · packet · packet · source · review · register
2026-09-27 published T-046 · $n = 19, 20, 26, 27$
Rectangle-density lower bounds verified at 48 counts in $n = 18 \dots 95$
V3 C3 Lower bound confirmed superseded by T-103, T-104, T-105 and T-106
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · wand125 rectangle bounds 2026-09-28 · packet · packet · source · review · register
2026-09-29 published T-058 · $n = 19, 20, 26, 27$
Rectangle-certificate ceiling α·UB(n) proved for $n = 1$ ..100; B·UB(n) on 64 grid rows
V3 C3 Method limit confirmed
Hosono after Tokoharu, Daniel · wand125 tools 2026 · packet · register
2026-09-29 published T-083 · $n = 19, 20, 26, 27$
$s (n) \geq 1 / 2 + \sqrt{n - ⌊ \sqrt{n} ⌋ + 1 / 4}$ for every nonsquare $8 \leq n \leq 324$
V3 C3 Lower bound confirmed on these cases, superseded by T-103, T-104, T-105 and T-106
Karakuş · Karakuş 2026 · source · register
2026-10-01 published T-068 · $n = 19, 20, 26, 27$
Rectangle-density lower bounds verified at 34 counts in $n = 19 \dots 95$
V3 C3 Lower bound confirmed on these cases, superseded by T-103, T-104, T-105 and T-106
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-10-01 · packet · source · review · register
2026-10-01 published T-074 · $n = 19, 20, 26, 27$
Rectangle-density lower bounds replayed at 31 counts in $n = 19 \dots 95$
V3 C3 Lower bound confirmed on these cases, superseded by T-103, T-104, T-105 and T-106
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-10-01 · packet · packet · source · review · register
2026-10-02 published T-077 · $n = 20$
Rectangle-density lower bounds replayed at $n = 20$ , 42 and 70
V3 C3 Lower bound confirmed superseded by T-104
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-10-02 · packet · packet · source 1 · source 2 · review 1 · review 2 · register
2026-10-06 published T-100 · $n = 19$
Mixed rectangle-measure lower bound verified at $n = 19$ , past the best 18-square packing
V3 C3 Lower bound confirmed superseded by T-103
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds finer net 2026-10-06 · packet · source · review · register
2026-10-06 published T-103 · $n = 19$
Mixed rectangle-measure lower bound verified at $n = 19$ , on the finest declared net yet
V3 C3 Lower bound confirmed
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds check2 2026-10-06 · packet · source · review · register
2026-10-06 published T-104 · $n = 20$
Mixed rectangle-measure lower bound verified at $n = 20$ , on a declared net
V3 C3 Lower bound confirmed
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds check2 2026-10-06 · packet · source · review · register
2026-10-06 published T-105 · $n = 26$
Mixed rectangle-measure lower bound verified at $n = 26$ , on a declared net
V3 C3 Lower bound confirmed
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds check2 2026-10-06 · packet · source · review · register
2026-10-06 published T-106 · $n = 27$
Mixed rectangle-measure lower bound verified at $n = 27$ , on a declared net
V3 C3 Lower bound confirmed
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds check2 2026-10-06 · packet · source · review · register
2026-10-07 published T-124 · $n = 20$
Reported non-strict local minima for 178 source configurations
V0 C0 Restricted optimality recorded
Daniel after Couzo · Daniel exact and local reports 2026 · packet · register
2026-10-08 published T-233 this result · $n = 19, 20, 26, 27$
Mixed rectangle-measure lower bounds reported at $n = 19, 20, 26, 27$ , on a 2,073-direction net
V0 C1 Lower bound reviewed
Hosono after Tokoharu and Levy · wand125 fine-net lower bounds 2026-10-08 · packet · packet · register
2026-10-12 published T-261 · $n = 19, 20, 26, 27$
Reported grade-C local minima for 233 source configurations of field degree at most 4
V3 C1 Restricted optimality incomplete
Daniel after Schadt, Ellsworth, Levy · Daniel exact and local reports 2026-10-12 · packet · packet · register
2026-10-16 published T-194 · $n = 19$
Fitzharding reports a Lean proof that Wainwright's packing is optimal, $s (19) = 3 + 4 \sqrt{2} / 3$
V0 C1 Optimality reviewed
Fitzharding after Levy, Ahmed · Fitzharding n19 Lean 2026 · packet · source · review · register

Links

On this site: Case record, $n = 19$ · Frontier row, $n = 19$ · Case record, $n = 20$ · Frontier row, $n = 20$ · Case record, $n = 26$ · Frontier row, $n = 26$ · Case record, $n = 27$ · Frontier row, $n = 27$ · T-233 in the results table
Issues: Issue #446

On GitHub, at main

Register: T-233 in results.yaml, line 33124
Evidence: E-wand125-fine-net-446-n19-n20-n26-report · E-wand125-fine-net-n27-5655-followup-report
Proofs and certificates: certificate certificates · certificate reported-n27-followup.json
Sources: wand125 fine-net lower bounds 2026-10-08 (its own site, retained copy)
Source packet: resources/web/wand125-fine-net-lower-bounds-2026-10-08/README.md · resources/web/wand125-fine-net-lower-bounds-446-release-2026-10-08/README.md
Artifacts: 27 artifacts and controls in 12 directories. Complete artifact list in the result entry. docs/project/reviews packing/benchmarks/measure-verifier/census-mixed/wand125-fine-net-lower-bounds-446-release-2026-10-08 packing/devtools packing/resources/web/wand125-fine-net-lower-bounds-2026-10-08 packing/resources/web/wand125-fine-net-lower-bounds-446-release-2026-10-08 packing/resources/web/wand125-fine-net-lower-bounds-446-release-2026-10-08/acquisition packing/resources/web/wand125-fine-net-lower-bounds-446-release-2026-10-08/receipts packing/resources/web/wand125-fine-net-lower-bounds-446-release-2026-10-08/release/certificates/mixed_n19_L48275 packing/resources/web/wand125-fine-net-lower-bounds-446-release-2026-10-08/release/certificates/mixed_n20_L49125 packing/resources/web/wand125-fine-net-lower-bounds-446-release-2026-10-08/release/certificates/mixed_n26_L5555 packing/resources/web/wand125-fine-net-lower-bounds-446-release-2026-10-08/release/certificates/mixed_n27_L5655 packing/resources/web/wand125-fine-net-lower-bounds-446-release-2026-10-08/review/review-2026-10-23
Case file: frontier/n-019.md (verified lower, verified upper, reported lower, reported upper) · frontier/n-020.md (verified lower, verified upper, reported lower, reported upper) · frontier/n-026.md (verified lower, verified upper, reported lower, reported upper) · frontier/n-027.md (verified lower, verified upper, reported lower, reported upper)

T-233: Mixed rectangle-measure lower bounds reported at n=19,20,26,27n=19,20,26,27, on a 2,073-direction net

The cases

Results on these cases

Links

T-233: Mixed rectangle-measure lower bounds reported at $n = 19, 20, 26, 27$ , on a 2,073-direction net