Case record
The best packing known for 18 squares, side 72+127, Hämäläinen 1980. Regularized by the Squares Project with Daniel's regularizer (evand/square-packing, MIT)
As published
The packing as published, Hämäläinen 1980 [Kingbird]

n=18

=open

941200≤s(18)≤72+127

4.704.823
456
4.2435.243
nn+1

Proven

4.70500≤s(18)≤4.822876

  • exact

Citation record n-018

lowerHosono after Tokoharu, Levy et al. 2026, GitHub (confirmed T-102)

upperHämäläinen 1980, Squares in Squares

Open

  • optimality

Bounds

Best known packing

72+127

4.82287565553229
Found by
Hämäläinen 1980
Construction
hand
Tilt angles
0∘, 24.295∘
Source
[Kingbird]
Evidence
E-kingbird-upper-register, E-lifted-q7-upper
Verified upper bound

72+127

4.82287565553229529525080787681963

The reported value, verified here.

Evidence
E-lifted-q7-upper
Reported lower bound

941200

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 s(18)≥941/200 from a density of 324 uniform rectangles of total mass 1799999/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 588/125 the record reported (T-099). 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-n018-wand125-mixed-4705-report
Verified lower bound

941200

The reported value, verified here.

Evidence
E-n018-wand125-mixed-4705-sqverify-fast-replay
Gap

72−241200≈ 0.11787565…

Verified upper minus verified lower.

