As published
=open
Proven
- exact
Citation record n-041
lowerHosono after Tokoharu, Levy et al. 2026, GitHub (confirmed T-111)
upperSchadt 2025, Squares in Squares (confirmed T-155)
Open
- optimality
Bounds
6.92669309…
6.92669309446880- Found by
- Schadt 2025
- Construction
- annealing
- Source
- [Kingbird]
- Evidence
E-kingbird-upper-register
Minimal polynomial, degree 42
6.92669309…
6.92669309446881The reported value, verified here.
- 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 376 uniform rectangles of total mass 4099999/100000, on a net the certificate declares: core side 999/1000 and 416 half-angle tangents of step 1/1001, 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 169/25 the record reported (T-068). sqverify-fast, this repository's clean-room measure verifier, decided it here at all 416 directions on 6 October 2026.
- Source
- [wand125 mixed bounds check2 2026-10-06]
- Evidence
E-n041-wand125-mixed-6775-report
The reported value, verified here.
0.15169309…
Verified upper minus verified lower.
Results in the register
T-007 V0 C1 Nagamochi · 2026-08-31 · 321 cases
for
T-044 V3 C3 Hosono after Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-09-29 · 17 cases
Weighted point lower bounds for ten counts in , plus seven from the same files
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-070 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-02 · 25 cases
Rectangle-density lower bounds replayed at 25 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-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-101 V3 C3 Daniel after Couzo, de Winter, Ellsworth, Levy · 2026-10-06 · 77 cases
Exact certificates of 77 catalogue packings:
s(n) ≤ S',1.2e-16to9.8e-15above each sideT-111 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-06 · n = 41
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 = 6.775.
The certificate is a density of 376 uniform rectangles in D4 orbits, and no point mass, of total mass 4099999/100000, on the net T-096's certificate declares: core side 999/1000 and 416 half-angle tangents of step 1/1001. Since 999/1000 (1 + 1/1001) = 500499/500500 < 1, and the last tangent 415/1001 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 416 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 169/25 = 6.76, the source's rectangle certificate rect_n41_L676 and the reported (T-068) and verified (T-074) lower bound at before it, by 0.015.
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, 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 409 and 415, 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.015 above T-074, 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-155 V3 C3 Levy after Daniel · 2026-10-12 · 59 cases
Exact regularized sides at 59 counts,
5.4e-20to9.9e-15below the ceilings they replaceT-202 V0 C0 Hosono after Tokoharu and Levy · 2026-10-17 · n = 41
Mixed rectangle-measure lower bound reported, on a 2,073-direction declared net
Claim and records
- Claim
- A rectangle measure of wand125/square-packing, published on 16 October 2026 and reported in jlevy/squares#446, is reported to prove = 6.8025.
The certificate, mixed_n41_L68025, is a density of 629 uniform rectangles in D4 orbits, and no point mass, of total mass 4099999/100000, on a net its 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 source reports every such core capturing mass at least one at all 2,073 directions, by sqverify-proof-net, its copy of this repository's sqverify_fast changed to read the declared net, in two complete runs, and a control with every mass scaled by 197/200 refused at 32 sampled directions.
The value is above T-111's 271/40 = 6.775, the verified and reported lower bound at , by 11/400.
Here the maintained readers accepted its exact mass, declared-net and check2 premises from the retained release asset. No complete replay has run here, so the value stands as reported.
wand125 after Tokoharu and Levy, square-packing. The source says parts of the work were produced with AI assistance under human direction. - Significance
- Scored as a claim: if a complete replay passes, it is the strongest lower bound on record at , 11/400 above the reported lane, by the certificate kind and declared net of T-132, T-142 and T-143, with no new technique, at S3 as T-176 to T-178 are.
- Novelty
- previously-published Present in an identified source
- Records
upper: replayed here; lower: replayed here
—
not rigid, numerically checked, numerical multiprecision
Evidence: E-translation-escape-not-rigid
Scope
Square 6 of the retained witness (witness id 7) translates 0.085821 along (0.707107, -0.707107) with the packing still valid, so the configuration admits a non-trivial feasible motion; 4 of its 41 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.
Regularized by the Squares Project with Daniel's regularizer (evand/square-packing, MIT), with the project's modifications: same-side exact re-solve (devtools.regularize_same_side). A drawing of T-155's packing at the witness's own side. Its exact side is registered as T-155, the upper bound it proves; the drawing itself is no further result.
17 evidence entries
E-regularized-bounds-2026-10-12-exact-decision, E-evand-exact-ceilings-2026-10-05-report, E-evand-exact-ceilings-2026-10-05-exact-replay, E-evand-exact-ceilings-2026-10-05-source-replay, E-n041-wand125-rect-676-sqverify-fast-replay, E-n041-wand125-mixed-6775-sqverify-fast-replay, E-n041-wand125-mixed-6775-report, E-wand125-rectangle-2026-10-01-source-replay, E-wand125-rectangle-2026-09-28-source-replay, E-wand125-rectangle-2026-10-01-report, E-wand125-rectangle-2026-09-28-report, E-wand125-rectangle-report, E-wand125-point-monotone-report, E-wand125-point-source-replay, E-kingbird-upper-register, E-nagamochi-lower, E-basic-grid-upper
- [evand exact optima 2026-10-05] formal certificate
- [wand125 mixed bounds check2 2026-10-06] lower bound proof
- [wand125 rectangle bounds 2026-10-01] lower bound proof
- [wand125 rectangle bounds 2026-09-28] lower bound proof
- [wand125 rectangle bounds 2026] lower bound proof
- [wand125 point bounds 2026] lower bound proof
- [Kingbird] record catalogue
- [Nagamochi 2005] lower bound proof
- [Friedman DS7] survey
— open
Exact regularized certificate, 2026-10-12. This project’s regularization pass, Daniel’s exact solver and regularizer run here on this register’s witness, produced an exact rational packing of this arrangement, decided here over by two exact checkers: it proves , the verified upper bound (T-155) rounded up at 36 places, which the record still prints as . Until then the verified upper bound was exactly , the side of Daniel’s exact certificate of this packing rounded up at the printed precision (T-101).
Exact certificate, 2026-10-06. Daniel’s
square-packing published
on 5 October 2026 an exact rational certificate of this packing, decided here over
by two exact checkers that share no code with each other or with the
source, and by the source’s own two run here: it proves ,
the verified upper bound from 6 to 12 October 2026 (T-101). Until then the verified
upper bound was the trivial grid bound .
External intake, 2026-10-06. Hosono’s
check2 source
reports (T-111), from a density of 376 rectangles of total
mass , on a net the certificate declares: core side and
416 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 reported (T-068) by . 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, 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 intake, 2026-10-01. Hosono’s rectangle-density source reports , since superseded (T-111), 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 verified until 2026-10-06, when the certificate above superseded it in both lanes. Hosono’s README says parts of the work were produced with AI assistance under human direction.
External intake, 2026-09-28. 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.
External intake, 2026-09-27. Hosono’s rectangle-density source reports a direct certificate for this case, whose reported bound the 2026-09-28 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.
External intake, 2026-09-22. Hosono’s retained source reports and identifies the monotone consequence at . The complete exact n40 replay verifies the source premise, so monotonicity verifies the n41 bound.
Open. The best known packing gives , and the verified lower bound
is , from Hosono’s check2 certificate on a declared net
(T-111, 2026-10-06, V3/C3), which superseded its rectangle-density certificate of 1
October at (T-074), leaving a gap of about .
The regularized exact certificate
This project’s regularization pass of 11 and 12 October 2026 ran Daniel’s exact
solver and regularizer
(evand/square-packing, MIT, vendored here)
on this register’s witness for this count, with the conservative angle policy and
coincide placement, and this project’s same-side re-solve then fixed the result’s
tight contacts over at the witness’s own side.
The result is an exact rational packing of the same 41 squares in a square of side
(rounded up at 36 places), below the
verified upper bound the record held before, and below the side of Daniel’s certificate of this packing (T-101): it is the witness’s own side.
Measured against the witness under the box’s eight symmetries, its squares pair one to
one with the witness’s; 5 move by more than , the largest by , and none
turns by more than as a sine.
It redraws the packing visibly, and is drawn only once the regularized layer admits it
under the regularization policy.
Each pair and each wall is decided over twice, by sqpack’s exact
separating-axis test and by an independent checker that shares no code with it, and both
accept it; both refuse it with its tightest pair pushed into overlap and with its box
shrunk past its least clearance (certificate).
The same two checkers accepted it in the run that made it, so this is a reproduction
with the producer’s code.
That proves , the verified upper bound
(T-155) rounded up at 36 places.
The exact side, a rational, is the exact form of the case’s verified_upper_bound,
which prints it as , the decimal it printed before and an upper
display of it. It says nothing about optimality, and the packing stays its finders’.
The earlier exact certificate
Daniel’s
square-packing published
on 5 October 2026 exact rational certificates of the packings this register lists as
best known, solved from its own witnesses, and offered those that do not lower a printed
side as a replay of the existing bounds, asking for nothing to be registered from them.
The certificate for this count holds the same 41 squares, each a rational centre and a
rational , in a square of side ,
above the side the Kingbird catalogue prints, . Square for
square, its pose lies within of the binary64 pose the atlas pictures for this
count. 2 squares move by more than , all of them squares the source lists as
carrying no force; every other square’s centre rounds to the witness’s. Daniel’s
solver moves the binary64 pose to a nearby exact KKT point of the problem of minimizing
the side under non-overlap, computed at 80 digits, and rounds it outward to rationals.
This repository decides the certificate exactly.
Converted without rounding, every pair and every wall is decided over
twice, by sqpack’s exact separating-axis test and by an independent checker that
shares no code with it, and the source’s own two checkers, run here as retained, accept
it as well
(receipts).
That proves , the verified upper bound until 12 October
2026: the certificate’s side rounded up at the fourteen decimals the catalogue prints,
as the record writes any certificate of a printed side.
It says nothing about optimality.
On jlevy/squares#375 its author wrote that the solver, its checkers and the batch “were
written with Claude (Anthropic) as a coding and research agent, directed and reviewed by
me.”
Its rounded-up side and the printed side agree to one unit of the printed side’s last place, the precision at which the record compares them. The printed side itself is not certified here: the certificate’s side lies above it.
The packing
Found by Schadt in 2025, via simulated annealing. Its side length is algebraic of degree 42 over .
The lower bound
The verified lower bound is , from Hosono’s check2 certificate of 6
October on a declared net (T-111), decided here by sqverify-fast at every direction
of its net.
Before it, , from its own n41 rectangle-density certificate of
1 October, replayed in full here (T-074); its certificate of 28 September,
(T-070), held the field earlier on 2 October.
Until then it was : the complete n40 exact replay verifies that bound, and
deleting one square from any hypothetical packing proves it for n41 too.
A second interval implementation or generalized native importer would add confirmation
and reuse, but it is not a missing premise of either 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. Nagamochi’s earlier general closed form remains part of the evidence history and applies to every :
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-n041-wand125-mixed-6775-sqverify-fast-replay |
replayed here | shared components | V-sqverify-fast (first-party) |
| verified upper | E-regularized-bounds-2026-10-12-exact-decision |
replayed here | producer’s code | V-sqpack-verify, V-check-rational-witness-independent (first-party); V-register-regularized-bounds (first-party, premises) |