n = 41 open ★=
Proven
- new result
- exact
Citation record n-041
lowerwand125 after Tokoharu, Levy et al. 2026, GitHub (confirmed T-111)
upperSchadt 2025, Squares in Squares (confirmed T-101)
Open
- optimality
Bounds
6.92669309…
6.92669309446880- Found by
- Thomas Schadt 2025
- Construction
- annealing
- Source
- [Kingbird]
- Evidence
E-kingbird-upper-register
Minimal polynomial, degree 42
6.92669309446881
The reported value, verified here.
- Proved by
- wand125 2026
- Kind
- counting
- Scope
- Unrestricted unit-square packing with independent rotations and disjoint interiors.
- Note
- wand125'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 wand125 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 wand125 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 wand125 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 wand125 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 wand125 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 wand125 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ş; chelokot · 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 wand125 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.
wand125 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. - Composition
- One primary certificate on its reported entry and its replay entry. The replay is sqverify-fast at all 416 directions of the net the retained candidate declares: one interval-certified method, replayed here by an implementation that shares the producer's components, C3, on the census route, whose conditions for a declared net this certificate meets. The source's own check is a copy of the same crate, and its C++ checker was run here at sampled directions only, so no second implementation and no second method stands beside it.
- Next rung
- V4 and C4 need two adversarial AI reviews of this result by distinct reviewers and a human oversight record; one is retained. A complete run of the source's C++ checker over all 416 directions (devtools.audit_wand125_declared_net cpp-sample, about 37 CPU-hours at the samples' rate) would add a check that shares no code with sqverify_fast beside the rung, though it is the producer's own code.
- 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
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.
16 evidence entries
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 certificate, 2026-10-06. Evan 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 (T-101). Until then the verified upper bound was the trivial
grid bound .
External intake, 2026-10-06. wand125’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.
wand125’s README says parts of the work were produced with AI assistance under human
direction.
External intake, 2026-10-01. wand125’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. wand125’s README says parts of the work were produced with AI assistance under human direction.
External intake, 2026-09-28. wand125’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. wand125’s README says parts of the work were produced with AI assistance under human direction.
External intake, 2026-09-27. wand125’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. wand125’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 wand125’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 exact certificate
Evan 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. Evan 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: 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.”
The verified upper bound and the printed side now 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 Thomas Schadt in 2025, via simulated annealing. Its side length is algebraic of degree 42 over .
The lower bound
The verified lower bound is , from wand125’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-evand-exact-ceilings-2026-10-05-exact-replay |
replayed here | independent | V-sqpack-verify, V-check-rational-witness-independent (first-party); V-evand-exact-certificates (first-party, premises) |
| verified upper | E-evand-exact-ceilings-2026-10-05-source-replay |
replayed here | producer’s code | V-evand-verify-cert-py, V-evand-verify-cert2-py (external); V-evand-exact-certificates (first-party, premises) |