=open
Proven
- exact
Citation record n-020
lowerHosono after Tokoharu, Levy et al. 2026, GitHub (confirmed T-104)
Open
- optimality
Bounds
- Proved by
- Hosono 2026
- Kind
- counting
- Scope
- Unrestricted unit-square packing with independent rotations and disjoint interiors.
- Note
- Hosono's square-packing-bounds (6 October 2026) reports from a density of 327 uniform rectangles of total mass 1999999/100000, on a net the certificate declares: core side 1999/2000 and 832 half-angle tangents of step 1/2006, 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 49/10 the record reported (T-077). sqverify-fast, this repository's clean-room measure verifier, decided it here at all 832 directions on 6 October 2026.
- Source
- [wand125 mixed bounds check2 2026-10-06]
- Evidence
E-n020-wand125-mixed-4905-report
The reported value, verified here.
= 0.095
Verified upper minus verified lower.
Results in the register
T-007 V0 C1 Nagamochi · 2026-08-31 · 321 cases
for
T-020 V3 C3 Levy after Burns, Massaccesi · 2026-09-04 · n = 19–21
for
Claim and records
- Claim
- , and , 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 and 1 + sqrt(14) = 4.7416... at -- 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 , +0.194449 at and +0.058343 at , 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 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 against T-019's +0.0842, the largest single-case movement in the register; and at and 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
T-021 V3 C3 Levy after Burns, Massaccesi · 2026-09-05 · n = 20, 21
for
Claim and records
- Claim
- and , from this project's weighted fractional unavoidable-set certificate at container side 97/20 = 4.85. Both sizes held 24/5 = 4.80 from T-020 earlier the same week in this register's verified fields; the movement is +0.05 at each. The certificate does not reach : its total mass is 19848723/1000000 = 19.848723, above nineteen, so Condition 2 gives it and upward and T-020's 24/5 rung, retained beside it, still carries .
The two sizes take no monotonicity step, for the reason T-020 gives: only Condition 2 mentions n among the five conditions, so an atom set of mass M certifies its side for every integer strictly above M. From on the register already holds 5, so the certificate is true there and weaker.
Where the rung came from is worth the record. A pre-registered bisection of [24/5, 9977/2000] ran four rungs unattended. The uniform grid walled at this side -- its restricted optimum crossed twenty at round 31 of 32 and stood at 20.000439 with placements still violated -- while a second site set, the 24/5 certificate's own 2260 atoms scaled by 97/96 and unioned with the grids, converged below twenty at the same side. The certificate is the second construction's; the first construction's crossing is why H-062 asks for two. - Significance
- Scored at S3 by the calibration note T-020 wrote for exactly this case: "Further sizes from the same generator, absent a new technique or a case that changes character, belong at S3." This is the same generator at the same two sizes, one rung higher, and neither size changes character at 4.85. What it adds beyond a rung is a measurement rather than a theorem, and the measurement is registered as such: the m = 5 covering wall is bracketed to [97/20, 39/8] -- a certificate at 4.85, crossings above twenty on both constructions at 4.875 -- which is the first bracket this project has put around a covering wall, and it sits far below the method's ceiling of 4.9885 rather than at it. That bears on planning, not on the strength of this claim.
- Novelty
- apparently-novel Not found in the recorded search, subject to its stated gaps
- Records
T-045 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-09-29 · 15 cases
Rectangle-density lower bounds replayed at 15 counts in
T-046 V0 C0 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-09-29 · 48 cases
Rectangle-density lower bounds reported for 48 counts in
T-058 V3 C3 Hosono after Tokoharu, Daniel · 2026-09-29 · 100 cases
Rectangle-certificate ceiling
α·UB(n)proved for ..100;B·UB(n)on 64 grid rowsT-068 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-01 · 34 cases
Rectangle-density lower bounds verified at 34 counts in
T-074 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-02 · 31 cases
Rectangle-density lower bounds replayed at 31 counts in
T-077 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-03 · n = 20, 42, 70
Rectangle-density lower bounds replayed at , 42 and 70
Claim and records
- Claim
- Three rectangle-density certificates in wand125/square-packing-bounds, raised on 2 October 2026, prove = 4.9, = 6.8275 and = 8.6275. Each raises the certificate T-068 reports at its count, which T-074 replayed, by 0.0025 to 0.0125.
Each is an exact nonnegative rational density on rectangles, D4-expanded, of mass n - 1/100, such that the shrunken core of every rotated unit square at each of 201 net directions captures mass at least one. The certificates were built with Tokoharu's solver, their weights scaled by one exact factor each to that mass. The same revision raised four more rungs, at , 77, 91 and 93, which are below what this record holds there: the exact values and , and the same revision's mixed certificates at and 92, the latter carried to (T-075).
Each passed a complete 201-direction replay here of Tokoharu's unchanged verify.cpp, in two cloud batches on 3 October 2026 whose receipts were merged into the packet on 6 October, and each replay reproduced the upstream accepting run's node count, leaf count and lower bound at every direction: confirmed, reproduced with the producer's code. The inputs were regenerated by this repository's exact preflight, which checks that each is the input the upstream accepting run recorded and checks the exact mass, net, smoothing and axis-event premises.
At and 42 the values raised the verified lower bound, from T-074's 1959/400 and 1363/200, and later on 6 October T-104's check2 certificate raised it again at and T-090's mixed certificate at ; at the mixed certificate of T-091 holds more.
Each was also decided by sqverify-fast, this repository's clean-room measure verifier, at all 201 net directions at Tokoharu's threshold 10001/10000 in the census of 3 October, and two mutants of each scaled below that threshold were refused on 6 October: confirmed, independently re-implemented as well. It shares no code with the source's checker and runs the same method, a second implementation and not a second method.
Hosono after Tokoharu and Levy, square-packing-bounds. No issue requests these certificates; the import of 2 October took them in from the source's own commits. The source says parts of the work were produced with AI assistance under human direction. - Significance
- Raised the verified lower bound at and 42, by 0.0025 and 0.0125 over T-074's replayed certificates, and the strongest rectangle-density lower bounds on record at all three counts. Raised rungs from one generator, as T-068's were, at S3; the 2 October review of the afternoon certificates proposed S3. Confirmed on 11 October beside T-068 and T-074.
- Novelty
- previously-published Present in an identified source
- Records
n = 20n = 42n = 70registerevidence 1evidence 2evidence 3evidence 4evidence 5source 1source 2review 1review 2
T-083 V3 C3 Karakuş · 2026-10-02 · 301 cases
for every nonsquare
T-085 V3 C3 Karakuş; Vlasenko · 2026-10-02 · 315 cases
Nagamochi 2005, Lemma 1 is false for every container with and
T-104 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-06 · n = 20
Mixed rectangle-measure lower bound verified at , on a declared net
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 = 4.905.
The certificate is a density of 327 uniform rectangles in D4 orbits, and no point mass, of total mass 1999999/100000, on the net T-099's certificate declares: core side 1999/2000 and 832 half-angle tangents of step 1/2006. Since 1999/2000 (1 + 1/2006) = 4011993/4012000 < 1, and the last tangent 831/2006 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 832 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 49/10 = 4.9 the record reported and verified at , the source's rectangle certificate rect_n20_L49 (T-077), by 0.005.
The certificate was decided here on 6 October 2026 by sqverify-fast, this repository's clean-room measure verifier, at all 832 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 679 and 831, 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 , by 0.005 above T-077, 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
T-124 V0 C0 Daniel after Couzo · 2026-10-07 · 178 cases
Reported non-strict local minima for 178 source configurations
upper: replayed here; lower: replayed here
—
not rigid, numerically checked, numerical multiprecision
Evidence: E-translation-escape-not-rigid
Scope
Square 15 of the retained witness (witness id 16) translates 1 along (0, 1) with the packing still valid, so the configuration admits a non-trivial feasible motion; 5 of its 20 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.
- 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 - Blocker (source evidence): The finer-net lower-bound report awaits complete maintained native capture, whole-net controls and independent result review.
E-wand125-fine-net-lower-bounds-446-report
17 evidence entries
E-n020-wand125-mixed-4905-sqverify-fast-replay, E-n020-wand125-mixed-4905-report, E-n020-wand125-rect-48975-sqverify-fast-replay, E-n020-wand125-rect-49-sqverify-fast-replay, E-wand125-rectangle-2026-10-02-source-replay, E-wand125-rectangle-2026-10-02-report, E-wand125-rectangle-2026-10-01-source-replay, E-wand125-rectangle-source-replay, E-wand125-rectangle-2026-10-01-report, E-wand125-rectangle-report, E-kingbird-upper-register, E-nagamochi-lower, E-basic-grid-upper, E-green-ds7-theorem10-reported-lower, E-n020-fractional-certificate-97-20, E-n020-evand-point-cover-4886-report, E-wand125-fine-net-lower-bounds-446-report
- [wand125 mixed bounds check2 2026-10-06] lower bound proof
- [wand125 rectangle bounds 2026-10-02] lower bound proof
- [wand125 rectangle bounds 2026-10-01] lower bound proof
- [wand125 rectangle bounds 2026] lower bound proof
- [Kingbird] record catalogue
- [Nagamochi 2005] lower bound proof
- [Friedman DS7] survey
- [wand125 fine-net lower bounds 2026-10-08] lower bound proof
— open
External intake, 2026-10-06. Hosono’s
check2 source
reports (T-104), from a density of 327 rectangles of total
mass , on a net the certificate declares: core side and
832 half-angle tangents of step . Since ,
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 (T-077), reported and verified, by . 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.
Hosono’s README says parts of the work were produced with AI assistance under human
direction.
External report, 2026-10-05. Daniel’s
repository reports that 20
unit squares need a side above , the side of
Wainwright’s packing of 19, so that . The certificate is a point cover of
side with total mass ,
accepted by his zmx2 and zm_mixed.py. It is below the verified and reported bounds
below, which already exceed ; the source keeps it as an independent
confirmation. It asks for no work, so it is not registered and was not replayed here.
The source’s CREDITS.md says the work was produced by Claude (Anthropic) in a single
session under human direction.
External intake, 2026-10-02. Hosono’s rectangle-density source reports , with total mass , 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 check2 certificate above superseded it later on 2026-10-06. Hosono’s README says parts of the work were produced with AI assistance under human direction.
External intake, 2026-10-01. Hosono’s rectangle-density source reports a direct certificate for this case, whose reported bound the 2026-10-02 intake above raises, with total mass , 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-02 intake above. Hosono’s README says parts of the work were produced with AI assistance under human direction.
External intake, 2026-09-27. Hosono’s rectangle-density source reports a direct certificate for this case, whose reported bound the 2026-10-01 intake above raises, with total mass , 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. Hosono’s README says parts of the work were produced with AI assistance under human direction.
Open. The best known packing gives . The verified lower bound is
, from Hosono’s check2 certificate on a declared net
(T-104, 2026-10-06, V3/C3), leaving a gap of . It superseded the source’s
rectangle-density certificate of 2 October at (T-077, replayed here on
2026-10-03 and entered on 2026-10-06), the verified lower bound earlier that day.
Its certificate of 1 October, (T-074, replayed here on
2026-10-02), held the field until then; its certificate of 27 September,
(T-045), held it earlier on 2 October, and had superseded this
repository’s weighted fractional unavoidable-set certificate at (T-021,
2026-09-05), which had raised the earlier verified bound (T-020) by
. The external reports below are recorded separately from these verified bounds.
The packing
The record catalogue does not picture : no arrangement has ever been found that beats the trivial grid, so the grid is still the best known packing. That is a statement about what has been searched, not a proof.
The lower bound
The earlier external report, [Friedman DS7], gives the lower-bound expression for (approximately ). 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. Inherited at n=20 by monotonicity. 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. Hosono’s certificates above have since replaced it in the reported field, and since their replays here, from 2026-10-02, in the verified one, where its check2 certificate of 6 October (T-104) now holds it. The source audit compares the exact theorem expressions separately from opaque table decimals.
Until 2026-10-02 the operative bound was the
T-021 certificate at side
: 1680 rationally weighted atoms on a D4-symmetric site set, total mass
, and least covered mass . An exact
event-cell sweep and an interval branch and bound independently decide its conditions
from the retained bytes and agree on that least mass.
Only Condition 2 mentions among the five certificate conditions.
The same atom set therefore certifies its side for every integer above its mass, which
is 20 and upward; neither this case nor its companion needs a monotonicity step.
The companion moved on to the stronger
T-034 certificate at on
2026-09-23, whose mass is above twenty and so does not reach this case, and is now
proved: Daniel’s mixed cover gives (n-021). The
earlier T-020 certificate
at remains valid and still supplies the verified 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. Before those adoptions, the verified field here used Nagamochi’s general closed form, which applies to every :
At , it remains the verified lower bound for 40 of the 65 open cases. Corrected 2 October 2026: it is now the verified lower bound of none of them; Karakuş’s weaker general bound replaced it there (T-083).
What the method can still add here
A certificate for cannot exist above , which at is , so the ceiling lay above the bound this method reached. The certificates on declared nets raise : at the of T-104’s net the ceiling is , which lies above the current . Unlike , no packing binds first: the best known packing here is the trivial grid at . So this method could in principle close the case to within of the upper bound, at that core, and can never reach it.
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-n020-wand125-mixed-4905-sqverify-fast-replay |
replayed here | shared components | V-sqverify-fast (first-party) |
| verified upper | E-basic-grid-upper |
replayed here | independent | V-check-basic-bounds (first-party) |