As published
= corrects Nagamochi 2005open
Proven
- exact
Citation record n-292
lowerKarakuş 2026, arXiv corrects Nagamochi 2005 (confirmed T-083)
upperChaoweeraprasit & Daniel, GitHub (confirmed T-146)
Open
- optimality
Bounds
17.59137814…
17.5913781454976982- Found by
- Chaoweeraprasit 2026
- Improved by
- Daniel
- Construction
- —
- Source
- [Daniel regularized lists 2026-10-10]
- Evidence
E-evand-regularized-certificate-report
17.59137814…
17.5913781454976982The reported value, verified here.
17.15703136722
- Proved by
- Green 2000
- Kind
- monotone
- Scope
- Source-reported only; no verification promotion.
- Note
- Friedman's DS7 survey, Theorem 9, k=17, reports this bound at n=290; 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 k=17 that point pattern leaves a unit square empty (devtools.check_green_ds7). Inherited at n=292 by monotonicity.
- Source
- [Friedman DS7]
- Evidence
E-green-ds7-theorem9-reported-lower
17.09066002…
17.090660023- Corrects
- Nagamochi 2005 (T-007)
- Evidence
E-karakus-strip-lower,E-karakus-strip-measure-interval
0.50071812…
Verified upper minus verified lower.
Results in the register
T-007 V0 C1 Nagamochi · 2026-08-31 · 321 cases
for
T-056 V3 C3 Couzo · 2026-09-29 · 49 cases
Smaller packings for 49 counts from to , each certified two independent ways
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-117 V3 C3 Rehwaldt after Couzo and earlier contributors · 2026-10-07 · n = 105, 292
Exact rational ceiling refinements at , 292
Claim and records
- Claim
- Complete exact replay, independently re-implemented, confirms the finite rational upper-bound refinement at , 292. Only finite feasibility enters; no optimality claim is registered.
- Significance
- Exact rational refinements of Couzo's packings at and 292, lowering the case ceilings by about 2.1e-11 and 4.3e-11: re-solves of arrangements the record already credits, at the scale of their rounding, which is what T-098 (S2), T-137 and T-139 are; a packing moved to a new optimum by 1e-7 or more (T-127, T-128) is S3. No solved case or new arrangement. Confirmed on 11 October.
- Novelty
- previously-published Present in an identified source
- Records
T-129 V0 C0 Daniel after Couzo, Levy · 2026-10-08 · n = 105, 130, 292
Three dated Daniel certificate reports with historical source custody
Claim and records
- Claim
- Complete author certificate reports at 105, 130 and 292 are retained with matching inputs and separate immutable pins, at the exact sides they state: , and . All three exact sides are superseded by smaller currently verified bounds; selected cases and original T-098/T-101 assurance are unchanged.
- Significance
- Historical certificate custody without a current frontier improvement.
- Novelty
- previously-published Present in an identified source
- Records
T-136 V3 C3 Chaoweeraprasit after Couzo, Xu, Göbel, Schadt, Ellsworth, Hajba, Levy · 2026-10-10 · 17 cases
Seventeen exact rational packings from SQUISH's third request
T-146 V3 C3 Daniel after Xu, Chaoweeraprasit, Polkovskyi, Levy · 2026-10-10 · 15 cases
Exact rational certificates at fifteen counts from Daniel's regularized record lists
T-174 V3 C3 PingYou Ltd after Friedman, Ellsworth, Daniel, Xu, Barnett, Couzo, Ostashev, Chaoweeraprasit, Gupta, Fang, Polkovskyi, Levy · 2026-10-14 · 68 cases
Tighter certificates at 68 counts from PingYou Ltd, of others' packings and its own
T-180 V0 C1 Hosono · 2026-10-14 · 264 cases
Closed-form lower bound for every non-square , reported
T-193 V3 C3 Daniel after Xu, Chaoweeraprasit, Ostashev, Couzo, PingYou Ltd, Gupta, Polkovskyi, Levy · 2026-10-16 · 16 cases
Exact algebraic sides at sixteen counts from Daniel, of packings the record credits
upper: replayed here; lower: external proof (read here), audited here
formal lower differs from report; reported lower: defect recorded
not rigid, numerically checked, numerical multiprecision
Evidence: E-translation-escape-not-rigid
Scope
Square 6 of the retained witness (witness id 7) translates 0.591378 along (0, 1) with the packing still valid, so the configuration admits a non-trivial feasible motion; 22 of its 292 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: port of his coincidence placement (regularize_grid_slack/1) rather than his code, same-side exact re-solve (devtools.regularize_same_side). A drawing of T-146's packing at the witness's own side: a pure regularization, which proves no new bound, so not a result. The house is itself its source's regularization of T-136's packing (Daniel after Xu, Chaoweeraprasit, Mishapolk, Levy), registered as T-146 for the upper bound its exact side proves.
- 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: s(292) <= 17.60256849240573729, Casson's packing, larger than the reported side (Casson)
- Priority: s(292) <= 17.601260370442159, the first of Couzo's packings for this count (Couzo)
- Priority: Earlier reported ceiling 17.597249391199519 from [franciscouzo square-packing 2026-09-27]; earlier construction and exact verification evidence remain historical. (Couzo)
- Priority: Earlier house 17.597249391156465040471442005510391858592626557 from [Rehwaldt Couzo refinements 2026-10-07], the case’s ceiling until 11 October 2026; its certificate and replay remain retained. (Couzo, Rehwaldt)
19 evidence entries
E-franciscouzo-2026-09-27-report, E-franciscouzo-2026-09-27-exact-replay, E-franciscouzo-2026-09-27-interval-replay, E-casson-2026-09-23-report, E-kingbird-upper-register, E-nagamochi-lower, E-basic-grid-upper, E-karakus-strip-lower, E-karakus-strip-measure-interval, E-nagamochi-lemma1-counterexample, E-green-ds7-theorem9-reported-lower, E-rehwaldt-couzo-refinements-2026-10-07-report, E-rehwaldt-couzo-refinements-2026-10-07-exact-replay, E-pingyou-574-certificate-report, E-pingyou-574-exact-feasibility, E-evand-regularized-certificate-report, E-evand-regularized-exact-feasibility, E-squish-481-certificate-report, E-squish-481-exact-feasibility
- [Rehwaldt Couzo refinements 2026-10-07] upper bound report
- [franciscouzo square-packing 2026-09-27] upper bound report
- [griffcass square-packing 2026-09-23] upper bound report
- [Kingbird] record catalogue
- [Nagamochi 2005] lower bound proof
- [Friedman DS7] survey
- [Karakuş 2026] lower bound proof
- [Daniel regularized lists 2026-10-10] upper bound report
— open
House adoption, 11 October 2026. Daniel’s display regularization of Chaoweeraprasit’s SQUISH packing (T-146) is now this case’s house: its exact certificate proves , the reported and the verified upper bound, rounded outward from its exact side. The exact certificate side improves the previous verified exact side by about . The earlier ceiling, displayed outward as from Couzo’s packing, improved by Rehwaldt (T-117), applied until this adoption and stays retained as history (the certificate).
Before the 7 October refinement, the best known published packing, Couzo’s (T-056), had the displayed ceiling , and the strongest lower bound independently verified here is from Karakuş’s general theorem, leaving a gap of . General bound: .
The packing
Couzo’s
square-packing
reports a packing of side for this count, dated 27 September 2026
and unchanged when this record retained the repository on 27 September 2026 (T-056). Its
first packing for this count, of side , is dated 26 September 2026.
The repository names no method and no tolerance, and itself states no AI assistance; its
author said on issue #227 that he found
the 102 and 103 packings “with the help of Claude”.
This repository certifies it exactly. The retained decimal pose rounds to an exact rational packing at centre dilation 1, of side , no larger than the printed side, and every pair and every wall is decided over twice, by the promotion’s exact separating-axis test and by an independent checker that shares no code with it (receipt). That replay established the earlier verified ceiling ; it says nothing about optimality. Interval arithmetic on the printed pose itself, with each angle’s true cosine and sine and no rational rounding, decides every pair and wall again and gives the same verified upper bound (interval route).
Casson’s
square-packing, dated
23 September 2026 and made with the help of Claude as its README says, reports a packing
of side for this count, larger than Couzo’s by
. Casson’s is the earlier of the two by the timestamps this
record’s priority notes keep: Couzo’s first packing for this count, of side
, is dated 26 September 2026. The record states both dates and
infers nothing about whether either packing derives from the other.
The previous best known packing
Before this intake the best known packing was the Kingbird catalogue’s, of side .
Found by an unrecorded author, via extension of a smaller record. Its side length is algebraic of degree 8 over .
The lower bound
The strongest lower bound independently verified in this record is Karakuş’s general bound, which applies to every nonsquare :
Correction, 2 October 2026. Until that date the verified lower bound here was Nagamochi’s general closed form, , which is stronger at this and is now recorded as a reported bound. Its published proof rests on Nagamochi’s Lemma 1, which Karakuş showed false; nothing is disproved, and no packing beating it is known (review of 2 October 2026). This register had recorded that proof as verified, its own error, logged as defect D-516.
Source-reported bounds are recorded separately from this independently verified theorem.
The reported lower-bound expression for is
(approximately ). Friedman’s DS7
survey, Theorem 9, k=17, reports this bound at n=290; 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 k=17 that
point pattern leaves a unit square empty (devtools.check_green_ds7). Inherited at n=292
by monotonicity. This is a source-reported lower bound; it does not replace the verified
bound above. The exact specialization and comparison are retained by
audit_ds7_lower_bounds.
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-karakus-strip-lower |
a published proof | no code | no verification code |
| verified lower | E-karakus-strip-measure-interval |
audited here | independent | V-check-karakus-strip-measure (first-party) |
| verified upper | E-evand-regularized-exact-feasibility |
replayed here | independent | V-sqpack-verify, V-check-rational-witness-independent, V-check-half-angle-area (first-party); V-evand-exact-certificates, V-evand-arrangement-receipts, V-upper-bound-reports (first-party, premises) |
The 7 October rational refinement
Rehwaldt reports the finite rational witness (T-117) at exact side , whose complete terminating decimal is . The pinned source refines Couzo’s existing construction with disclosed OpenAI Codex assistance. The complete finite witness is now exact-replayed here at V3/C3 after scoped review and public recovery of all original scientific evidence. Earlier ceilings and verification remain historical evidence for their own geometries. No unrestricted lower bound, optimality or rigidity claim is added. The earlier rigidity screen belongs to the earlier geometry and is preserved in the packet’s prior-state record; the current numerical translation screen is separate from the exact feasibility evidence.
Evan Daniel’s certificate (T-146)
Daniel’s display regularization of Chaoweeraprasit’s SQUISH packing, reported in his regularized record lists, on no issue, at exact side , displayed upward as (T-146). The certificate gives a rational side and, for each of the 292 unit squares, a rational centre and the tangent of its half-angle; the retained packet holds it with the complete native jobs that decided it.
Both maintained exact routes decided it here, sqpack’s exact separating-axis verifier
and the independent rational corner checker, with its duplicate-square and
outside-container controls, and a third exact route, half-extent containment and exact
intersection area, decided it again.
No route here is the source’s code, so the replay is independently re-implemented.
The
review of 11 October 2026
and the
final review of 11 October 2026
accepted the replay for finite feasibility.
That proves , the verified upper bound: confirmed,
independently re-implemented.
It says nothing about optimality, rigidity or a local minimum.
The certificate regularizes for display the packing T-136 records, at the side the source reports as that packing’s exact optimum, so the packing stays with its finder and Daniel is credited with the regularization and the certificate. That the two are one packing is the source’s claim, measured here and not decided (T-146’s regularizations).
The source’s credits say the repository’s work was produced by Claude (Anthropic) under human direction.
The house it replaces, from Couzo’s packing, improved by Rehwaldt (T-117), stays retained with its own replay as history. The other certificates confirmed here at this count, T-136 at , stay verified and are not selected. T-174 at , below this house, is confirmed here and accepted by the review of 14 October 2026. From 15 October 2026 until the owner’s house rule of 16 October 2026 lifted the hold, PR #574’s houses were held for the owner, since their witnesses would add about 18.5 MB to a checkout and their custody inputs about 5.8 MB to every worker’s snapshot. The case keeps this house until T-193’s adoption, staged under think-ot5c, moves it to T-193’s side, below T-174’s, once the writer takes an algebraic side. T-193’s exact algebraic side at this count, a root of a degree-6 integer polynomial below this house, is confirmed here and accepted by the review of 16 October 2026.