Results in the register

  • T-002 V3 C3 Levy after Bentz · 2026-08-31 · n = 18

    s(18)≥4426213/1000000, by monotonicity from T-001

    Claim and records
    Claim
    s(18)≥4426213/1000000, by monotonicity from T-001 (a packing of 18 unit squares contains a packing of 17).
    Significance
    The same movement carried to n=18, above Nagamochi's 4.316625; the derivation adds nothing beyond T-001 but the case's frontier field moved for the first time since 2005.
    Novelty
    apparently-novel Not found in the recorded search, subject to its stated gaps
    Records

    n = 18registerevidence 1evidence 2

  • T-003 V3 C3 Levy after Bentz · 2026-08-31 · n = 17, 18

    The sixteen-point set's unavoidability ceiling lies in [4426213/1000000,4427/1000)

    Claim and records
    Claim
    The sixteen-point set's unavoidability ceiling lies in [4426213/1000000, 4427/1000): certification at the left endpoint, an exact escaping pose at the right, with the top strips' a + 2b <= 2*sqrt(2) hypothesis identifying the closing mechanism at 753/250 + sqrt(2), inside the bracket.
    Significance
    Sharpens what T-001's construction can and cannot give; the exact equality claim at 753/250 + sqrt(2) remains analysis until the Q(sqrt 2) certificate lands.
    Novelty
    apparently-novel Not found in the recorded search, subject to its stated gaps
    Records

    n = 17n = 18registerevidence 1evidence 2

  • T-007 V0 C1 Nagamochi · 2026-08-31 · 321 cases

    s(n)≥min(⌈n⌉,n−2⌊n⌋+1+1) for 4≤n≤324

  • T-016 V3 C3 Massaccesi after Burns · 2026-09-03 · n = 18, 19

    s(n)≥22529/5000 for n=18,19, by monotonicity from T-015

    Claim and records
    Claim
    s(18)≥22529/5000 and s(19)≥22529/5000, by monotonicity from T-015 (a packing of n >= 17 unit squares contains a packing of 17). At n=19 this replaces Nagamochi's 1 + sqrt(12) = 4.4641... since (22529/5000 - 1)^2 = 307265841/25000000 > 12; at n=20 the certificate does not improve 1 + sqrt(13) = 4.6055... since that square is below 13, and nothing changes.
    Significance
    The same movement carried to n=18 (+0.079587 over T-002) and n=19 (+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

    n = 18n = 19registerevidence 1evidence 2

  • T-019 V3 C3 Levy after Burns, Massaccesi · 2026-09-04 · n = 17–19

    s(n)≥459/100=4.59 for n=17,18,19

    Claim and records
    Claim
    s(17)≥459/100, and s(18)≥459/100 and s(19)≥459/100, 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 n=20, where Nagamochi's 1 + sqrt(13) = 4.6055... is larger -- the certificate does prove s(20)≥459/100, but that is the weaker statement.
    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 n=17, 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

    n = 17n = 18n = 19registerevidence 1evidence 2

  • T-027 V3 C3 Levy after Burns, Massaccesi · 2026-09-18 · n = 18

    s(18)≥467/100=4.67

    Claim and records
    Claim
    s(18)≥467/100 = 4.67, from this project's weighted fractional unavoidable-set certificate at container side 467/100. The case previously held 459/100 = 4.59 from T-019; the movement is +0.08. The selected external report 9141/2000 = 4.5705 (GitHub; not replayed here) lies 0.0995 below this result.

    One size, and not by monotonicity. Only Condition 2 mentions n among the five conditions, so an atom set of mass 8937839/500000 = 17.875678 certifies the side for every integer strictly above that mass, which is 18 and upward. It does not reach n=17, where T-019 still holds 459/100. From n=19 on the register already holds 24/5 = 4.80, so the certificate is true there and weaker.

    One rung is retained rather than a ladder. The side was reached by seeding the generator's site set with T-019's own atoms scaled from 459/100 after the uniform grid locked at 18.000000.
    Significance
    Scored at S3 by the calibration note T-020 wrote for exactly this case: "Further sizes from the same generator, absent a new technique or a case that changes character, belong at S3." This is the same generator at n=18, one size-specific covering rather than T-019's Condition 2 carry, and n=18 does not change character at 4.67. The movement is +0.08 against T-019's verified field and 0.0995 against the strongest named public candidate. Held below S4 because the technique is the one T-017 already banked, the displacement is of this project's own prior rung rather than a published closed form, and n=18 is not a central open case.
    Novelty
    apparently-novel Not found in the recorded search, subject to its stated gaps
    Records

    n = 18registerevidence 1evidence 2

  • T-028 V3 C3 Levy after Burns, Massaccesi · 2026-09-19 · n = 18

    s(18)≥187/40=4.675

    Claim and records
    Claim
    s(18)≥187/40 = 4.675, from this project's weighted fractional unavoidable-set certificate at container side 187/40. The case previously held 467/100 = 4.67 from T-027; the movement is +0.005. The selected external report 9141/2000 = 4.5705 (GitHub; not replayed here) lies 0.1045 below this result.

    One size, and not by monotonicity. Only Condition 2 mentions n among the five conditions, so an atom set of mass 35758287/2000000 = 17.8791435 certifies the side for every integer strictly above that mass, which is 18 and upward. It does not reach n=17, where T-019 still holds 459/100. From n=19 on the register already holds 24/5 = 4.80, so the certificate is true there and weaker.

    One rung is retained rather than a ladder. The side was reached by seeding the generator's site set with T-027's own atoms scaled from 467/100 and adding a windows-5 lattice after 117/25 locked at 18.000000. n=18 is off the H-218 sweep, so this retain does not confirm that claim.
    Significance
    Scored at S3 by the calibration note T-020 wrote for exactly this case: "Further sizes from the same generator, absent a new technique or a case that changes character, belong at S3." This is the same generator at n=18, one size-specific covering rather than T-019's Condition 2 carry, and n=18 does not change character at 4.675. The movement is +0.005 against T-027's verified field and 0.1045 against the strongest named public candidate. Held below S4 because the technique is the one T-017 already banked, the displacement is of this project's own prior rung rather than a published closed form, and n=18 is not a central open case.
    Novelty
    apparently-novel Not found in the recorded search, subject to its stated gaps
    Records

    n = 18registerevidence 1evidence 2

  • T-029 V3 C3 Levy after Burns, Massaccesi · 2026-09-19 · n = 18

    s(18)≥1871/400=4.6775

    Claim and records
    Claim
    s(18)≥1871/400 = 4.6775, from this project's weighted fractional unavoidable-set certificate at container side 1871/400. The case previously held 187/40 = 4.675 from T-028; the movement is +0.0025. The selected external report 9141/2000 = 4.5705 (GitHub; not replayed here) lies 0.107 below this result.

    One size, and not by monotonicity. Only Condition 2 mentions n among the five conditions, so an atom set of mass 17889361/1000000 = 17.889361 certifies the side for every integer strictly above that mass, which is 18 and upward. It does not reach n=17, where T-019 still holds 459/100. From n=19 on the register already holds 24/5 = 4.80, so the certificate is true there and weaker.

    One rung is retained rather than a ladder. The side was reached by seeding the generator's site set with T-028's own atoms scaled from 187/40 and adding a windows-5 lattice. Auto at 1871/400 resolved to (32, 43, 54), not T-028's (32, 43, 53). n=18 is off the H-218 sweep, so this retain confirms H-219, not H-218.
    Significance
    Scored at S3 by the calibration note T-020 wrote for exactly this case: "Further sizes from the same generator, absent a new technique or a case that changes character, belong at S3." This is the same generator at n=18, one size-specific covering rather than T-019's Condition 2 carry, and n=18 does not change character at 4.6775. The movement is +0.0025 against T-028's verified field and 0.107 against the strongest named public candidate. Held below S4 because the technique is the one T-017 already banked, the displacement is of this project's own prior rung rather than a published closed form, and n=18 is not a central open case.
    Novelty
    apparently-novel Not found in the recorded search, subject to its stated gaps
    Records

    n = 18registerevidence 1evidence 2

  • T-030 V3 C3 Levy after Burns, Massaccesi · 2026-09-19 · n = 18

    s(18)≥4679/1000=4.679

    Claim and records
    Claim
    s(18)≥4679/1000 = 4.679, from this project's weighted fractional unavoidable-set certificate at container side 4679/1000. The case previously held 1871/400 = 4.6775 from T-029; the movement is +0.0015. The selected external report 9141/2000 = 4.5705 (GitHub; not replayed here) lies 0.1085 below this result.

    One size, and not by monotonicity. Only Condition 2 mentions n among the five conditions, so an atom set of mass 71573611/4000000 = 17.89340275 certifies the side for every integer strictly above that mass, which is 18 and upward. It does not reach n=17, where T-019 still holds 459/100. From n=19 on the register already holds 24/5 = 4.80, so the certificate is true there and weaker.

    One rung is retained rather than a ladder. The side was reached by seeding the generator's site set with T-029's own atoms scaled from 1871/400 and adding a windows-5 lattice. Auto at 4679/1000 resolved to (32, 43, 54), the same triple T-029 used. n=18 is off the H-218 sweep, so this retain confirms H-221, not H-218.
    Significance
    Scored at S3 by the calibration note T-020 wrote for exactly this case: "Further sizes from the same generator, absent a new technique or a case that changes character, belong at S3." This is the same generator at n=18, one size-specific covering rather than T-019's Condition 2 carry, and n=18 does not change character at 4.679. The movement is +0.0015 against T-029's verified field and 0.1085 against the strongest named public candidate. Held below S4 because the technique is the one T-017 already banked, the displacement is of this project's own prior rung rather than a published closed form, and n=18 is not a central open case.
    Novelty
    apparently-novel Not found in the recorded search, subject to its stated gaps
    Records

    n = 18registerevidence 1evidence 2

  • T-045 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-09-29 · 15 cases

    Rectangle-density lower bounds replayed at 15 counts in n=18…78

  • 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 n=18…95

  • T-058 V3 C3 Hosono after Tokoharu, Daniel · 2026-09-29 · 100 cases

    Rectangle-certificate ceiling α·UB(n) proved for n=1..100; B·UB(n) on 64 grid rows

  • T-083 V3 C3 Karakuş · 2026-10-02 · 301 cases

    s(n)≥1/2+n−⌊n⌋+1/4 for every nonsquare 8≤n≤324

  • T-085 V3 C3 Karakuş; Vlasenko · 2026-10-02 · 315 cases

    Nagamochi 2005, Lemma 1 is false for every container with a>3 and b>2

  • T-096 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-05 · n = 18

    Mixed rectangle-measure lower bound replayed at n=18, on a net the certificate declares

    Claim and records
    Claim
    A rectangle density of wand125/square-packing-bounds, checked at coverage one on a net it declares and published on 5 October 2026, proves s(18)≥47/10 = 4.7.

    The certificate is a density of 136 uniform rectangles in D4 orbits, and no point mass, of total mass 1799999/100000, on a net it declares itself: core side 999/1000 and 416 half-angle tangents of step 1/1001. The source's earlier mixed certificates, from T-069 on, use core side 9977/10000 on 201 tangents of step 83/40000. Since 999/1000 (1 + 1/1001) = 500499/500500 < 1, every unit square contains a concentric core of side 999/1000 at a net angle strictly in its interior. The source reports every such core 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-069's certificates, and at the axis by exact integer tables.

    The value is above the 939/200 = 4.695 of the source's rectangle certificate rect_n18_L4695 (T-045), the reported and verified lower bound at n=18, by 0.005. Its mass is below 19 too, but the record holds more there.

    The certificate passed a complete replay here on 5 October 2026 of the bundle's own driver and the source's unchanged checker on the pinned tarball: all 416 net nodes, each regenerated record equal to the certificate's own. The replay runs the source's own algorithm and is not an independent decision of coverage. Its exact premises, those of the declared net among them, were recomputed here, every shipped record and input was bound to the declared net and the expanded candidate, and the 5 October review found no defect. This repository's clean-room verifier sqverify-fast, extended to read a declared net, also decided all 416 directions here, a second implementation that is not yet a registered verifier and on which no rung rests.

    Hosono after Tokoharu and Levy, square-packing-bounds. Registration was requested in jlevy/squares#366. The source says parts of the work were produced with AI assistance under human direction.
    Significance
    Raised the verified lower bound at n=18 by 0.005, to within 0.123 of Hämäläinen's packing, by the certificate kind and checker of T-069 and later on a finer net that the same driver reads from the candidate: a parameter choice within the framework, no new technique, at S3 as those are. The 5 October review confirmed the draft.
    Novelty
    previously-published Present in an identified source
    Records

    n = 18registerevidence 1evidence 2sourcereview

  • T-099 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-06 · n = 18

    Mixed rectangle-measure lower bound verified at n=18, on a finer 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 s(18)≥588/125 = 4.704.

    The certificate is a density of 209 uniform rectangles in D4 orbits, and no point mass, of total mass 1799999/100000, on a net it declares itself: core side 1999/2000 and 832 half-angle tangents of step 1/2006, finer than the 416 of step 1/1001 at core 999/1000 that T-096's certificate declares. Since 1999/2000 (1 + 1/2006) = 4011993/4012000 < 1, and the last tangent 831/2006 is past tan(pi/8), every unit square contains a concentric core of side 1999/2000 at a net angle strictly in its interior.

    The source reports every such core capturing mass at least one: at all 831 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 changed only to allow more workers, and at the axis by exact integer tables.

    The value is above T-096's 47/10, the source's earlier certificate and the reported and verified lower bound at n=18 before it, by 0.004, and supersedes it.

    The certificate was decided here on 6 October 2026 by sqverify-fast, this repository's clean-room measure verifier, at all 832 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 re-derived the 832-node net in exact arithmetic and found no defect. The source's own checker was also replayed here in full, the bundle's own driver over all 832 nodes with its assertions on, each returning the certificate's own record: confirmed, reproduced with the producer's code.

    Hosono 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.
    Significance
    The strongest verified lower bound on record at n=18, by 0.004 above T-096, and the strongest reported. The certificate kind and checker of T-069 and later on a net twice as fine as T-096's, a parameter choice the same driver reads from the candidate; no new technique, at S3 as T-096, T-074 and T-045 are. The 6 October review confirmed the draft.
    Novelty
    previously-published Present in an identified source
    Records

    n = 18registerevidence 1evidence 2evidence 3source 1source 2review

  • T-102 V3 C3 Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-06 · n = 18

    Mixed rectangle-measure lower bound verified at n=18, 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 s(18)≥941/200 = 4.705.

    The certificate is a density of 324 uniform rectangles in D4 orbits, and no point mass, of total mass 1799999/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 588/125 = 4.704 of T-099, the source's earlier certificate and the reported and verified lower bound at n=18 before it, by 0.001, 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 1234 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.

    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 n=18, by 0.001 above T-099, 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

    n = 18registerevidence 1evidence 2sourcereview

Verification

upper: replayed here; lower: replayed here

—

Rigidity

not rigid, numerically checked, numerical multiprecision

Evidence: E-translation-escape-not-rigid

Scope

Square 1 of the retained witness (witness id 2) translates 0.451416 along (1, 0) with the packing still valid, so the configuration admits a non-trivial feasible motion; 6 of its 18 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 drawing

Regularized by the Squares Project with Daniel's regularizer (evand/square-packing, MIT), with the project's modifications: retry rung dps-100, same-side exact re-solve (devtools.regularize_same_side). A drawing at the witness's own side: a pure regularization, which proves no new bound, so not a result; no registered result holds the packing.

Open questions
  • Blocker (source evidence): MacIver's historical n18 corollary depends on his n17 proof; its fourteen C1-C14 certificates and exact ledger/assembly scripts are absent from the inspected public source commit. E-n017-maciver-reported-lower
  • Blocker (source evidence): The complete source checker has not been independently replayed here. E-n017-anabologyco-weighted-certificate
  • Priority: Corollary 1.2 of '[MacIver 2026 n17]', a manuscript dated 8 August 2026, reports s(18) >= s(17) > (40sqrt(2)+19)/17 + 1/200, approximately 4.450208382054341. This historical monotonicity claim is weaker than the independently verified 4679/1000 and has not been replayed here. (MacIver)
Evidence and sources
30 evidence entries

E-n018-wand125-mixed-4705-sqverify-fast-replay, E-n018-wand125-mixed-4705-report, E-n018-wand125-mixed-4704-sqverify-fast-replay, E-n018-wand125-mixed-4704-source-replay, E-n018-wand125-mixed-4704-report, E-n018-wand125-mixed-470-source-replay, E-n018-wand125-mixed-470-report, E-wand125-rectangle-source-replay, E-wand125-rectangle-report, E-kingbird-upper-register, E-nagamochi-lower, E-basic-grid-upper, E-lifted-q7-upper, E-green17-sixteen-point-lower, E-green17-interval-audit, 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-n017-maciver-reported-lower, E-n018-fractional-certificate, E-n018-t028-fractional-certificate, E-n018-t029-fractional-certificate, E-n018-t030-fractional-certificate, E-fractional-interval-decision, E-n017-guzhou-r012-source-replay, E-n017-guzhou-r012-interval-decision

s(18) — open

External intake, 2026-10-06. Hosono’s check2 source reports s(18)≥941/200=4.705 (T-102), from a density of 324 rectangles of total mass 1799999/100000<18, on a net the certificate declares: core side 4999/5000 and 2073 half-angle tangents of step 1/5002. Since 4999/5000·(1+1/5002)<1, 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 588/125 (T-099) by 0.001. 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. Hosono’s README says parts of the work were produced with AI assistance under human direction.

External intake, 2026-10-06. Hosono’s finer-net source reports s(18)≥588/125=4.704 (T-099), since superseded (T-102), from a density of 209 rectangles of total mass 1799999/100000<18, on a net the certificate declares: core side 1999/2000 and 832 half-angle tangents of step 1/2006, twice as many as the net of the 5 October certificate below. Since 1999/2000·(1+1/2006)<1, every unit square contains a core at a net angle strictly in its interior. The source accepts it at every net angle by the same checker at threshold one. It is above the 5 October certificate’s 47/10 by 0.004. This repository’s clean-room verifier sqverify-fast decided it here on 6 October 2026 at all 832 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 also replayed here in full on 6 October 2026, the bundle’s own driver over all 832 nodes with its assertions on, each returning the certificate’s own record: confirmed, reproduced with the producer’s code. 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 s(18)≥47/10=4.7 (T-096), from a density of 136 rectangles of total mass 1799999/100000<18, on a net the certificate declares: core side 999/1000 and 416 half-angle tangents of step 1/1001, where its earlier mixed certificates use 9977/10000 and 201 tangents of step 83/40000. Since 999/1000·(1+1/1001)<1, 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 source’s rectangle certificate’s 939/200 by 0.005. Its complete replay here on 5 October 2026, the bundle’s own driver and the source’s unchanged checker on the pinned tarball, returned the certificate’s own record at all 416 net nodes, so it was also the verified lower bound until 2026-10-06, when the certificate above superseded it in both lanes. This repository’s clean-room sqverify-fast, extended to read a declared net, also verified all 416 directions; no rung rests on it. 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 the rectangle certificate rect_n18_L4695 at side 939/200=4.695, since superseded (T-096), with total mass 1799/100=17.99<18, 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-05. 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 the same certificate at side 939/200=4.695, with total mass 1799/100=17.99<18, 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.

Open. The best known packing gives s(18)≤4.82287566. The verified lower bound is s(18)≥941/200=4.705, from Hosono’s check2 certificate on its finest declared net (T-102, 2026-10-06, V3/C3), leaving a bound gap of 0.1179 to the reported record. It superseded the source’s certificate at 588/125=4.704 on a coarser declared net (T-099, 2026-10-06), the verified lower bound until later that day, and that one superseded the source’s certificate at 47/10=4.7 on a coarser declared net (T-096, 2026-10-05), which was the verified lower bound until 2026-10-06, and that one superseded Hosono’s rectangle-density certificate at 939/200=4.695 (T-045, 2026-10-02), which was the verified lower bound until 2026-10-05, and that one superseded this repository’s weighted fractional unavoidable-set certificate at 4679/1000=4.679 (T-030, 2026-09-19), which was the verified lower bound until 2026-10-02. That certificate is not inherited by monotonicity: only Condition 2 of the five mentions n, so an atom set of total mass 71573611/4000000=17.89340275 certifies its side for every integer strictly above that mass — 18 and upward. The bounds it superseded in turn: this repository’s own 1871/400=4.6775 (T-029, 2026-09-19), which held until later on 2026-09-19; 187/40=4.675 (T-028, 2026-09-19), previously; 467/100=4.67 (T-027, 2026-09-18), previously; 459/100=4.59 (T-019, 2026-09-04), which still holds n = 17; the selected external report 9141/2000=4.5705; the n=17 Massaccesi certificate’s 22529/5000=4.5058, carried here by monotonicity as T-016; the first-party sixteen-point certificate’s 4.426213 (T-002); and Nagamochi’s general 4.316625 (closed form: s(N)≥min(⌈N⌉,N−2·⌊N⌋+1+1)). 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

Hämäläinen’s 1980 packing, at the tilt arcsin((7−1)/4) DS7 names exactly, for which the survey states the angle but no generating rule. cases/lifted_q7 lifts the retained witness’s every coordinate into Q(sqrt 7) at small height — the repository’s first exact verification outside Q(sqrt 2) — 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 (D-398, and the operation D-402 does not foreclose).

The lower bound

The earlier external report, [n17 weighted certificates 2026-09-20], gives the lower-bound expression 461300/99999 for s(18) (approximately 4.613046130461). Guzhou0806’s R012 parent-angle certificate of 20 September 2026 states s(17) >= 461300/99999 = 4.61304613 …, and both its own exact replay and this repository’s interval decision accept all 2925 catalogue entries. R012’s ATTRIBUTION.md names it as research by “Guzhou0806 / N17 project, with AI assistance”. Inherited at n=18 by monotonicity. Hosono’s rectangle-density certificate above replaced it in the reported field, and was also the verified lower bound from its replay here on 2026-10-02 until Hosono’s mixed certificate on a declared net (T-096) replaced it in both on 2026-10-05, and T-099 replaced that one in both on 2026-10-06. The source audit compares the exact theorem expressions separately from opaque table decimals.

MacIver’s manuscript dated 8 August 2026 separately reports s(18)≥s(17)>(402+19)/17+1/200≈4.450208382054341, in Corollary 1.2. The archived source review records it as a historical claim whose essential certificate and replay files are absent from the inspected public snapshot. It does not change the stronger verified bound below.

Until 2026-10-02 the operative bound was this repository’s own T-030 certificate at side 4679/1000: 957 rationally weighted atoms on a D4-symmetric site set, total mass 71573611/4000000=17.89340275<18, every closed B-square at every net direction capturing mass at least one, the least being 200001/200000. 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. The site set is BC-191 auto grids (32,43,54) unioned with T-029’s 804 atom sites scaled from 1871/400 to 4679/1000, plus a windows-5 lattice. Auto at this side resolved to (32,43,54), the same triple T-029 used. The row loop never crossed 18 and converged. No monotonicity step is involved and none is needed: the covering program the search solves does not contain n at all, and Condition 2 — total mass strictly below n — is the only place n enters, so the same atoms certify the side at every size above their own mass. The certificate does not reach n = 17, whose mass must sit strictly below 17; T-019 still holds that case at 459/100. From n = 19 on the register already holds 24/5=4.80 (T-020), so this certificate is true there and weaker. A run at 117/25=4.68 drove three historical site sets in succession, 538, 578 and 618 orbits, and each returned a restricted optimum of exactly 18.000000. The T-019 seed that previously certified 467/100 as T-027 locked at 18.000000 there too, as did T-027’s own atoms. Adding sites can still lower a restricted optimum, so 117/25 is not barred. Four weaker bounds are retained for provenance: T-029’s 4.6775, which held this case until later on 2026-09-19; T-028’s 4.675, previously; T-027’s 4.67, previously; and T-019’s 4.59 below them, which held until 2026-09-18. 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 N≥4:

s(N)≥min{⌈N⌉,N−2⌊N⌋+1+1}

It is weaker here than the verified 4.679 bound recorded above.

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-n018-wand125-mixed-4705-sqverify-fast-replay replayed here shared components V-sqverify-fast (first-party)
verified upper E-lifted-q7-upper replayed here independent V-sqpack-verify (first-party)