Bounds

Results in the register

• 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-020 S4 V3 C3 Levy after Burns, Massaccesi · 2026-09-04 · n = 19–21

  \(s(n) \ge 24/5 = 4.80\)$s(n)\ge 24/5=4.80$ for \(n = 19, 20, 21\)$n=19,20,21$

  Claim and records

  Claim

  \(s(19) \ge 24/5\)$s(19)\ge 24/5$, \(s(20) \ge 24/5\)$s(20)\ge 24/5$ and \(s(21) \ge 24/5\)$s(21)\ge 24/5$, 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 \(n = 20\)$n=20$ and 1 + sqrt(14) = 4.7416... at \(n = 21\)$n=21$ -- 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 \(n = 19\)$n=19$, +0.194449 at \(n = 20\)$n=20$ and +0.058343 at \(n = 21\)$n=21$, 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 \(n = 22\)$n=22$ 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 -- \(n = 17\)$n=17$'s top rung has 0.066920 and \(n = 12\)$n=12$'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 \(n = 19\)$n=19$ 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 \(n = 20\)$n=20$ and \(n = 21\)$n=21$ 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 \(n = 19\)$n=19$ 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 \(n = 20\)$n=20$ and \(n = 21\)$n=21$ and stops at \(n = 19\)$n=19$. 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 \(n = 20\)$n=20$ and \(n = 21\)$n=21$ 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 \(n = 19\)$n=19$, 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, \(s(19) \ge 963/200\)$s(19)\ge 963/200$ (T-045), superseded it at \(n = 19\)$n=19$ 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 \(n = 19\)$n=19$ against T-019's +0.0842, the largest single-case movement in the register; and at \(n = 20\)$n=20$ and \(n = 21\)$n=21$ 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

  n = 19n = 20n = 21registerevidence 1evidence 2

  n = 19n = 20n = 21registerevidence 1evidence 2

• T-021 S3 V3 C3 Levy after Burns, Massaccesi · 2026-09-05 · n = 20, 21

  \(s(n) \ge 97/20 = 4.85\)$s(n)\ge 97/20=4.85$ for \(n = 20, 21\)$n=20,21$

  Claim and records

  Claim

  \(s(20) \ge 97/20\)$s(20)\ge 97/20$ and \(s(21) \ge 97/20\)$s(21)\ge 97/20$, from this project's weighted fractional unavoidable-set certificate at container side 97/20 = 4.85. Both sizes held 24/5 = 4.80 from T-020 earlier the same week in this register's verified fields; the movement is +0.05 at each. The certificate does not reach \(n = 19\)$n=19$: its total mass is 19848723/1000000 = 19.848723, above nineteen, so Condition 2 gives it \(n = 20\)$n=20$ and upward and T-020's 24/5 rung, retained beside it, still carries \(n = 19\)$n=19$.
  
  The two sizes take no monotonicity step, for the reason T-020 gives: only Condition 2 mentions n among the five conditions, so an atom set of mass M certifies its side for every integer strictly above M. From \(n = 22\)$n=22$ on the register already holds 5, so the certificate is true there and weaker.
  
  Where the rung came from is worth the record. A pre-registered bisection of [24/5, 9977/2000] ran four rungs unattended. The uniform grid walled at this side -- its restricted optimum crossed twenty at round 31 of 32 and stood at 20.000439 with placements still violated -- while a second site set, the 24/5 certificate's own 2260 atoms scaled by 97/96 and unioned with the grids, converged below twenty at the same side. The certificate is the second construction's; the first construction's crossing is why H-062 asks for two.

  Composition

  Primary at both sizes: 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

  The margin is 0.151277 below twenty, wider than T-020's 0.077380 was, so the side was not pushed to where the covering value stops it either. What is new is that the stopping side is now bracketed rather than guessed: 39/8 = 4.875 walls on both constructions and 97/20 certifies, so the m = 5 covering wall lies in an interval of width 0.025, and 979/200 = 4.895 and 997/200 = 4.985 wall as well. H-062 asked for 0.02 and the four decided rungs give 0.025, so the hypothesis is unresolved rather than accepted; the round is exp-061 and the remaining rung is the midpoint by the same rule.
  
  One reading of the 4.985 wall does not survive inspection and is recorded here so nobody repeats it. Just below the ceiling the twenty-five axis-parallel B-squares of a 5 x 5 arrangement overlap only in strips of width 5B - L = 0.0035, and the restricted dual is checked at sites only, so a site set with no site in those strips makes twenty-five unit weights dual-feasible and the restricted optimum exactly 25.000000 whatever the covering value is. No uniform inset-1/2 grid at any count the lane could afford puts a site in every strip. The exactly round value this register has learned to distrust has, at m = 5, a mechanism.
  
  The \(n = 21\)$n=21$ half of the margin was taken on 2026-09-23: T-034 certifies 122/25 = 4.88 at \(n = 21\)$n=21$ from an unseeded site set and supersedes this result there. What this result still held alone was \(n = 20\)$n=20$, whose bound stayed 97/20 because T-034's atoms are too heavy for it, until wand125's replayed rectangle certificate, \(s(20) \ge 979/200\)$s(20)\ge 979/200$ (T-045), superseded it there on 2026-10-02. This result stays true as stated at both of its sizes.

  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 the same two sizes, one rung higher, and neither size changes character at 4.85. What it adds beyond a rung is a measurement rather than a theorem, and the measurement is registered as such: the m = 5 covering wall is bracketed to [97/20, 39/8] -- a certificate at 4.85, crossings above twenty on both constructions at 4.875 -- which is the first bracket this project has put around a covering wall, and it sits far below the method's ceiling of 4.9885 rather than at it. That bears on planning, not on the strength of this claim.

  Novelty

  apparently-novel Not found in the recorded search, subject to its stated gaps

  Records

  n = 20n = 21registerevidence 1evidence 2

  n = 20n = 21registerevidence 1evidence 2

