T-006: s(13)=4

V3 C3 optimality confirmed

2010-09-13 published · Bentz; Daniel after Burns, Massaccesi · n=13

s(13)=4 (Bentz 2010, Theorem 9). Proved again, without cases, by Evan Daniel's weighted closed cover of [0,4]^2.

The second proof was kernel-checked in Lean 4 here on 30 September 2026: SquarePacking.s13_eq_4 : minSide 13 = 4, depending only on propext, Classical.choice and Quot.sound, built from the retained source with Mathlib's official cache. The cover's zero-margin property was also certified here by the source's zmx2 over every root of its D4 region.

The theorem is Bentz's. The case-free proof is Evan Daniel's, evand/square-packing, building on Burns's and Massaccesi's method, with an AI agent under human direction as his CREDITS.md says.

Significance, composition and next rung
Significance
A published exact value in the m^2 - 3 family; the score is the theorem's, not ours.
Composition
Two independent proofs of one value. Bentz's is compound, with Sections 3.1-3.2's case analysis read rather than machine-checked. Evan Daniel's case-free proof is complete as it stands: the Lean kernel checked s13_eq_4 from the definitions, including every one of the 209 cover chunks (E-n013-evand-casefree-cover-lean-kernel). A kernel check is machine evidence at V3: V5 also needs a human expert's review of the formalization, and the retained review of s13_eq_4 was written by an AI lane. The confirmation rung comes from the machine-method replay E-n013-evand-casefree-cover-zmx2-replay (C3); whether a kernel check itself counts toward C is the owner's open question.
Next rung
One named human expert's review of the formalization restores V5; C5 needs two, with the open-review pointer, beside the rebuild already done here. V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained. A second machine method on the same cover, for example a complete zeromargin.py sweep (1 h 42 min on 8 processes at the source) beside the zmx2 replay, would be shown beside the rung. Bentz's own route would reach C3 by machine-checking Sections 3.1-3.2's staged sets (typed on think-1o1f), which would also make it the second fully audited theorem of the paper.
Novelty
previously-published Present in an identified source

The case

Case record

n=13

4
345
3.6064.606
nn+1

Proven

s(13)=4

  • optimal
  • exact

Citation record n-013

lowerBentz 2010, Electron. J. Combin. 17, #R126 (confirmed T-006)

The case record

LowerUpper
Verified44
Reported44
Gap0 solved: the verified bounds meet

Results on the case

7 results in the register on n=13, oldest first, each with what it established and how it stands now.

  1. 2005 published T-007

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

    V0 C1 lower bound incomplete on this case, superseded by T-006

    Nagamochi · Nagamochi 2005 · source · register

  2. 2010-09-13 published T-006 this result

    s(13)=4

    V3 C3 optimality confirmed

    Bentz; Daniel after Burns, Massaccesi · Bentz 2010 · evand square-packing 2026-09-28 · packet · source 1 · source 2 · review · register

  3. 2026-08-31 established T-005

    Bentz 2010, Lemma 10 is false as printed and true as corrected to (1.74,1)

    V3 C3 correction confirmed

    Levy after Bentz · source · register

  4. 2026-09-04 published T-085

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

    V3 C3 correction confirmed

    Karakuş; chelokot · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register

  5. 2026-09-29 published T-058

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

    V3 C3 method limit confirmed

    wand125 after Tokoharu, Daniel · wand125 tools 2026 · packet · register

  6. 2026-09-29 published T-083

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

    V3 C3 lower bound confirmed on this case, superseded by T-006

    Karakuş · Karakuş 2026 · source · register

  7. 2026-10-07 published T-124

    Reported non-strict local minima for 178 source configurations

    V0 C0 restricted optimality recorded

    Daniel after Couzo · Daniel exact and local reports 2026 · packet · register