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-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.

  Composition

  Primary: one certificate, one verifier, one accepted verdict. The bound is the certificate's container side directly, with no monotonicity or composition step between the artifact and the claim.

  Next rung

  Two machine methods decide it. The independent re-derivation agrees but is exact-algebraic like the first; the second method is the interval-certified decision, which bounds coverage by branch and bound over boxes of centres with directed rounding: the two routes share the certificate and the closed-form conditions, and share no part of how Condition 5 is decided. The register shows the two methods beside the rung. V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained.
  
  The bound itself: the ladder 19/5, 77/20, 97/25, 39/10, 393/100, 197/50, 79/20, 99/25 was climbed once the separation oracle was corrected to score the cells the verifier decides (D-434), and every rung is retained.
  
  The retained certificate's total is 149987/12500 = 11.998960, leaving 0.001040 below twelve -- the tightest margin of any rung in the record, and it survived on the sign of a rounding rather than by design. The next tightest, two rungs below at 197/50, is about seven times wider.
  
  Rationalisation rounds each orbit up to a multiple of 1/scale, so its cost is at most atoms/scale; at 2097 atoms and scale 200,000 it took 0.005314, five times what remained. Raising the scale twentyfold would have cost about 0.00027 and would not have changed the atom count. That is a defaults question and it is BC-191's.
  
  Margin does not shrink monotonically as the ladder climbs -- the 197/50 rung two below this one has 0.007175 and 79/20 has 0.029410, so a tight rung is evidence about that run and not about how much room is left.
  
  This rung also cost the exhaustive tier, when it was retained: 2097 atoms is 1.8 times the next largest retained certificate, the 1184-atom \(n = 17\)$n=17$ rung, and the exact sweep is quadratic in the atom count, so deciding it took 4866 s where the interval route took 110 s. The sweep was rewritten the same day to decide in integers on the weights' common scale, in parallel over directions, and returns the same verdict in well under a minute; BC-195 owns whether the tier can still afford what it holds.
  
  What is left is bounded, though, and by the method rather than by the search. A certificate for n cannot exist above ceil(sqrt(n)) * B, since a container wider than that holds ceil(sqrt(n))^2 pairwise disjoint axis-parallel B-squares, each carrying mass at least 1 by Condition 5, which forces the total past n and breaks Condition 2. Here that ceiling is 4B = 3.9908 on this certificate's own B, and it is what binds: 4/(1 + D) = 3.990816 is the supremum over every shrink the 181-direction net admits, and the grid packing's 4 sits above both. So the retained 99/25 has 0.0308 of runway left.
  
  The consequence for this case is structural and worth stating exactly: the grid packing gives \(s(12) \le 4\)$s(12)\le 4$, the ceiling sits strictly below 4, and 4 is the conjectured value -- so no single certificate of this shape certifies \(s(12) \ge 4\)$s(12)\ge 4$, however fine the net or the site set. What the ceiling does not exclude is a proved family of certificates with sides tending to 4 and a limit argument on top of it; whether such a family exists is a question about the covering value, and an earlier version of this sentence overstated the ceiling into a method-wide impossibility (PR 78's adversarial review, F14). What remains is how close to 4 a certificate can get.

  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\ldots\)$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 Evan 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$.
  
  Evan Daniel, evand/square-packing (formerly square-packing-12), building on Sam Burns's and Gustavo Massaccesi's weighted exact-rational covering method. The source's CREDITS.md says the work was produced with an AI agent under human direction.

  Composition

  Primary at \(n = 12\)$n=12$: one certificate, no monotonicity. Two entries whose methods differ decide it, the source's exact arrangement sweep (exact-algebraic, replayed here) and this repository's directed-rounding interval coverage of every row (interval-certified); that is C3, with the two methods shown beside the rung. Both rest on the source's certificate and the same counting theorem, and the thin reader that maps the source's integer file onto parent-core rows has had no review reading of its own.

  Next rung

  A review reading of the native reader (devtools.verify_evand_angle_net_native) would close the one unread link in the second method's route. 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. Rung 5 needs a proof-assistant formalization reviewed by human experts. The exact value remains open; the conjecture is \(s(12) = 4\)$s(12)=4$.

  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.

  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 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-078 S2 V3 C3 squarepacker after Daniel · 2026-10-03 · n = 12

  \(s(12) \ge 31360/7901 = 3.9691178\ldots\)$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 Sungjoon) after Evan 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 squarepacker'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 squarepacker'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 Sungjoon), s12-lower-bound, archived as Zenodo 10.5281/zenodo.23106582, after Evan 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.

  Composition

  Primary at \(n = 12\)$n=12$: one certificate, no monotonicity. Two entries whose methods differ decide it: the producer's two arrangement sweeps, Daniel's verify and squarepacker's indep_check.cpp (exact-algebraic, replayed here, one method in two implementations), and this repository's directed-rounding interval coverage of every row (interval-certified); that is C3, with the two methods shown beside the rung. All three rest on the certificate, the counting theorem and the shrink lemma on the net \(N = 24000\)$N=24000$, and the native rows are Daniel's bins and sigma_k by design.

  Next rung

  V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record; the one retained review was written by the lane that ran the replays, so a separately prompted read is the next step. Rung 5 needs a proof-assistant formalization reviewed by human experts; the source notes that Daniel's Lean pose-box-tree checker, which kernel-checks T-049's certificate, could in principle take this one. The exact value remains open; the conjecture is \(s(12) = 4\)$s(12)=4$.

  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.

  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\ldots\)$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 Evan Daniel's 1,736 points. It raises the verified lower bound by 33774720/31204391123, about 0.0010824, over squarepacker'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 Evan Daniel's certificate and verifier (T-049), whose method is Burns's and Massaccesi's, and after squarepacker'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.

  Composition

  Primary at \(n = 12\)$n=12$: one certificate, no monotonicity. Two methods decide it: Daniel's arrangement sweep (exact-algebraic), run by the producing lane and replayed by the review lane, and this repository's directed-rounding interval coverage of every row (interval-certified); that is C3, with two methods shown beside the rung. The exact audit of the file is a premise check, well-formedness only, and decides nothing. All rest on the certificate, the counting step and the shrink lemma on the net \(N = 96000\)$N=96000$, and the native rows are the sweep's bins and sigma_k by design.

  Next rung

  V4 and C4 need a second adversarial AI review by a distinct reviewer and a human oversight record. Rung 5 needs a proof-assistant formalization reviewed by human experts; Daniel's Lean pose-box-tree checker, which kernel-checks T-049's certificate, could in principle take this one. The same 1,736 points carried the bound further: the LP total was 0.024 below 12 at this side, and squarepacker's re-weighting of them reached 7943/2000 (T-095). The exact value remains open; the conjecture is \(s(12) = 4\)$s(12)=4$.

  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.

  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) \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-095 S3 V3 C3 squarepacker 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 Sungjoon) after Evan 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$. squarepacker'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 Sungjoon), s12-lower-bound, archived as Zenodo 10.5281/zenodo.23157015, after Evan 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).

  Composition

  Primary at \(n = 12\)$n=12$: one certificate, no monotonicity. Two methods decide it: Daniel's arrangement sweep (exact-algebraic), the producer's verifier replayed here in full with overflow checks, and this repository's directed-rounding interval coverage of every row (interval-certified), which shares no code with it or with the search that made the weights; that is C3, with two methods shown beside the rung.
  
  squarepacker's indep_check.cpp, replayed here too, is a second implementation of the sweep's method and the producer's own, and its range-restricted copy was the search's stopping rule, so it is producer evidence and confirms nothing beyond the other two (review F3). The exact audit of the file is a premise check and decides nothing. All rest on the certificate, the counting step and the shrink lemma on the net \(N = 96000\)$N=96000$, and the native rows are the sweep's bins and sigma_k by design (review F9).

  Next rung

  V4 and C4 need a second adversarial AI review by a distinct reviewer and a human oversight record; the one retained review read the argument and computed nothing (its F1), so a second one that runs its own exact checks would add most. Rung 5 needs a proof-assistant formalization reviewed by human experts; Daniel's Lean pose-box-tree checker, which kernel-checks T-049's certificate, could in principle take this one, as the source notes. The source's own analysis puts re-weighting of these points near its end below 560/141 = 3.97163; a higher bound needs new points or another method, and point covers stop short of 3.99. The exact value remains open; the conjecture is \(s(12) = 4\)$s(12)=4$.

  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

In the frontier survey On GitHub