• T-034 S3 V3 C3 Levy after Burns, Massaccesi · 2026-09-23 · n = 21

  \(s(21) \ge 122/25 = 4.88\)$s(21)\ge 122/25=4.88$

  Claim and records

  Claim

  \(s(21) \ge 122/25\)$s(21)\ge 122/25$, from this project's weighted fractional unavoidable-set certificate at container side 122/25 = 4.88. The case held 97/20 = 4.85 from T-021 in this register's verified field, and the movement is +0.03. The certificate does not reach \(n = 20\)$n=20$: its total mass is 5036431/250000 = 20.145724, above twenty, so Condition 2 gives it \(n = 21\)$n=21$ and upward, and T-021's 97/20 rung, retained beside it, still carries \(n = 20\)$n=20$.
  
  The size takes no monotonicity step, for the reason T-020 gives: only Condition 2 mentions n among the five conditions, so an atom set of mass M certifies its side for every integer strictly above M. From \(n = 22\)$n=22$ on the register already holds 5, so the certificate is true there and weaker.
  
  The site set is the plainest the generator offers: auto grids (34, 46, 56) at inset 1/2 with no seed and no windows, converged below twenty-one in 36 LP rounds. At the same side a T-021-seeded set ran out its deadline unconverged, and a five-window set converged but stalled the interval route on a seam where atom rows sit exactly B apart; neither run decides anything about the side.

  Composition

  Primary at \(n = 21\)$n=21$: 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, as for T-021; that is C3, with the two methods shown beside the rung. The standard-library verifier the review also ran is a second implementation of the sweep's method, so it adds nothing to that count.
  
  One adversarial AI review is retained, the mapped 2026-09-23 review by Fable at max thinking, which covers the complete claim: it re-decided the frozen bytes by three routes, checked each of the five conditions and the \(n = 21\)$n=21$-only scope, and found nothing that refutes them. A different agent than the lane that produced the certificate wrote it, inside the same session; it is not an external review, and it is not a human oversight record.

  Next rung

  The margin is 0.854276 below twenty-one, more than five times T-021's 0.151277 below twenty, so the side was not pushed to where the covering value stops it. H-240 froze it below X-047's estimated additive crossing near 4.886, which is an estimate and not a bound, and this run did not test it.
  
  A certificate for \(n = 21\)$n=21$ cannot exist above ceil(sqrt(21)) * B = 4.9885, leaving 0.1085 of runway above 122/25, and the best known packing is the trivial 5, so the ceiling binds first: the method could in principle close the case to within 0.0115 of the upper bound and can never reach it.
  
  The next rung is a pre-registered side above 122/25 on the same unseeded construction, read from the restricted optimum a converged run reaches. Set B's refusal is the instrument note to carry with it: a window lattice at pitch B puts atom rows exactly B apart, and the interval route stalls on the seam where an upright square has both closed edges on such a pair. A stall there is not a counterexample, and it decides nothing.
  
  V4 and C4 need a second adversarial AI review by a distinct reviewer and a human oversight record; rung 5 would need a proof-assistant formalization of the five-condition theorem, reviewed by human experts.

  Significance

  Scored at S3 by the calibration note T-020 wrote and T-021 applied: "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 one of the same sizes, one rung higher, and \(n = 21\)$n=21$ does not change character at 4.88. What it adds beyond the rung is a reading about the instrument rather than a theorem: the stock generator with no seed and no windows converged where the seeded and windowed site sets did not decide. The side also sits above 39/8 = 4.875, where both of H-062's constructions crossed twenty at \(n = 20\)$n=20$; a mass above twenty is consistent with that wall and says nothing about \(n = 20\)$n=20$.

  Novelty

  apparently-novel Not found in the recorded search, subject to its stated gaps

  Records

  n = 21registerevidence 1evidence 2

  n = 21registerevidence 1evidence 2

