n = 19 open ★=
Proven
- new result
- exact
Citation record n-019
lowerwand125 after Tokoharu, Levy et al. 2026, GitHub (confirmed T-103)
upperWainwright 1979, Squares in Squares
Open
- optimality
Bounds
4.88561808316412
- Found by
- Robert Wainwright 1979
- Construction
- hand
- Source
- [Kingbird]
- Evidence
E-kingbird-upper-register,E-lifted-q2-upper
4.88561808316412673173558496561293
The reported value, verified here.
- Evidence
E-lifted-q2-upper
- 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 341 uniform rectangles of total mass 1899999/100000, on a net the certificate declares: core side 4999/5000 and 2073 half-angle tangents of step 1/5002, 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 48229/10000 the record reported (T-100). sqverify-fast, this repository's clean-room measure verifier, decided it here at all 2073 directions on 6 October 2026.
- Source
- [wand125 mixed bounds check2 2026-10-06]
- Evidence
E-n019-wand125-mixed-4825-report
The reported value, verified here.
≈ 0.06061808…
Verified upper minus verified lower.
Results in the register
T-007 V0 C1 Nagamochi · 2026-08-31 · 321 cases
for
T-016 V3 C3 Massaccesi after Burns · 2026-09-03 · n = 18, 19
for , by monotonicity from T-015
Claim and records
- Claim
- and , by monotonicity from T-015 (a packing of n >= 17 unit squares contains a packing of 17). At this replaces Nagamochi's 1 + sqrt(12) = 4.4641... since (22529/5000 - 1)^2 = 307265841/25000000 > 12; at the certificate does not improve 1 + sqrt(13) = 4.6055... since that square is below 13, and nothing changes.
- Composition
- Derived: the minimum over T-015 and the monotonicity step, which is one recorded line carried in the evidence limitations and the n-018 and n-019 case bodies; T-015 sits at V3/C3, so the derived claim keeps the rungs.
- Next rung
- Rises with T-015; a bespoke or certificate stronger than the inherited bound would be a new result, not a rung change. Superseded as the verified lower bound on 2026-09-04 by T-019, which carries 459/100 to and by the same monotonicity step this result uses, from a larger base. This result stays true as stated and keeps its rungs.
- Significance
- The same movement carried to (+0.079587 over T-002) and (+0.0416984 over Nagamochi's 1 + sqrt(12), the first movement of that case's verified lower bound since 2005); the derivation adds one line beyond T-015 and inherits its source and credit.
- Novelty
- previously-published Present in an identified source
- Records
T-019 V3 C3 Levy after Burns, Massaccesi · 2026-09-04 · n = 17–19
for
Claim and records
- Claim
- , and and , from this project's weighted fractional unavoidable-set certificate at container side 459/100 = 4.59.
This displaces Massaccesi's 22529/5000 = 4.5058 (T-015) and the two cases T-016 carried from it, all three of which had held that value until 2026-09-04. The movement past the published value is +0.0842 at each of the three sizes.
A stronger public candidate, anabologyco-maker's side 4.5705 (nine thousand one hundred forty-one two-thousandths) of 16 August 2026 (GitHub; not replayed here), was outside the record's search corpus when this was registered and was found on 2026-09-07; it lies 0.0195 below this result. Two rungs are retained below it, 451/100 and 229/50.
The September 2026 DS7 audit identifies a stronger reported n19 bound from Theorem 10 at k=4, approximately 4.6172815, with an unresolved theorem/table discrepancy and missing proof. T-019 does not improve that report; its public source displacement is supported at n17 and n18, while all three certified inequalities and their movements from the prior register remain valid.
The three sizes do not need a monotonicity step. Only Condition 2 mentions n among the five conditions, so an atom set of mass 423327/25000 certifies the side for every integer above it, which is 17 and upward; monotonicity would give the same thing and is not what is used.
It does not improve , where Nagamochi's 1 + sqrt(13) = 4.6055... is larger -- the certificate does prove , but that is the weaker statement. - Composition
- Primary at all three sizes: one certificate, one accepted verdict, the bound being the container side directly. Its mass 423327/25000 is below seventeen, and Condition 2 is the only condition that mentions n. The same certificate therefore applies directly at n17, n18 and n19; monotonicity would also prove the latter two inequalities but is unnecessary for this certificate.
- Next rung
- A second machine method decides it, the interval-certified decision, the first here that is not exact-algebraic. V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained.
The bound itself: the retained certificate's total is 423327/25000 = 16.933080, leaving 0.066920 below seventeen, and that margin is what a further rung has to be found inside.
One figure from the ladder is worth carrying, because it contradicts the obvious reading. Margin is not monotone in the side. The 451/100 rung two below this one has total 16.593620 and margin 0.406380 -- an order of magnitude more headroom at a side 0.08 lower -- and the 229/50 rung between them has margin 0.034265, half of what 459/100 has at a higher side. So the covering value at a given side is set by the site set at least as much as by the side itself, and a better site set at a higher side can open the margin back up rather than close it. The ladder shows the same shape in the same direction: margin 0.007175 at 197/50, then 0.029410 at the higher 79/20.
Massaccesi's own atoms are the reference point and not a limit: they give a covering value of 203/12 at 4.5058, tight by construction, which bounds nothing about what a different site set reaches at a larger side.
A further rung is therefore a search question, and the quantity to read is the restricted optimum a converged run reaches, never an extrapolated rate.
One such question was asked and answered on 2026-09-04, at and side 117/25 = 4.68, and it is recorded here as measurement rather than as a claim about tau*. Three site sets in succession -- 538, 578 and 618 orbits -- returned a restricted optimum of exactly 18.000000, the third of them after 157 row-generation rounds that grew the row set from 15888 to 27516 and cost 7056 s. Adding sites can only lower a restricted optimum, and across those three it did not move at all.
Two readings are open and the run did not separate them. Either the covering value at that side is at or above eighteen, in which case no certificate exists there; or the site sets are still short of it and the optimum is sitting on a degenerate vertex, which the collapse of pricing from 90 s to 1--3 s suggests -- a dual that sparse is what a degenerate basis looks like. Exactly round values are the known artefact signature in this pipeline, 18.0 having been one for 's grid-31 optima, so the second reading cannot be dismissed.
What is not in doubt is the cost of settling it: two hours for the round that did not move. The run was stopped for that reason rather than for its answer, and the side is available to a later block with a cheaper decision path.
The method's own ceiling is not close here. A certificate for n cannot exist above ceil(sqrt(n)) * B, a wider container holding ceil(sqrt(n))^2 pairwise disjoint axis-parallel B-squares whose masses Condition 5 forces past n; for that is 5B = 4.9885, so 459/100 still has 0.3985 of runway. Unlike , where the ceiling sits below the conjectured value and forecloses the case, nothing structural stops this one.
Where the next rung is worth spending on, though, is not . Of the five conditions only Condition 2 mentions n, and the covering program behind the search does not contain n at all -- minimising total mass subject to every admissible B-square carrying mass at least 1 is a question about L, B and the net. So one atom set proves >= L for every integer n above its mass, this certificate's 16.933080 reaching 17, 18 and 19 directly, and a larger n is strictly easier at the same side.
The headroom said the rest, when this was written. had 0.0855 to its best known packing at 4.675530; had 0.2329 to 4.822876 and had 0.2956 to 4.885618, both still carrying this certificate's side in the verified register; and had 0.3944 to the trivial 5, holding Nagamochi's closed-form 1 + sqrt(13) = 4.605551. A run at a side whose covering value lands between 17 and 18 would raise and leave where it is; one landing between 19 and 20 would displace a published closed form.
The resumed search ran the same day and is registered as T-020, at side 24/5 with retained certificate mass 18.922620, between eighteen and nineteen. It supersedes this result at and moves and as well. What this result still holds alone is and : T-020's atoms are too heavy for either, which is the reach rule above read in the other direction. This result stays true as stated at all three of its sizes and keeps its rungs.
For the reading is unchanged and the runway is 0.3985 to the ceiling and 0.0855 to the packing. For , T-030 now certifies 4679/1000; T-029's 1871/400 remains as the previous rung. 117/25 remains the open probe this next_rung named. - Significance
- Scored against the rubric's anchor for S4, "a reusable technique, bound family, or resolved disputed value". One certificate moves three registered cases, and it replaces a published value rather than an inherited or closed-form one -- the only bound this project has displaced that someone else had put in print.
A stronger public candidate found afterwards, anabologyco-maker's 9141/2000 = 4.5705 of 16 August 2026 (GitHub; not replayed here), was outside the search corpus at scoring time, so the displacement at n17 and n18 is 0.0195 over that public report and 0.0842 over the one this record had adopted. At n19, the DS7 audit now retains a stronger source-reported bound than T-019; its 0.0842 movement refers to the prior register. The family-level score is unchanged.
Held below S5 because none of , 18, 19 is a central open case, the movement is 0.0842 rather than a qualitative change, weighted resource counting predates this project, the recent pure-atomic rational direction-net architecture follows Burns, the LP parameter line follows Massaccesi, and the case does not change character at the new value. - Novelty
- apparently-novel Not found in the recorded search, subject to its stated gaps
- Records
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. - Composition
- Primary at all three sizes: one certificate, one accepted verdict, the bound being the container side directly. There is no monotonicity or composition step anywhere between the artifact and the claim -- the three sizes come out of Condition 2, which is the only condition that mentions n. Two evidence entries whose method values differ decide it, the exact event-cell sweep and the interval branch and bound, both run in this repository; that is C3, with the two methods shown beside the rung. Unlike T-017 and T-019 no independent evaluator reviewed the scoring, and no review record is retained, so rung 4 waits on two adversarial AI reviews and a human oversight record.
- Next rung
- This result's 24/5 rung has total 18.922620, leaving 0.077380 below nineteen, and that margin is where a further rung had to be found. It is a wide margin by this register's standards -- 's top rung has 0.066920 and 's has 0.001040 -- which says the side was not pushed to where the covering value stops it, only to where the run was stopped. That is the honest reading of how this one was obtained.
The column generation was halted at round 9 with a restricted optimum of 18.916941, because four more rounds would have cost about 3.75 h to buy margin nothing needed. The side above it was never attempted.
Where the ceiling sits differs across the three sizes and it matters. A certificate for n cannot exist above ceil(sqrt(n)) * B, which for all three is 5B = 4.9885, so 0.1885 of structural runway remains. But at the best known packing is 4.885618, and no certificate can exceed a side a packing achieves, so the real runway there is 0.085618. At and the best known packing is the trivial 5, so the ceiling binds first: the method could in principle close either to within 0.0115 of the upper bound and can never reach it. That asymmetry is the targeting instruction.
A run above 4.885618 that succeeded would contradict the retained packing and is a refutation to look for rather than a rung to expect; a run between 4.80 and 4.9885 that succeeds moves and and stops at . The quantity to read is the restricted optimum a converged run reaches, never an extrapolated rate, and the cost was the exhaustive tier: the 24/5 rung's exact sweep took 5378 s at its own 2260-atom set, against 173 s for the interval route on the same bytes. The same evening the sweep was rewritten to decide in integers on the weights' common scale, in parallel over directions, and returns the same least covered mass in 38.7 s on the same box.
The margin was found and taken the following day: T-021 certifies 97/20 = 4.85 at and from a site set seeded with this certificate's own atoms, and supersedes this result at both sizes. What this result still holds alone is , whose bound stays 24/5 because T-021's atoms are too heavy for it; the rung itself is retained at cases/n20_fractional_certificate/certificate-24-5.json and replays by name. On 2026-10-02 wand125's replayed rectangle certificate, (T-045), superseded it at as well. This result stays true as stated at all three of its sizes. - 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-045 V3 C3 wand125 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 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-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-100 V3 C3 wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-06 · n = 19
Mixed rectangle-measure lower bound verified at , past the best 18-square packing
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.8229.
The certificate is a density of 313 uniform rectangles in D4 orbits, and no point mass, of total mass 1899999/100000, on the net T-096's certificate declares: core side 999/1000 and 416 half-angle tangents of step 1/1001, with 999/1000 (1 + 1/1001) = 500499/500500 < 1. The source reports every core at a net angle capturing mass at least one: at all 415 oblique net angles by code/mixed_rotated_verify.cpp, its research copy of Tokoharu's verify.cpp at coverage threshold one, run by the same driver as T-096's certificate, and at the axis by exact integer tables.
The value is above the 1927/400 = 4.8175 of the source's rectangle certificate rect_n19_L48175 (T-074), the reported and verified lower bound at before it, by 0.0054. It is also above (7 + sqrt 7)/2 = 4.8228757..., the side of Hämäläinen's packing of 18 squares and the verified upper bound at , by about 2.43e-5, so < , as the source notes.
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, independently re-implemented. The verifier shares no code with the source's checker and runs the same net-and-shrink method, so it is a second implementation and not a second method. The 6 October review of the certificate found no defect. The source's own checker was replayed here at 10 of the 416 directions, each returning the certificate's own record, and not in full.
wand125 after Tokoharu and Levy, square-packing-bounds. Registration was requested in a comment of 6 October 2026 on jlevy/squares#366. 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 independent implementation, C3, on the census route, whose per-certificate conditions for a declared net the soundness review of the declared-net change set and this certificate meets. The source's checker was replayed at 10 directions and its axis tables were not run in full here, so no second method and no complete reproduction with the producer's code stands beside it.
The separation < is cited from 's record, whose verified upper bound is E-lifted-q7-upper, the exact verification of Hämäläinen's packing; this entry adds no evidence for it beyond its own bound. - Next rung
- V4 and C4 need two adversarial AI reviews of this result by distinct reviewers and a human oversight record. One is retained, the review of 6 October that read the certificate. A complete replay of the source's own checker, the bundle's driver over all 416 nodes by devtools.audit_wand125_declared_net replay (13.4 CPU-hours priced here), would add a reproduction with the producer's code beside the rung; a second machine method would be a method-distinct decision of rotated coverage.
- Significance
- The strongest verified lower bound on record at , by 0.0054, and the first to pass the side of the best packing of 18 squares, which separates from (Evan Daniel's question on jlevy/squares#281), by about 2.43e-5. The certificate kind and checker of T-069 and later on T-096's declared net; no new technique, at S3 as T-074 is, the separation a corollary of this bound and Hämäläinen's packing rather than a method or a family of bounds. The 6 October review confirmed the draft.
- Novelty
- previously-published Present in an identified source
- Records
T-103 V3 C3 wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-06 · n = 19
Mixed rectangle-measure lower bound verified at , on the finest declared net yet
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.825.
The certificate is a density of 341 uniform rectangles in D4 orbits, and no point mass, of total mass 1899999/100000, on a net it declares itself, finer than any it declared before: core side 4999/5000 and 2073 half-angle tangents of step 1/5002. 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 2073 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 48229/10000 = 4.8229 of T-100, the source's earlier certificate and the reported and verified lower bound at before it, by 0.0021, and supersedes it.
The certificate was decided here on 6 October 2026 by sqverify-fast, this repository's clean-room measure verifier, at all 2073 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 1021 and 2072, 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 2073 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 2073 directions (devtools.audit_wand125_declared_net cpp-sample, about 97 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.0021 above T-100, 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 11 of the retained witness (witness id 12) translates 0.028595 along (0, 1) with the packing still valid, so the configuration admits a non-trivial feasible motion; 4 of its 19 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
22 evidence entries
E-n019-wand125-mixed-4825-sqverify-fast-replay, E-n019-wand125-mixed-4825-report, E-n019-wand125-mixed-48229-sqverify-fast-replay, E-n019-wand125-mixed-48229-report, E-n019-wand125-rect-48175-sqverify-fast-replay, 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-lifted-q2-upper, E-n017-massaccesi-source-replay, E-n017-burns-source-replay, E-n017-burns-control-decision, E-n017-mira-point-certificate-replay, E-n017-fort-point-certificate-replay, E-n017-anabologyco-weighted-certificate, E-n017-massaccesi-h052-agreement, E-green-ds7-theorem10-reported-lower, E-n020-fractional-certificate
- [wand125 mixed bounds check2 2026-10-06] lower bound proof
- [wand125 mixed bounds finer net 2026-10-06] 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
- [Burns–Massaccesi n17] lower bound proof
- [GitHub n17 certificates 2026] lower bound proof
- [Friedman DS7] survey
— open
External intake, 2026-10-06. wand125’s
check2 source
reports (T-103), from a density of 341 rectangles of total
mass , on a net the certificate declares: core side and
2073 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-100) by . This repository’s clean-room
verifier sqverify-fast decided it here on 6 October 2026 at all 2073 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-06. wand125’s
finer-net source
reports (T-100), since superseded (T-103), from a
density of 313 rectangles of total mass , on a net the certificate
declares: core side and 416 half-angle tangents of step , the net of
its 5 October certificate at . Since , every
unit square contains a core at a net angle strictly in its interior.
The source accepts it at every net angle by its research copy of Tokoharu’s checker at
threshold one. It is above the rectangle certificate’s below by , and
above , the side of Hämäläinen’s packing of 18 squares and
the verified upper bound at , by about , so
, as the source notes.
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, independently re-implemented, so it was also the verified lower bound until
later that day, when the check2 certificate above superseded it in both lanes.
The source’s own checker was replayed here at 10 of the 416 directions, each returning
the certificate’s own record, and not in full.
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 , 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-27. 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.
Open. The best known packing gives . The verified lower bound is
, from wand125’s check2 certificate on its finest declared net
(T-103, 2026-10-06, V3/C3), leaving a gap of to the reported record.
It is above ’s verified upper bound , so , as
was its predecessor at (T-100, 2026-10-06), the verified lower
bound until later that day.
That one superseded wand125’s rectangle-density certificate of 1 October at
(T-074, replayed here on 2026-10-02), which was the verified lower
bound until 2026-10-06. That one’s predecessor of 27 September,
(T-045), held the field earlier that day, and had superseded this repository’s
weighted fractional unavoidable-set certificate at (T-020, 2026-09-04).
On 2026-09-04 this case moved twice in one day, from to
(T-019) and then to , a total of . Nagamochi’s
general had held it before that, and was already weaker
than the first of the two.
Corrected 2 October 2026: Nagamochi’s value is now a reported bound, his Lemma 1
being false (Karakuş 2026;
review).
This register had recorded that proof as verified, its own error, logged as defect
D-516.
The packing
Wainwright’s diagonal strip of width two (1979), for which the survey states no
generating rule — only the figure.
cases/lifted_q2 lifts the retained witness’s every coordinate into Q(sqrt 2) at
small height and verifies the lifted pose exactly, which is what moved
verified_upper_bound from the grid ceiling onto the published exact side.
The lift is a candidate generator and the exact verifier is the proof; the certificate
is the witness’s own geometry, made exact (D-398, and the operation D-402 does not
foreclose).
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. 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. wand125’s rectangle-density certificate above has since replaced it in the reported field, and from its replay here on 2026-10-02 it was also the verified lower bound until wand125’s mixed certificate on a declared net (T-100) replaced it in both on 2026-10-06. The source audit compares the exact theorem expressions separately from opaque table decimals.
Until 2026-10-02 the operative bound was a weighted fractional unavoidable-set
certificate at side : 2260 rationally weighted atoms on a D4-symmetric site set,
total mass , every closed -square at every net direction capturing
mass at least one, the least being . It is decided from its own bytes by an
exact event-cell sweep and by an interval branch and bound over centre boxes, which
agree on that least value to the digit.
Nothing is inherited by monotonicity.
Of the five conditions only Condition 2 mentions , so this atom set certifies its
side for every integer strictly above its own mass — 19 and upward — which is why the
same certificate also carries and . Its predecessor, T-019, reaches
this case the same way from a lighter set, and before either of them the case was held
by the Massaccesi certificate carried across by monotonicity, a 2026 blog-post
result whose author marks the value “(?)” and which is replayed here twice (H-052,
BC-150, BC-151). 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).
Nagamochi’s general closed form remains the external published baseline and applies to
every :
Here it gives , now weaker by ; the first movement of this case’s verified lower bound since 2005 came on 2026-09-03.
What the method can still add here
A certificate for cannot exist above , which at is — but no certificate can exceed a side an actual packing achieves either, and Wainwright’s packing achieves . So the packing binds first and the runway above was , not ; above it was , above it was , and above the current it is . A run that certified a side above would contradict the retained witness; that is a refutation to go looking for, not a rung to expect.
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-n019-wand125-mixed-4825-sqverify-fast-replay |
replayed here | shared components | V-sqverify-fast (first-party) |
| verified upper | E-lifted-q2-upper |
replayed here | independent | V-sqpack-verify (first-party) |