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-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-051 S4 V3 C3 Daniel after Burns, Massaccesi · 2026-09-29 · n = 32

  \(s(32) = 6\)$s(32)=6$

  Claim and records

  Claim

  \(s(32) = 6\)$s(32)=6$: the lower half by Evan Daniel's weighted closed cover of 26 September 2026, the upper half by the \(6 \times 6\)$6\times 6$ grid.
  
  The cover is 13,085 D4-invariant rational points of [0,6]^2, total weight 3171350535386/10^11 = 31.713505354 < 32, such that every closed unit square in [0,6]^2 captures weight at least one, a boundary point counting. A packing at side below 6 would scale to 32 disjoint closed unit squares capturing at least 32.
  
  The margin is zero at the grid, so the source decides the cover by exhaustive exact pose-space subdivision of its D4 fundamental region (zeromargin.py, 7,200 root boxes), and a Lean theorem derives minSide 32 = 6 from that one checker hypothesis.
  
  The complete zeromargin.py sweep was replayed here on 27 September 2026 with the source's runner, checker and settings: all 7,200 roots certified, 164,130 boxes, every root's census equal to the source's.
  
  The source's third checker, zmx2, was run here on the same cover on 29 September 2026 with --pair-points: all 3,600 roots of the D4 region certified, 1,405,342 boxes, none uncertified. zmx2 is a second implementation of the same subdivision by the same author and agent. Its point test derives from zeromargin.py's, but it closes germs by its own pair lemma and decides by exact integer tests on outward-rounded binary64 enclosures of chord ends. On 2 October 2026 zmx2 was run here again with --sym-atoms, without the D4 fold, over all 28,800 roots of the whole pose space: none uncertified, and every root's census equal to the source's run.
  
  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 upper half is the \(6 \times 6\)$6\times 6$ grid replayed exactly by the basic-bounds checker (E-basic-grid-upper), a construction its replay establishes, so under epistemics.md's Scope and Composition the equality takes the C of its lower half, which sets the rung.
  
  The lower half rests on complete replays here of the source's zero-margin pose-space subdivision by two checkers whose method values differ: zeromargin.py, exact-algebraic, over the 7,200 roots of the D4 fundamental region (E-n032-evand-closed-cover-source-run), and zmx2, interval-certified, over the 3,600 roots of the D4 region (E-n032-evand-closed-cover-zmx2-replay) and, with --sym-atoms and no fold, over all 28,800 roots of the whole pose space (E-n032-evand-zmx2-full-sym-replay). That is C3, with the two methods shown beside the rung.
  
  The two checkers differ in how germs are closed (zmx2's pair lemma Z and pair dynamic programme over lines one unit apart, against zeromargin.py's monotone chains), in arithmetic and in their parsers. Taken as zeromargin.py's run and zmx2's run without the fold, they no longer share the D4 fold, the region or any symmetry premise: the zmx2 side rests on its own Lemma A (search/ZMX2.md section 4.9, proved, and checked against the code by the 2 October review) where zeromargin.py's rests on the fold, which the source's Lean development kernel-checks, and nothing in zeromargin.py corresponds to Lemma A.
  
  The common mode is what remains shared: the author and AI agent and the statement decided; the point-in-square formulation, G0-G3 with the corner-and-vertex rule, one design in two arithmetics, which for a point cover is the primitive that decides most leaves; the pose parametrisation; and the branch-and-bound architecture. The source's Lean development kernel-checks the formulation on zeromargin.py's side, which bounds the common mode and does not remove it. The two checkers are separately written, not independent.
  
  The point test is shared by derivation: on 1 October 2026 the source stated that zmx2 was written to be independent of zm_mixed.py only and that its author was permitted to read zeromargin.py, so Lemma P derives from zeromargin.py's G0-G3 (jlevy/squares#238, retained as packing/resources/web/evand-square-packing-2026-10-01/issue-238-author-2026-10-01.json). The brief that governed that reading was not public when this entry was reviewed. The source published it on 3 October, and the 4 October evand packet retains it (s12/tasks/s21-finish/xcheck.md, think-83zc): it forbids zm_mixed.py and its write-up and permits zeromargin.py, zmcheck and their write-ups, as the source said.

  Next rung

  V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained; whether a mapped same-project review of another author's result counts toward them is the owner's decision. V5 needs the source's hypothesis-free Lean theorem s32_eq_6 built, which decides a generated box tree in the kernel with zeromargin.py only as the tree generator's untrusted oracle, and a human expert's review of the formalization. Mathlib's build cache became reachable on 2026-09-30, and the conditional s32_eq_six_of_checker and s13_eq_4 were built here (the 2026-09-28 packet's receipts/lean/). The cost that remains is compute: a probe puts s32_eq_6 at 14 to 28 CPU-hours emitted in about 320 parts of about 4 GB each, with 8 to 10 GB for the generator (think-angg).
  
  Beside the rung, the source's zmx2 --full --pair-points --sym-atoms run was replayed here on 2 October (think-48e1, E-n032-evand-zmx2-full-sym-replay), which took the D4 fold out of what the two checkers share. It changes neither rung: it is evidence of the kind already held, a machine replay of the source's own checker with a mapped review, as section 8 of the 2 October review says, and what it changes is the composition that rung 4's reviewers and oversight record will read.

  Significance

  An exact value for a case that was open, the first this record holds for s(k^2 - 4) with k >= 4, 0.204 above Nagamochi's closed form. S4 by the anchor "a reusable technique": the zero-margin closed cover decided by exhaustive pose-space subdivision, which the same author carried to \(n = 21\)$n=21$ and 45 (T-052, T-053) and wand125 to \(n = 45\)$n=45$ (T-054). Not S5: \(n = 32\)$n=32$ is not a central open case of this project.

  Novelty

  previously-published Present in an identified source

  Records

  n = 32registerevidence 1evidence 2evidence 3evidence 4evidence 5evidence 6source 1source 2review 1review 2review 3

  n = 32registerevidence 1evidence 2evidence 3evidence 4evidence 5evidence 6source 1source 2review 1review 2review 3

• 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