Bounds

Results in the register

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

  \(s(18) \ge 4426213/1000000\)$s(18)\ge 4426213/1000000$, by monotonicity from T-001

  Claim and records

  Claim

  \(s(18) \ge 4426213/1000000\)$s(18)\ge 4426213/1000000$, by monotonicity from T-001 (a packing of 18 unit squares contains a packing of 17).

  Composition

  Derived: the minimum over T-001 and the monotonicity step, which is one recorded line (any 18-packing contains a 17-packing) carried in the evidence limitations and the n-018 case body; both inputs sit at V3/C3, so the derived claim keeps the rungs.

  Next rung

  Rises with T-001; a bespoke \(n = 18\)$n=18$ set stronger than the inherited bound would be a new result, not a rung change.

  Significance

  The same movement carried to \(n = 18\)$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

  n = 18registerevidence 1evidence 2

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

  The sixteen-point set's unavoidability ceiling lies in \([4426213/1000000, 4427/1000)\)$[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.

  Composition

  Compound: the lower side of the bracket carries T-001's two methods and the refutation side rests on the interval audit alone. Both are machine-replayed here, so the bracket is C3; a second method on one side does not change the rung. The equality reading is deliberately not this claim.

  Next rung

  think-iye2: the shared certifier generalized to a Q(sqrt 2) scalar certifies at the ceiling exactly and an exact escape family above it turns the bracket into an equality at C3.

  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

  n = 17n = 18registerevidence 1evidence 2

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

  \(s(n) \ge \min(\lceil\sqrt{n}\rceil, \sqrt{n - 2\lfloor\sqrt{n}\rfloor + 1} + 1)\)$s(n)\ge min(\lceil \sqrt{n}\rceil ,\sqrt{n-2\lfloor \sqrt{n}\rfloor +1}+1)$ for \(4 \le n \le 324\)$4\le n\le 324$

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

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

  Claim and records

  Claim

  \(s(18) \ge 22529/5000\)$s(18)\ge 22529/5000$ and \(s(19) \ge 22529/5000\)$s(19)\ge 22529/5000$, by monotonicity from T-015 (a packing of n >= 17 unit squares contains a packing of 17). At \(n = 19\)$n=19$ this replaces Nagamochi's 1 + sqrt(12) = 4.4641... since (22529/5000 - 1)^2 = 307265841/25000000 > 12; at \(n = 20\)$n=20$ 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 \(n = 18\)$n=18$ or \(n = 19\)$n=19$ 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 \(n = 18\)$n=18$ and \(n = 19\)$n=19$ 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 \(n = 18\)$n=18$ (+0.079587 over T-002) and \(n = 19\)$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

  n = 18n = 19registerevidence 1evidence 2

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

  \(s(n) \ge 459/100 = 4.59\)$s(n)\ge 459/100=4.59$ for \(n = 17, 18, 19\)$n=17,18,19$

  Claim and records

  Claim

  \(s(17) \ge 459/100\)$s(17)\ge 459/100$, and \(s(18) \ge 459/100\)$s(18)\ge 459/100$ and \(s(19) \ge 459/100\)$s(19)\ge 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\)$n=20$, where Nagamochi's 1 + sqrt(13) = 4.6055... is larger -- the certificate does prove \(s(20) \ge 459/100\)$s(20)\ge 459/100$, 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 \(n = 12\)$n=12$ 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 \(n = 18\)$n=18$ 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 \(n = 17\)$n=17$'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 \(n = 17\)$n=17$ that is 5B = 4.9885, so 459/100 still has 0.3985 of runway. Unlike \(n = 12\)$n=12$, 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 \(n = 17\)$n=17$. 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 \(s(n)\)$s(n)$ >= 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. \(n = 17\)$n=17$ had 0.0855 to its best known packing at 4.675530; \(n = 18\)$n=18$ had 0.2329 to 4.822876 and \(n = 19\)$n=19$ had 0.2956 to 4.885618, both still carrying this certificate's side in the verified register; and \(n = 20\)$n=20$ 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 \(n = 18\)$n=18$ and leave \(n = 17\)$n=17$ 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 \(n = 19\)$n=19$ and moves \(n = 20\)$n=20$ and \(n = 21\)$n=21$ as well. What this result still holds alone is \(n = 17\)$n=17$ and \(n = 18\)$n=18$: 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 \(n = 17\)$n=17$ the reading is unchanged and the runway is 0.3985 to the ceiling and 0.0855 to the packing. For \(n = 18\)$n=18$, 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 \(n = 17\)$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

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

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

  \(s(18) \ge 467/100 = 4.67\)$s(18)\ge 467/100=4.67$

  Claim and records

  Claim

  \(s(18) \ge 467/100\)$s(18)\ge 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\)$n=17$, where T-019 still holds 459/100. From \(n = 19\)$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.

  Composition

  Primary at \(n = 18\)$n=18$: one certificate, one accepted verdict, the bound being the container side directly, with no monotonicity or composition step between the artifact and the claim. 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 on the frozen bytes; that is C3, with the two methods shown beside the rung. As with T-020 there is no independent evaluator and no review record, so rung 4 waits on two adversarial AI reviews and a human oversight record.

  Next rung

  T-028 took the next rung at 187/40 on 2026-09-19. This result stays true as stated and keeps its bytes at certificate-467-100.json. The remaining runway to the packing is now T-028's business. V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained.

  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\)$n=18$, one size-specific covering rather than T-019's Condition 2 carry, and \(n = 18\)$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\)$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

  n = 18registerevidence 1evidence 2

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

  \(s(18) \ge 187/40 = 4.675\)$s(18)\ge 187/40=4.675$

  Claim and records

  Claim

  \(s(18) \ge 187/40\)$s(18)\ge 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\)$n=17$, where T-019 still holds 459/100. From \(n = 19\)$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\)$n=18$ is off the H-218 sweep, so this retain does not confirm that claim.

  Composition

  Primary at \(n = 18\)$n=18$: one certificate, one accepted verdict, the bound being the container side directly, with no monotonicity or composition step between the artifact and the claim. 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 on the frozen bytes; that is C3, with the two methods shown beside the rung. As with T-027 there is no independent evaluator and no review record, so rung 4 waits on two adversarial AI reviews and a human oversight record.

  Next rung

  T-029 took the next rung at 1871/400 on 2026-09-19. This result stays true as stated and keeps its bytes at certificate-187-40.json. The remaining runway to the packing is now T-029's business. V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained.

  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\)$n=18$, one size-specific covering rather than T-019's Condition 2 carry, and \(n = 18\)$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\)$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

  n = 18registerevidence 1evidence 2

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

  \(s(18) \ge 1871/400 = 4.6775\)$s(18)\ge 1871/400=4.6775$

  Claim and records

  Claim

  \(s(18) \ge 1871/400\)$s(18)\ge 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\)$n=17$, where T-019 still holds 459/100. From \(n = 19\)$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\)$n=18$ is off the H-218 sweep, so this retain confirms H-219, not H-218.

  Composition

  Primary at \(n = 18\)$n=18$: one certificate, one accepted verdict, the bound being the container side directly, with no monotonicity or composition step between the artifact and the claim. 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 on the frozen bytes; that is C3, with the two methods shown beside the rung. As with T-028 there is no independent evaluator and no review record, so rung 4 waits on two adversarial AI reviews and a human oversight record.

  Next rung

  T-030 took the next rung at 4679/1000 on 2026-09-19. This result stays true as stated and keeps its bytes at certificate-1871-400.json. The remaining runway to the packing is now T-030's business. V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained.

  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\)$n=18$, one size-specific covering rather than T-019's Condition 2 carry, and \(n = 18\)$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\)$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

  n = 18registerevidence 1evidence 2

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

  \(s(18) \ge 4679/1000 = 4.679\)$s(18)\ge 4679/1000=4.679$

  Claim and records

  Claim

  \(s(18) \ge 4679/1000\)$s(18)\ge 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\)$n=17$, where T-019 still holds 459/100. From \(n = 19\)$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\)$n=18$ is off the H-218 sweep, so this retain confirms H-221, not H-218.

  Composition

  Primary at \(n = 18\)$n=18$: one certificate, one accepted verdict, the bound being the container side directly, with no monotonicity or composition step between the artifact and the claim. 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 on the frozen bytes; that is C3, with the two methods shown beside the rung. As with T-029 there is no independent evaluator and no review record, so rung 4 waits on two adversarial AI reviews and a human oversight record.

  Next rung

  The retained certificate's total is 71573611/4000000 = 17.89340275, leaving 426389/4000000 = 0.10659725 below eighteen, and that margin is what a further rung has to be found inside. The side above it, 117/25 = 4.68, locked at 18.000000 on the T-019-seeded construction, on T-027's own atoms, on T-028's own atoms, and on three earlier site sets; adding sites can still lower a restricted optimum, so 117/25 is not barred. The remaining interval to that plateau is 0.001. The method's ceiling is 5B = 4.9885, and the best known packing is 4.82287566, so the real runway is 0.1439 to the packing. V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained.
  
  Superseded as the verified lower bound on 2026-10-02 by wand125's replayed \(s(18) \ge 939/200\)$s(18)\ge 939/200$ (T-045), so a further rung of this method moves the case only above 4.695; stays true as stated.

  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\)$n=18$, one size-specific covering rather than T-019's Condition 2 carry, and \(n = 18\)$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\)$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

  n = 18registerevidence 1evidence 2

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

  Rectangle-density lower bounds replayed at 15 counts in \(n = 18\ldots78\)$n=18\dots 78$

