$n=12$$n=12$

Bounds

Results in the register

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

  s(n)≥min(⌈n​⌉,n−2⌊n​⌋+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-017 S4 V3 C3 Levy after Burns, Massaccesi · 2026-09-04 · n = 12

  $s(12)\ge 99/25=3.96$$s(12)\ge 99/25=3.96$

  Claim and records

  Claim

  $s(12)\ge 99/25$$s(12)\ge 99/25$, by this project's weighted fractional unavoidable-set certificate at container side 99/25 = 3.96.
  
  This is the first lower bound specific to $n=12$$n=12$ in the retained corpus: the case previously held 2 + 4/sqrt(5) = 3.788854..., which is Stromquist's $s(11)$$s(11)$ bound inherited by monotonicity and says nothing about twelve squares in particular. The movement is +0.171146, and the case stays open against its conjectured optimum of 4, now by 0.04. Seven rungs are retained below it, 19/5 through 79/20.
  
  It also separates the two cases for the first time. The retained side exceeds Trump's 1979 packing of eleven squares at 3.877084, so $s(12)$$s(12)$ > $s(11)$$s(11)$ strictly, by at least 0.082916. Monotonicity gives only $s(12)$$s(12)$ >= $s(11)$$s(11)$; the strict inequality did not follow from anything on record before, because $n=12$$n=12$'s previous lower bound was $s(11)$$s(11)$'s own 3.788854 and sat below Trump's packing.

  Significance

  Scored against the rubric's anchor for S4, "a reusable technique, bound family, or resolved disputed value". What is retained is not one bound but an eight-rung ladder -- 19/5, 77/20, 97/25, 39/10, 393/100, 197/50, 79/20, 99/25 -- by a generator that applies at every n and that has since produced the $n=11$$n=11$ result as well, so this is a bound family rather than a case result.
  
  It is also the first bound located in the retained corpus that is proved about $n=12$$n=12$ rather than inherited from $n=11$$n=11$: the frontier case body had recorded that nothing specific to $n=12$$n=12$ had been proved there.
  
  Held below S5 because $n=12$$n=12$ is not a central open case, weighted resource counting predates this project, the recent pure-atomic rational direction-net architecture follows Burns, the LP parameter line follows Massaccesi, the second exact check shares a method family with the first, and the gap to the conjectured 4 is 0.04, which this approach does not close.

  Novelty

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

  Records

  n = 12registerevidence 1evidence 2

  n = 12registerevidence 1evidence 2

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

  $s(12)\ge 15680/3951=3.9686155\dots$$s(12)\ge 15680/3951=3.9686155\dots$

  Claim and records

  Claim

  $s(12)\ge 15680/3951$$s(12)\ge 15680/3951$ = 3.9686155..., by Daniel's weighted point certificate, published on 25 August 2026 and first seen here on 27 September. It raised the verified bound by 851/98775, about 0.0086, over T-017.
  
  The certificate is 1,736 D4-invariant rational points of total weight 11.9738036 < 12 such that every closed unit square in [0, 15680/3951]^2, at every angle, captures weight at least one, decided over the rational angle net 2 arctan(k/6000) with a per-bin shrink of 1/(cos d + sin d).
  
  It was replayed here on 27 September 2026 by the source's Rust arrangement-sweep verifier at $N=6000$$N=6000$, least captured weight 10000056/10^7 at bin 0 as the source records, and by its exact Python re-check on 50 bins. It was also decided completely by this repository's native parent-core interval branch and bound over all 2,486 rows, which shares nothing with the source's sweep and gives the strict $s(12)>15680/3951$$s(12)>15680/3951$.
  
  Daniel, evand/square-packing (formerly square-packing-12), building on Burns's and Massaccesi's weighted exact-rational covering method. The source's CREDITS.md says the work was produced with an AI agent under human direction.

  Significance

  Raised the verified lower bound at $n=12$$n=12$ by 0.0086 to within 0.0314 of the grid's 4, on two methods. The method is Burns's and Massaccesi's, as this repository's own $n=12$$n=12$ ladder is; the instance is new. A substantive case result, S3. It entered its source ten days before T-017 was scored, which bears on T-017's "first lower bound specific to $n=12$$n=12$" (the plan's open question 3) but not on this score. Confirmed on 11 October beside T-017 (S4, the $n=12$$n=12$ generator and its ladder) and T-079 and T-095 (S3, re-weightings of these points): an instance of the method at one count.

  Novelty

  previously-published Present in an identified source

  Records

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

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

