T-179: Linear-measure lower bound $s (n) \geq 306 / 25 = 12.24$ for $n = 145 \dots 149$ , reported

V0 C1 Lower bound reviewed

2026-10-13 published · Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 5 cases, $n = 145$ to 149

A measure of points, segments and rectangles that wand125/square-packing published on 13 October 2026, reported on no issue, is reported to prove $s (145) \geq 306 / 25$ = 12.24. Its mass is below 145, and a packing of 146 to 149 squares contains one of 145, so it also gives $s (146), s (147), s (148), s (149) \geq 306 / 25$ : five counts in all. At $n = 150$ and beyond the record already holds more.

The measure, mixed_n145_L1224, is 594 point, 1,541 segment and 9 rectangle orbits under D4, with exact rational geometry, of total mass 14499999/100000, at core side 9977/10000 on 201 net half-angles of step 83/40000: the measure kind, net and checker of T-080 and T-144. The source reports it accepted at all 201 net angles, the axis included, by code/unified_linear_verify.cpp, byte for byte T-080's checker, and a complete replay of its tarball on a fresh machine.

The value exceeds Green's reported 12.2138669477... at $n = 145$ to 148, by more than 0.0261, and Nagamochi's 12.2249721603... at $n = 149$ , and the verified Karakus strip bounds at all five.

Here the T-080 route's readers accepted its exact premises: the measure, its D4 invariance, digest, net, centre domains, checker and code identity, the 201 records, the source's audit, the proof bundle's 810 files and every angle's input. Two angles replayed here by the source's replay function and unchanged checker, from this repository's retained copies, returned the certificate's own records: a diagnostic, not a replay. No complete replay has run here, so the value stands as reported.

