=open
Proven
- exact
Citation record n-051
lowerHosono after Tokoharu, Levy et al. 2026, GitHub (confirmed T-090)
upperXu 2026, GitHub (confirmed T-126)
Open
- optimality
Bounds
7.6903559372884918
- Found by
- Xu 2026
- Construction
- —
- Minimal polynomial, degree 2
- Source
- [ry-xu square packing 2026]
- Evidence
E-ryxu-432-radical-n51-report
7.6903559372884918
The 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 (4 October 2026) reports from a density of 489 uniform rectangles of total mass 5099999/100000, at core side 9977/10000 on 201 net half-angles, accepted there at every angle by its research copy of Tokoharu's verify.cpp at threshold one. It is above the 373/50 this case reported, from the source's mixed_n51_L746 (T-082). sqverify-fast decided it here on 6 October 2026 at all 201 net directions.
- Source
- [wand125 mixed bounds 2026-10-04]
- Evidence
E-n051-wand125-mixed-747-report
The reported value, verified here.
≈ 0.22035593…
Verified upper minus verified lower.
Results in the register
T-007 V0 C1 Nagamochi · 2026-08-31 · 321 cases
for
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-048 V3 C3 Hosono after Daniel, Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-09-29 · n = 50, 51
Claim and records
- Claim
- = 7.4, by Hosono's mixed rectangle-density certificate of 28 September 2026. It exceeds Green's reported 2 sqrt(2) + 101/25 + 3 sqrt(14)/25 = 7.3174260 by more than 0.0825739888. The certificate's mass is below 51 too, so it gives as well.
The certificate is a D4-expanded rectangle density of 553 orbit representatives, total mass 4999999/100000 < 50, core side 9977/10000 and 201 net half-angles of step 83/40000. It is accepted at every oblique net angle by code/mixed_rotated_verify.cpp, a research copy of Tokoharu's verify.cpp that accepts coverage at least 1 instead of 10001/10000 and checks each net node's unit-square centre domain, and at angle zero by exact integer tables.
The source's complete replay was run here on 29 September 2026 on the pinned bundle, with the source's driver and checker unchanged: all 201 directions, each equal to the shipped record. This repository's exact audit checked the premises and the integrity of all 621 bundle files and all 200 oblique inputs. The replay runs the source's own algorithm and is not an independent decision of coverage.
Hosono after Daniel and Tokoharu, square-packing-bounds, the measure resting on Tokoharu's format and checker. The source says parts of the work were produced with AI assistance under human direction. - Significance
- Raised the verified lower bound at by 0.317 over Nagamochi's closed form, and at by 0.236, and stands 0.0826 above Green's reported value at . The two changes to Tokoharu's checker were read and found legitimate on 2026-09-28. A substantive case result at S3. The closed form has been a reported bound since Karakuş's finding (T-085, merged 2026-10-03), so the margins over the verified floor it left, Karakuş's general bound, are larger. Confirmed on 11 October: the mixed certificate, point masses beside rectangle densities, is a kind within Tokoharu's framework, as T-073's linear measure is, and an extension at one count is S3 with the kind noted, as T-073 is; T-047, the framework, holds the S4.
- Novelty
- previously-published Present in an identified source
- Records
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-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-082 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-03 · 22 cases
Mixed rectangle-measure lower bounds verified at 22 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-090 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-05 · 17 cases
Mixed rectangle-measure lower bounds verified at 17 counts in
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-125 V3 C3 Xu · 2026-10-08 · 25 cases
Complete rational construction reports at 25 counts
T-126 V3 C3 Xu · 2026-10-08 · n = 51
Undilated n51 construction over Q(sqrt2)
Claim and records
- Claim
- Complete independently reviewed exact replay, independently re-implemented, confirms the undilated 51-square construction ceiling <= (16+5sqrt(2))/3. This is finite feasibility, not equality with the optimum or the unconfirmed source contact count.
- Significance
- Xu's new 51-square arrangement at its exact side (16 + 5 sqrt 2)/3, about 0.0104 below the ceiling Daniel's certificate of the catalogue packing held (T-101), and the side the case now holds. A new arrangement lowering a case ceiling is a case result, S3, as T-125's rational certificate of the same packing is; the exact closed form is the citable detail and not the claim's weight, where an exact form alone (T-120 to T-123) is S2. No optimum established. Confirmed on 11 October.
- Novelty
- previously-published Present in an identified source
- Records
T-180 V0 C1 Hosono · 2026-10-14 · 264 cases
Closed-form lower bound for every non-square , reported
T-204 V0 C0 Hosono after Tokoharu and Levy · 2026-10-17 · n = 51
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 = 7.5275.
The certificate, mixed_n51_L75275, is a density of 908 uniform rectangles in D4 orbits, and no point mass, of total mass 5099999/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-090's 747/100 = 7.47, the verified and reported lower bound at , by 23/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 , 23/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.025126 along (-0, 1) with the packing still valid, so the configuration admits a non-trivial feasible motion; 9 of its 51 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-theorem9-reported-lower - Priority: Earlier source ceiling 7.70079923541701 from [Kingbird]; full prior geometry and record remain retained in the packet. (Schadt)
17 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-n051-wand125-mixed-747-sqverify-fast-replay, E-n051-wand125-mixed-746-sqverify-fast-replay, E-wand125-rectangle-2026-09-28-source-replay, E-n050-wand125-mixed-740-source-replay, E-wand125-rectangle-2026-09-28-report, E-wand125-rectangle-report, E-kingbird-upper-register, E-nagamochi-lower, E-basic-grid-upper, E-karakus-strip-lower, E-nagamochi-lemma1-counterexample, E-green-ds7-theorem9-reported-lower, E-ryxu-432-radical-n51-report, E-ryxu-432-radical-n51-feasibility
- [ry-xu square packing 2026] upper bound report
- [evand exact optima 2026-10-05] formal certificate
- [wand125 mixed bounds 2026-10-04] lower bound proof
- [wand125 mixed bounds 2026-10-03] lower bound proof
- [wand125 point and mixed bounds 2026-09-28] lower bound proof
- [wand125 rectangle bounds 2026-09-28] lower bound proof
- [wand125 rectangle bounds 2026] lower bound proof
- [Kingbird] record catalogue
- [Nagamochi 2005] lower bound proof
- [Friedman DS7] survey
- [Karakuş 2026] lower bound proof
— open
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 previously proved
, the verified upper bound (T-101). Until then the verified
upper bound was the trivial grid bound .
Verified lower bound, 2026-10-06. sqverify-fast, this repository’s clean-room
measure verifier, decided Hosono’s mixed_n51_L747 (T-090) here at all 201 net
directions of the retained candidate, with two mutants scaled below coverage one refused
(E-n051-wand125-mixed-747-sqverify-fast-replay, V3/C3), so
is the verified lower bound, above by the
that T-070’s replay of rect_n51_L74425 had made it earlier that day, which had
replaced the carried from . It shares no code with the source’s checker,
so it decides coverage a second way with the same method; the source’s own checker was
not run here.
External intake, 2026-10-02. Hosono’s
rectangle-density source
reports the rectangle certificate rect_n51_L74425 at side , since
superseded (T-082, T-090), with total mass , accepted by
Tokoharu’s unchanged interval checker.
The complete 201-direction coverage replay here accepted it again on 3 October, 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 the verified lower bound
from its entry on 6 October (T-070) until T-090’s certificate was decided here later
that day. Hosono’s README says parts of the work were produced with AI assistance under
human direction.
External intake, 2026-10-05. Hosono’s
mixed-certificate source
reports (T-090), from a density of 489 rectangles of total
mass , accepted there at every net angle by its research copy of
Tokoharu’s checker at threshold one.
It is above the this case reported, by . It supersedes the source’s
mixed_n51_L746. sqverify-fast, this repository’s clean-room verifier, decided it here
on 6 October 2026 at all 201 net directions, so it is also the verified lower bound:
confirmed, independently re-implemented.
Hosono’s README says parts of the work were produced with AI assistance under human
direction.
External intake, 2026-10-03. Hosono’s
mixed-certificate source
reports the mixed certificate mixed_n51_L746 at side (T-082), since
superseded (T-090), from a density of 446 rectangles of total mass
, accepted there at every net angle by its research copy of
Tokoharu’s checker at threshold one.
It is above the this case reported, by . sqverify-fast, this
repository’s clean-room verifier, decided it here on 6 October 2026 at all 201 net
directions: confirmed, independently re-implemented.
The verified lower bound is unchanged, the certificate above being higher.
Hosono’s README says parts of the work were produced with AI assistance under human
direction.
Verified lower bound, 2026-10-02. Hosono’s
mixed rectangle-density certificate for 50 squares (T-048), of mass
, carries here by monotonicity: its complete
replay passed here on 29 September, so it was the verified lower bound until 6 October,
above Nagamochi’s closed form, which has been a reported bound since Karakuş’s finding
(see below). The reported bound below was higher and had not then been replayed; on 6
October rect_n51_L74425’s (T-070), whose complete replay with
Tokoharu’s checker ran on 3 October, replaced it, and T-090’s (above) replaced
that later the same day.
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 the rectangle certificate rect_n51_L74425 at side , since
superseded (T-082), 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 had not yet run
here, so the verified lower bound was unchanged until that replay was entered on 6
October (T-070, 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-09-28 intake above raises, with total mass , accepted by Tokoharu’s unchanged interval checker. At that intake, this repository’s exact audit checked 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.
Previously, , found by Schadt in January 2026 by simulated annealing, refound and refined by Ellsworth, and analytically optimized to a degree-12 algebraic number in February 2026.
The exact certificate
Daniel’s
square-packing published
on 5 October 2026 exact rational certificates of the packings this register then listed
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 51 squares, each a rational
centre and a rational , in a square of side
, above the side the Kingbird catalogue prints,
. Rounded to binary64, square for square, its pose is the one the
atlas then pictured for this count.
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 previously proved , the verified upper bound at that
intake: 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 at that intake agreed to one unit of the printed side’s last place, the precision at which the record compares them. The printed side itself was not certified by that rational certificate: the certificate’s side lay above it.
The best published data on how hard these searches are
This case matters out of proportion to its size because Ellsworth published run statistics for it, and they are the most informative artifact in the entire subject. Across nine sessions on an NVIDIA RTX 3080 Ti with the annealer configured for 65,536 threads, the search found 3,004 distinct basins, of which only 4 refine to the record — about 23.6 seconds per basin, and an expected 4.9 hours of GPU time to hit the record basin once. Ellsworth’s own description: “an exceedingly rare find.”
That quantifies the shape of the objective landscape better than any prose can. The optimum is a needle among thousands of basins that look almost as good, which is why general-purpose global optimization loses ground past and why the records are held by a purpose-built stochastic searcher rather than a solver.
It is also why an open annealer with reproducible, counter-based randomness would be worth building: statistics like these exist for exactly two values of , and only because one person chose to publish them.
Reported Lower Bound
The earlier external report, [Friedman DS7], gives the lower-bound expression for (approximately ). Friedman’s DS7 survey, Theorem 9, k=7, reports this bound at n=50; reference [8] is Green’s private communication (2000). The source proof has not been recovered. The unavoidable-set argument DS7’s Figure 34 illustrates does not prove it: at that point pattern leaves a unit square empty (review). Inherited at n=51 by monotonicity. Hosono’s rectangle-density certificate above has since replaced it in the reported field, and the replayed certificate the verified one, itself replaced on 6 October by the replayed rectangle certificate for this count, and that later the same day by this count’s own mixed certificate, decided here (above). Before that certificate the verified lower bound was , Nagamochi’s closed form (corrected 2 October 2026: a reported bound since that date, Karakuş’s general bound giving here, since Nagamochi’s Lemma 1, on which the earlier value rested, is false; review). This register had recorded that proof as verified, its own error, logged as defect D-516. The source audit compares the exact theorem expressions separately from opaque table decimals.
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-n051-wand125-mixed-747-sqverify-fast-replay |
replayed here | independent | V-sqverify-fast (first-party) |
| verified upper | E-ryxu-432-radical-n51-feasibility |
replayed here | independent | V-sqpack-verify, V-ryxu-undilated-n51-independent (first-party); V-ryxu-complete-custody (first-party, premises) |
The Xu construction
Xu reports (T-126) a construction at exact side , displayed upward as . The pinned factual packet retains the entire source input and complete actual deciding outcomes.
This is the undilated construction over , using all 51 source coefficient poses. It is distinct from the source’s rational certificate, which already includes its stated dilation.
Complete native replay, required full-roster controls and scoped independent review confirm finite feasibility at V3/C3. The source discloses LLM assistance. No global optimum, local-minimum theorem, rigidity or novelty is established. The source’s 191-touching-pair assertion for n51 is unconfirmed and is not admitted.