• T-058 S2 V3 C3 Hosono 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-078 S2 V3 C3 Ryu after Daniel · 2026-10-03 · n = 12

  $s(12)\ge 31360/7901=3.9691178\dots$$s(12)\ge 31360/7901=3.9691178\dots$, Daniel's certificate rescaled by $7902/7901$$7902/7901$

  Claim and records

  Claim

  $s(12)\ge 31360/7901$$s(12)\ge 31360/7901$ = 3.96911783..., by squarepacker (Ryu) after Daniel, published on 2 October 2026 and reported on jlevy/squares#309. It raises the verified bound by 15680/31216851, about 0.000502, over T-049.
  
  The certificate is Daniel's 1,736-point weighted certificate of T-049 with every coordinate and the container multiplied by 7902/7901 and the weights unchanged, total 11.9738036 < 12. The rescaling and its verification on the finer angle net are Ryu's; the certificate and the verifier that decides it are Daniel's. Every closed unit square in [0, 31360/7901]^2, at every angle, captures weight at least one, decided over the rational angle net 2 arctan(k/24000) with a per-bin shrink of 1/(cos d + sin d). The nets $N=6000$$N=6000$ and 12000 refuse it, which a pass at one net does not need: each net's test is a complete sufficient condition.
  
  It was replayed here on 2 October 2026 by Daniel's verifier and by Ryu's own indep_check.cpp at $N=24000$$N=24000$, least captured weight 10000056/10^7 at bin 0 in both, as the source records, and decided completely by this repository's native parent-core interval branch and bound over all 9,942 rows, which shares nothing with the two sweeps and gives the strict $s(12)>31360/7901$$s(12)>31360/7901$.
  
  squarepacker (Ryu), s12-lower-bound, archived as Zenodo 10.5281/zenodo.23106582, after Daniel's certificate and verifier (T-049). The source's README says the rescaling, the verification runs and its checker were prepared with the help of an AI assistant from Anthropic, which it names.

  Significance

  True and replayed in full by three checkers, and it raises the verified lower bound at $n=12$$n=12$, but by 0.000502, moving the gap to the grid's 4 from 0.0314 to 0.0309. It rescales T-049's certificate until a finer angle net stops accepting it, which spends that certificate's slack and adds no technique, as the source says itself; T-061 is the precedent for scoring such a step by what it changes. Confirmed on 11 October beside T-061 and T-093 (S2, the other slack-spending steps) and against T-079 and T-095 (S3, new weights on the same points).

  Novelty

  previously-published Present in an identified source

  Records

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

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