• T-050 S3 V3 C3 Daniel after Burns, Massaccesi · 2026-09-29 · n = 21

  \(s(21) \ge 5000/1001 = 4.995004995\ldots\)$s(21)\ge 5000/1001=4.995004995\dots$

  Claim and records

  Claim

  \(s(21) \ge 5000/1001\)$s(21)\ge 5000/1001$ = 4.995004995..., by Evan Daniel's weighted point certificate of 23 September 2026. It raised the verified bound by 2878/25025, about 0.115, over T-034.
  
  The certificate is 4,604 D4-invariant rational points in 580 orbits, total weight 260057/12500 = 20.80456 < 21, decided over the rational angle net at \(N = 6000\)$N=6000$ by the method of T-049.
  
  It was replayed here on 27 September 2026 by the source's Rust verifier at \(N = 6000\)$N=6000$, least captured weight 10000083/10^7 at bin 684 as the source records, and by its exact Python re-check on four bins including the binding one; the two are one angle-net method.
  
  Evan Daniel, evand/square-packing, building on Burns's and Massaccesi's method, with an AI agent under human direction as its CREDITS.md says.

  Next rung

  V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained. A second machine method would be the native parent-core decision, which certified rows 0 to 2,378 of 2,486 before it was stopped and projects to about 2.8 CPU-hours complete; its journal was not retained, so it must run again. Superseded as the verified lower bound on 2026-09-29 by Evan Daniel's \(s(21) = 5\)$s(21)=5$ (T-052); stays true as stated.

  Significance

  Moved \(n = 21\)$n=21$ by 0.115 over T-034 to within 5/1001 of the grid's 5, past this repository's own fixed-shrink ceiling of 4.9885 for the format. A substantive case result, S3; superseded within two days by the same author's exact value.

  Novelty

  previously-published Present in an identified source

  Records

  n = 21registerevidence 1evidence 2sourcereview

  n = 21registerevidence 1evidence 2sourcereview