Hosono after Tokoharu and Levy, square-packing. 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: if a complete replay passes, it raises the reported and verified lower bounds at five counts, $n = 145$ to 149, past Green's reported values and Nagamochi's closed form, by T-080's certificate kind, net and checker at a new size, with no new technique, at S3 as T-080 and T-144 are.
Composition: One reported certificate on its reported entry. $n = 146$ to 149 take it directly, its mass being below them, so no step is added. A replay here would run the source's checker unchanged, as T-080's did: one interval-certified method, and no second implementation stands beside it.
Next rung: C3 needs a complete replay of all 201 angles by the T-080 route, with the certificate registered in devtools.audit_wand125_linear so that linear-replay writes resumable receipts, the route's linear-control receipt and a review that reads this certificate, as the 2 October review read T-080's. The two-angle sample prices the replay and control at about 37 CPU-hours on a loaded host (the author's own replay suggests up to about 64). It waits for an owner budget in think-u0av.
Unfinished confirmations: C3 (think-u0av): a complete replay of all 201 angles by the T-080 route, with the certificate registered in devtools.audit_wand125_linear so that linear-replay writes resumable receipts, the route's linear-control receipt and a review that reads this certificate, as the 2 October review read T-080's. About 36.97 CPU-hours, up to about 64 (priced 2026-10-14).
Novelty: previously-published Present in an identified source

The cases

This result concerns 5 cases, too many to draw one by one. Each is listed with the film’s bounds, the proved lower bound and the best known side, and links to its case record, where its packing and number line are drawn.

n	Proved lower	Best known	Gap	Status	Records
145	12.043396	12.535534	0.49213752…	open=	frontier n-145.md
146	12.086630	12.583783	0.49715196…		frontier n-146.md
147	12.129703	12.656855	0.52715089…		frontier n-147.md
148	12.172617	12.656855	0.48423671…		frontier n-148.md
149	12.215374	12.707107	0.49173226…		frontier n-149.md

Results on these cases

13 results in the register on these cases, oldest first

2005 published T-007 · 5 of these cases
$s (n) \geq min (⌈ \sqrt{n} ⌉, \sqrt{n - 2 ⌊ \sqrt{n} ⌋ + 1} + 1)$ for $4 \leq n \leq 324$
Lower bound incomplete on these cases, superseded by T-083 and T-180 (reported)
Nagamochi · Nagamochi 2005 · source · register
2026-09-04 published T-085 · 5 of these cases
Nagamochi 2005, Lemma 1 is false for every container with $a > 3$ and $b > 2$
Correction confirmed
Karakuş; Vlasenko · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register
2026-09-29 published T-083 · 5 of these cases
$s (n) \geq 1 / 2 + \sqrt{n - ⌊ \sqrt{n} ⌋ + 1 / 4}$ for every nonsquare $8 \leq n \leq 324$
Lower bound confirmed
Karakuş · Karakuş 2026 · source · register
2026-10-05 published T-101 · 5 of these cases
Exact certificates of 77 catalogue packings: s(n) ≤ S', 1.2e-16 to 9.8e-15 above each side
Upper bound confirmed
Daniel after Couzo, de Winter, Ellsworth, Levy · evand exact optima 2026-10-05 · packet · register
2026-10-08 published T-125 · case 146
Complete rational construction reports at 25 counts
Upper bound confirmed superseded by T-187
Xu · ry-xu square packing 2026 · packet · register
2026-10-10 published T-146 · case 146
Exact rational certificates at fifteen counts from Daniel's regularized record lists
Upper bound confirmed on these cases, superseded by T-187
Daniel after Xu, Chaoweeraprasit, Polkovskyi, Levy · Daniel regularized lists 2026-10-10 · packet · register
2026-10-11 published T-150 · case 146
Exact rational refinements of Xu's packings of 146 and 261 squares
Upper bound confirmed superseded by T-187
Barnett after Xu, Daniel, Levy · Barnett refinements 2026-10-11 · packet · register
2026-10-12 established T-155 · cases 145, 147, 148, 149
Exact regularized sides at 59 counts, 5.4e-20 to 9.9e-15 below the ceilings they replace
Upper bound confirmed
Levy after Daniel · register
2026-10-12 published T-168 · case 146
A further exact refinement of Xu's packing of 146 squares, after Barnett's
Upper bound confirmed superseded by T-187
PingYou Ltd after Xu, Barnett, Daniel, Levy · PingYou n146 refinement 2026-10-12 · packet · register
2026-10-13 published T-174 · case 146
Tighter certificates at 68 counts from PingYou Ltd, of others' packings and its own
Upper bound confirmed on these cases, superseded by T-187
PingYou Ltd after Friedman, Ellsworth, Daniel, Xu, Barnett, Couzo, Ostashev, Chaoweeraprasit, Gupta, Fang, Polkovskyi, Levy · PingYou PR 574 certificates 2026-10-13 · packet · register
2026-10-13 published T-179 this result · 5 of these cases
Linear-measure lower bound $s (n) \geq 306 / 25 = 12.24$ for $n = 145 \dots 149$ , reported
Lower bound reviewed
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 linear n145 2026-10-13 · packet · register
2026-10-13 published T-180 · 5 of these cases
Closed-form lower bound $s (N) \geq a (N)$ for every non-square $N \geq 49$ , reported
Lower bound reviewed
Hosono · wand125 closed form 2026-10-14 · packet · packet · register
2026-10-14 published T-187 · case 146
A smaller packing of 146 squares from Daniel's chain search, started from Xu's packing
Upper bound confirmed
Daniel after Xu · Daniel n146 2026-10-14 · packet · register

Links

On this site: The frontier survey · T-179 in the results table

On GitHub, at main

Register: T-179 in results.yaml, line 24190
Evidence: E-wand125-linear-n145-1224-report
Proofs and certificates: certificate completion-audit.json
Sources: wand125 linear n145 2026-10-13
Source packet: resources/web/wand125-linear-n145-2026-10-13/README.md
Artifacts: 7 artifacts and controls
resources/web/wand125-linear-n145-2026-10-13/README.md resources/web/wand125-linear-n145-2026-10-13/acquisition/sources.json resources/web/wand125-linear-n145-2026-10-13/square-packing/problems/square-lower-bounds/certificates/mixed_n145_L1224/completion-audit.json resources/web/wand125-linear-n145-2026-10-13/receipts/linear-premises.json resources/web/wand125-linear-n145-2026-10-13/receipts/linear-sample-diagnostic.json devtools/fine_net_followup.py devtools/audit_wand125_linear.py
Case file: each case’s file is linked from its row above

T-179: Linear-measure lower bound s(n)≥306/25=12.24s(n)≥306/25=12.24 for n=145…149n=145…149, reported

The cases

Results on these cases

Links

T-179: Linear-measure lower bound $s (n) \geq 306 / 25 = 12.24$ for $n = 145 \dots 149$ , reported