• T-079 S3 V3 C3 Levy after Daniel · 2026-10-03 · n = 12

  $s(12)\ge 15680000/3949423=3.9702002\dots$$s(12)\ge 15680000/3949423=3.9702002\dots$, Daniel's points re-weighted

  Claim and records

  Claim

  $s(12)\ge 15680000/3949423$$s(12)\ge 15680000/3949423$ = 3.97020020..., by re-weighting Daniel's 1,736 points. It raises the verified lower bound by 33774720/31204391123, about 0.0010824, over Ryu's $s(12)\ge 31360/7901$$s(12)\ge 31360/7901$ (T-078), and leaves a gap of 117692/3949423, about 0.0298, to the grid's 4.
  
  The certificate keeps the points of Daniel's $s(12)$$s(12)$ certificate (T-049), every coordinate scaled by 3951000/3949423, and solves for new weights by linear programming over their 223 D4 orbits, with rows from the near-tight cells Daniel's verifier reports; the total is 14970347/1250000 = 11.9762776 < 12. Every closed unit square in [0, 15680000/3949423]^2, at every angle, captures weight at least one, decided over the rational angle net 2 arctan(k/96000) with Daniel's per-bin shrink.
  
  It was decided here three ways on 2 and 3 October 2026: by Daniel's verifier, built unmodified with overflow checks on, in the producing run and again by a review lane that did not produce it, both VERIFIED over all 39,765 bins, least captured weight 10000045/10^7; and by this repository's parent-core interval branch and bound over all 39,765 rows, which shares no code with the sweep or with the LP and gives the strict $s(12)>15680000/3949423$$s(12)>15680000/3949423$. Both checkers refuse two mutated certificates.
  
  This project's re-weighting, after Daniel's certificate and verifier (T-049), whose method is Burns's and Massaccesi's, and after Ryu's rescaling of that certificate (T-078), which showed a finer net leaves room for a larger container. The same work rescaled Daniel's certificate whole to $s(12)\ge 1568000/395039$$s(12)\ge 1568000/395039$, which this bound implies.

  Significance

  Raises the verified lower bound at $n=12$$n=12$ again, by 0.0016 over Daniel's T-049 and 0.0011 over T-078, to within 0.0298 of 4, the best verified bound at $n=12$$n=12$ this repository knows of. T-049, which raised it by 0.0086, is S3, and the step here is new weights on Daniel's geometry, not a rescaling alone. Not S4: the method, a weighted cover re-optimised at a finer net, is Daniel's, Burns's and Massaccesi's. Not S5: pure point covers are capped well short of 4, so the central question at $n=12$$n=12$ does not move. Confirmed on 11 October beside T-095 (S3, the next re-weighting) and against T-078 (S2, a rescaling).

  Novelty

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

  Records

  n = 12registerevidence 1evidence 2evidence 3evidence 4source 1source 2review

  n = 12registerevidence 1evidence 2evidence 3evidence 4source 1source 2review

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

  s(n)≥1/2+n−⌊n​⌋+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ş; Vlasenko · 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-095 S3 V3 C3 Ryu after Daniel, Levy · 2026-10-05 · n = 12

  $s(12)\ge 7943/2000=3.9715$$s(12)\ge 7943/2000=3.9715$, Daniel's points dilated and re-weighted

  Claim and records

  Claim

  $s(12)\ge 7943/2000$$s(12)\ge 7943/2000$ = 3.9715, by squarepacker (Ryu) after Daniel and this project's Route B (T-079), published on 5 October 2026 as release v1.1 of squarepacker/s12-lower-bound and reported on jlevy/squares#363. It raises the verified lower bound by 10266889/7898846000, about 0.0013, over T-079's 15680000/3949423, and leaves 57/2000 = 0.0285 to the grid's 4.
  
  The certificate keeps Daniel's 1,736 points of T-049, dilated by 31382793/31360000 to the container 7943/2000 and rounded to the grid 1/4000000 one D4 orbit at a time, every coordinate within 11/39200000 of its exact image, with new weights found by linear programming: all 223 orbits positive, total 119974808/10^7 = 11.9974808 < 12. Every closed unit square in [0, 7943/2000]^2, at every angle, captures weight at least one, decided over the rational angle net 2 arctan(k/96000) with Daniel's per-bin shrink. The nets $N=24000$$N=24000$ and 48000 refuse it, which a pass at one net does not need.
  
  It was decided here on 5 October 2026 by Daniel's verifier, reproduced with the producer's code: built from the retained source with overflow checks on, VERIFIED over all 39,765 bins, least captured weight 10000050/10^7 at bin 0, every line as the source's log; and independently re-implemented by this repository's parent-core interval branch and bound over all 39,765 rows, which shares no code with the sweep or with the search that made the weights and gives the strict $s(12)>7943/2000$$s(12)>7943/2000$. Ryu's own indep_check.cpp, replayed here at $N=96000$$N=96000$ and 192000 with the source's minimum, is the producer's evidence: the search stopped when its range-restricted copy found no violation. All three refuse the source's two altered certificates.
  
  squarepacker (Ryu), s12-lower-bound, archived as Zenodo 10.5281/zenodo.23157015, after Daniel's points and verifier (T-049) and this project's re-weighting of them (T-079), whose tool the source says guided its own scripts, written from scratch. The source says the rescaling, the re-weighting, the verification runs and its tools were prepared with the help of Claude (Anthropic).

  Significance

  Raises the verified lower bound at $n=12$$n=12$ by 0.0013 over T-079, the largest step since T-049. New weights on Daniel's points by T-079's recipe, Route B, with a complete scan in every cycle of the search, so no new technique and not S4; T-078, a rescaling, is S2, and T-079, new weights, is S3. Its source shows these points nearly exhausted for re-weighting, about 1.3e-4 below 560/141, which answers T-079's open "the same points may carry the bound further". Not S5: point covers are capped below 3.99.

  Novelty

  previously-published Present in an identified source

  Records

  n = 12registerevidence 1evidence 2evidence 3evidence 4source 1source 2review 1review 2

  n = 12registerevidence 1evidence 2evidence 3evidence 4source 1source 2review 1review 2

• T-124 S2 V0 C0 Daniel after Couzo · 2026-10-07 · 178 cases

  Reported non-strict local minima for 178 source configurations

In the frontier survey On GitHub