• T-052 S4 V3 C3 Daniel after Burns, Massaccesi · 2026-09-29 · n = 21

  \(s(21) = 5\)$s(21)=5$, by a mixed cover of points and grid-line segments

  Claim and records

  Claim

  \(s(21) = 5\)$s(21)=5$: the lower half by Evan Daniel's mixed cover of 27 September 2026, the upper half by the \(5 \times 5\)$5\times 5$ grid.
  
  The cover is 7,536 weighted points of [0,5]^2 plus mass spread uniformly along 1,872 segments of length 1/50 on the interior grid lines, total 522368729933/(25*10^9) = 20.894749197 < 21, exactly D4-invariant. Every closed unit square in [0,5]^2 captures mass at least one, a boundary point and a segment along an edge counting in full.
  
  The source certifies that at margin zero with two separately written checkers, zm_mixed.py in exact rational arithmetic and the Rust zmx2 with outward-widened binary64 enclosures, and Lean proves minSide 21 = 5 from the one checker statement.
  
  zmx2 was replayed here in full on 28 and 29 September 2026, D4-reduced over 2,500 roots and unreduced over 20,000, every root's census equal to the source's; zm_mixed.py was only sampled.
  
  Evan Daniel, evand/square-packing, building on Burns's and Massaccesi's method, with an AI agent under human direction as its CREDITS.md says.

  Composition

  Compound: the lower half is E-n021-evand-mixed-cover-zmx2-replay (interval-certified, zmx2 replayed here), the upper half the grid (E-basic-grid-upper, exact-algebraic). The two machine entries differ in method, but they certify different halves; the lower half, which sets the minimum, stands on one replayed method, and the equality is C3, as T-008 reads its own halves.

  Next rung

  V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained. A complete zm_mixed.py re-sweep, about 12.9 CPU-hours at the source, recorded as a second, exact-algebraic entry, would give the lower half a second machine method; the shared pose-space architecture stays the residual common-mode risk. V5 would need the checker statement S21CheckerCover proved in Lean and a human expert's review of the formalization; the reduction s21_eq_five_of_checker, from that statement to \(s(21) = 5\)$s(21)=5$, was kernel-checked here on 2026-09-30 with the standard axioms only (the 2026-09-28 packet's receipts/lean/).

  Significance

  An exact value for a case that was open, the second of the s(k^2 - 4) family after T-051, and the release that introduced line mass on the grid lines, which is what makes a zero-margin cover below the count possible at an integer side. S4 by the anchor "a reusable technique"; T-053 reuses it at \(n = 45\)$n=45$.

  Novelty

  previously-published Present in an identified source

  Records

  n = 21registerevidence 1evidence 2evidence 3sourcereview

  n = 21registerevidence 1evidence 2evidence 3sourcereview

• T-055 S2 V3 C3 wand125 after Daniel, Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-09-29 · n = 21

  \(s(21) = 5\)$s(21)=5$ by a point-only route

  Claim and records

  Claim

  \(s(21) = 5\)$s(21)=5$ by a second, point-only route: the lower half by wand125's point-only measure, completed on 28 September 2026 with a Lean 4 reduction, the upper half by the \(5 \times 5\)$5\times 5$ grid.
  
  The lower half is Evan Daniel's s21_lower_4.9950.txt support (T-050) scaled by 1001/1000 and re-weighted, 4,604 D4-invariant entries of total 2624862500021/125000000000, with capture threshold q = 249987/250000 over every closed unit square in [0,5]^2, so that 21q exceeds the total by 999979/125000000000.
  
  The capture statement is decided by the source's own exact rational replay of a retained certificate tree over 5,000 root boxes, and Lean proves minSide 21 = 5 from that one hypothesis.
  
  That replay was run here in full on 29 September 2026, the source's runner unchanged: every stage passed, and its records match the source's M1 run, 45,436 of the 45,446 output files byte for byte and the rest in every certified quantity. The Lean overlay was not built here.
  
  wand125 after Evan Daniel, square-packing-bounds. The source names Daniel's mixed-cover proof (T-052) as first, claims no priority, and says its code was developed with Codex.

  Composition

  Compound, and the minimum is set by the lower half. The lower half is E-n021-wand125-point-endpoint-source-replay (exact-algebraic, the source's runner replayed here), the upper half the grid (E-basic-grid-upper); the equality is C3. The runner is the source's, so the replay confirms the source's run rather than adding a second method, and the Lean reduction, not built here, adds nothing to the rung.

  Next rung

  V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record; one adversarial review is retained. A build of the Lean overlay with its axiom receipt, and the runner's lemmas formalised (review F10), would be the road to rung 5. The controls end at the first root box that holds a pose, so neither exercises the sieve or frontier stages; a control refused deeper in the tree would test more of the runner.

  Significance

  A second, point-only route to a value T-052 already holds, with a positive-margin threshold rather than a zero-margin cover and a Lean reduction of its own. A citable detail that changes no theorem.

  Novelty

  previously-published Present in an identified source

  Records

  n = 21registerevidence 1evidence 2evidence 3sourcereview

  n = 21registerevidence 1evidence 2evidence 3sourcereview

• 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-081 S4 V0 C1 Daniel after Burns, Massaccesi · 2026-10-03 · 14 cases

  \(s(k^2 - 4) = k\)$s(k^2-4)=k$ for every integer \(k\)$k$ from 5 up; \(k = 5\ldots18\)$k=5\dots 18$ are the cases held here

• 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$

In the frontier survey On GitHub