• T-046 S3 V0 C0 wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-09-29 · 48 cases

  Rectangle-density lower bounds reported for 48 counts in \(n = 18\ldots95\)$n=18\dots 95$

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

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

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

  \(s(n) \ge 1/2 + \sqrt{n - \lfloor\sqrt{n}\rfloor + 1/4}\)$s(n)\ge 1/2+\sqrt{n-\lfloor \sqrt{n}\rfloor +1/4}$ for every nonsquare \(8 \le n \le 324\)$8\le n\le 324$

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

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

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

  Mixed rectangle-measure lower bound replayed at \(n = 18\)$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) \ge 47/10\)$s(18)\ge 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\)$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.
  
  wand125 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.

  Composition

  One claim on one certificate, on its own reported entry and its own replay entry. E-n018-wand125-mixed-470-source-replay replays it in full with the bundle's own driver and the source's checker: one interval-certified method, reproduced with the producer's code, C3. Coverage is decided by the source's C++ checker alone, byte for byte the checker the 28 September and 2, 3 and 5 October reviews read; the axis tables are a second implementation for one direction and not a second method.

  Next rung

  V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record; one adversarial review is retained. A second machine method would be a method-distinct decision of rotated coverage; the replay here runs the source's own checker. The checker's controls were made on the \(n = 37\)$n=37$ certificate of the same kind. A sqverify-fast evidence entry (think-3ok2) would show beside the rung as independently re-implemented.

  Significance

  Raised the verified lower bound at \(n = 18\)$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

  n = 18registerevidence 1evidence 2sourcereview

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

  Mixed rectangle-measure lower bound verified at \(n = 18\)$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) \ge 588/125\)$s(18)\ge 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\)$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.
  
  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 832 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. Beside it, the bundle's own driver replayed the source's checker over all 832 nodes, the axis tables among them, each returning the shipped record: a complete reproduction with the producer's code, not a second method.

  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 second machine method would be a method-distinct decision of rotated coverage; the complete replay of the source's own checker already stands beside the rung (E-n018-wand125-mixed-4704-source-replay).

  Significance

  The strongest verified lower bound on record at \(n = 18\)$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

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

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

  Mixed rectangle-measure lower bound verified at \(n = 18\)$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) \ge 941/200\)$s(18)\ge 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\)$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.
  
  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 95 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 \(n = 18\)$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

  n = 18registerevidence 1evidence 2sourcereview

In the frontier survey On GitHub