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-010 S4 V3 C3 Levy after Stromquist · 2026-08-31 · n = 11

  \(s(11) \ge 2 + 4/\sqrt{5}\)$s(11)\ge 2+4/\sqrt{5}$, by a repair of Stromquist 2003's Figure 14 point set

  Claim and records

  Claim

  \(s(11) \ge 2 + 4/\sqrt{5}\)$s(11)\ge 2+4/\sqrt{5}$, by a source-distinct repair of Stromquist 2003's Figure 14 point set: the replacement G' = (79/100, 37/20) restores the complete Figure 13 localization, A-triple forcing, repaired unavoidability, and 3+9 capacity chain, certified exactly. The printed argument does not close (exp-016) and is not relied on.

  Next rung

  V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained. A second independent mechanism, the pose-space interval audit built for T-001 run at side 2 + 4/sqrt(5) over the repaired twelve-point set, would be shown beside the rung. Rung 5 needs a proof-assistant formalization reviewed by human experts.

  Significance

  Resolves the proof status of the subject's flagship case: the \(n = 11\)$n=11$ lower bound was stated in 1979 and cited as proved since, its printed argument was falsified here, and this restores it with a source-distinct repair.

  Novelty

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

  Records

  n = 11registerevidence 1

  n = 11registerevidence 1

• T-011 S2 V3 C3 Trump · 2026-08-31 · n = 11

  Trump's 1979 packing is exactly valid, so \(s(11) \le 3.877083590022814\ldots\)$s(11)\le 3.877083590022814\dots$

  Claim and records

  Claim

  Trump's 1979 packing is exactly valid: 11 unit squares in a square of side the published degree-8 algebraic number 3.877083590022814..., with 14 of 55 pairs in exact zero-separation contact and 20 corner coordinates exactly on the boundary, so \(s(11)\)$s(11)$ <= that side.

  Next rung

  V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained. A second independent exact verification of the same degree-8 witness would be shown beside the rung (the retained rational control proves a slightly weaker side and does not confirm this claim). Rung 5 needs a proof-assistant formalization reviewed by human experts.

  Significance

  Confirms the record witness exactly, deciding the 14 zero-gap contacts no finite numerical evaluation can: real and citable, changing no theorem.

  Novelty

  previously-published Present in an identified source

  Records

  n = 11registerevidence 1

  n = 11registerevidence 1

• T-018 S5 V3 C3 Levy after Burns, Massaccesi · 2026-09-04 · n = 11

  \(s(11) \ge 381/100 = 3.81\)$s(11)\ge 381/100=3.81$

  Claim and records

  Claim

  \(s(11) \ge 381/100\)$s(11)\ge 381/100$, by this project's weighted fractional unavoidable-set certificate at container side 381/100 = 3.81. This improves Stromquist's 2 + 4/sqrt(5) = 3.788854..., stated in 1984 (Memo III, p. 10) and published in 2003.
  
  No intervening improvement was found by the recorded search, and \(n = 11\)$n=11$ was then the smallest open case. The movement was +0.021146, and the case stayed open against Trump's 1979 packing at 3.877084: the interval narrowed from 0.088230 to 0.067084. Two rungs are retained below it -- 19/5, the value that first passed Stromquist, and the 189/50 calibration rung below him.

  Composition

  Primary: one certificate, one verifier, one accepted verdict. The bound is the certificate's container side directly, with no monotonicity or composition step. It raises no other case: every n > 11 already carries a larger verified bound.

  Next rung

  A second machine method decides it, the interval-certified decision, which is independent in method and, deciding coverage on the doubled net, never invokes the D4 reflection and so does not need Condition 1 at all. One adversarial AI review is retained, PR 78's, ported here as a dated record on 2026-09-05; V4 and C4 need a second adversarial AI review by a distinct reviewer and a human oversight record. An outside mathematical review and an archival release would strengthen the priority record without changing this rung.
  
  The bound itself: 3.81 converged with margin -- objective 10.8603 against eleven, rationalised to 434547/40000 = 10.863675 -- so the next rung is a search question rather than a limit of the method. Getting there took two attempts at the same side, and the difference between them is worth keeping. The first stopped with its row loop still finding violated placements (final least 0.9764) and was refused by the exact sweep at directions 55 to 63, least cell 199531/200000. The second ran the loop to convergence -- three row rounds, 25318 rows, final oracle least mass exactly 1 -- and was accepted at every direction. An objective below n proves nothing on its own; the loop's stopping condition is the thing to read.
  
  Where it stops: 3.82 was then attacked from both sides and neither route closes. The covering LP was run on two independent site sets, and the two stop at exactly eleven for different reasons, which is worth separating because only one of them converged.
  
  The grid-built set, 6637 sites and 14820 rows at the end, ran its row loop to convergence and finished at an objective of exactly 11.000000, descending to it from 11.6 over twelve rounds and never crossing below.
  
  The set seeded from this certificate's own 1121 atoms, 24069 sites, has not converged and does not need to. Its objective has stood at 11.000000 through twenty-four row rounds and 30240 rows while the loop's least covered mass climbed from 0.8490 towards 1, reaching 0.9997 at the round the run was stopped -- so violated placements remained and the loop had not exhausted. Adding rows can only raise a restricted optimum, so the optimum for that site set is at least eleven whatever the loop does next, and no certificate exists on it. Reading the objective alone would have understated this: the loop's stopping state is what makes the conclusion independent of finishing.
  
  A certificate needs mass strictly below eleven, so neither site set yields one. The rejection route does not close either, and it is much further from closing than the search's own progress figures suggest. H-061's object was built and decided exactly: the converged dual is 76 squares, 608 after the D4 images, with a raw total of exactly 11, and sqpack.fractional.ceiling checked all 1650944 vertices of their arrangement, 272244 of them in exact arithmetic. The maximum pointwise depth is 1925/1152 = 1.671007, so the feasible total -- the raw total scaled to make the family a packing -- is 1152/175 = 6.5829 against the eleven a ceiling needs.
  
  The gap between that and the search's running estimate is the thing to carry forward. Column generation prices against a grid sample and reported a depth of 12/11 = 1.0909, which would have made the feasible total 121/12 = 10.08. The exact maximum is 53 per cent higher, because depth peaks at vertices of the arrangement that no grid samples. A ceiling must therefore be judged on the exact check and never on the sampled depth, which flatters it.
  
  One thing 3.82 is not: the method's ceiling. A certificate for n cannot exist above ceil(sqrt(n)) * B, because a wider container holds ceil(sqrt(n))^2 pairwise disjoint axis-parallel B-squares whose masses Condition 5 forces past n; for \(n = 11\)$n=11$ that is 4B = 3.9908, leaving 0.1808 of runway above the retained 381/100. The wall at 3.82 is a covering wall, met far below where the method stops working.
  
  If tau*(3.82) is exactly eleven then this is the one configuration where neither pre-registered route can close, since a certificate needs mass below n and a ceiling needs the scaled dual to reach n, and both fail by an infinitesimal at exactly n. That is a limit on the reach of the rejection route rather than a stalled search. It is recorded as measurement: two LP runs agreeing to six decimals is evidence about the restricted optima, not a proof that tau* equals eleven, and nothing here rules out a site set neither run found.

  Significance

  Scored against the rubric's own anchor for S5, "movement on a central open case". \(s(11)\)$s(11)$ is the smallest open case and a central one for this project; the recorded public search found no movement beyond Stromquist's value, stated in 1984 and published in 2003, and this displaces a bound from the refereed literature rather than an inherited or closed-form one.
  
  What S5 does not claim: the weighted-resource lineage predates this project and the pure-atomic direction-net architecture follows Burns and Massaccesi, so what is new is an instance and the generator that found it; apparent novelty is not absolute priority; and the remaining gap to Trump's 1979 packing is 0.067, which this approach does not close. The calibration rung at 189/50, below Stromquist's bound, was run first by design and is retained.

  Novelty

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

  Records

  n = 11registerevidence 1evidence 2

  n = 11registerevidence 1evidence 2

• T-022 S5 V3 C3 Levy after Burns, Massaccesi · 2026-09-06 · n = 11

  \(s(11) \ge 38100\sqrt{8100042893309449}\mathbin{/}899996306539 = 3.8100257\ldots\)

  Claim and records

  Claim

  \(s(11) \ge 38100\)$s(11)\ge 38100$*sqrt(8100042893309449)/899996306539 = 3.810025723614703, proved by an exact dilation-limit corollary of T-018's retained certificate. For every positive rational q with q^2 below 810004289330944900000000/809993351783841654158521, common scaling preserves the source hypotheses other than containment, and the exact sharpened containment lemma rules out a packing at side qL. Rational density and upward embedding exclude every real side below the supremum, which proves the displayed lower bound. The direct certificate family covers strict rational sides below the supremum; the density-and-embedding step supplies the exact >= conclusion at the supremum.

  Composition

  Derived from a full replay of T-018's accepted five-condition source, scaling equivariance for Condition 1, invariance of Conditions 2 and 3, inverse-dilation preservation of Condition 5, and a separate sharpened containment lemma proved by an exact rational-square comparison. Rational density and upward embedding then supply the limit step. The mapped, non-superseded source-distinct review independently re-derived the theorem and attacked the endpoint, frozen-Condition-4, compactness, scale, and byte-trust boundaries. It is one adversarial AI review, by an agent of this project, and not a human oversight record, so the result is C3; nor is the review a method-distinct second derivation.

  Next rung

  V4 and C4 need a second adversarial AI review by a distinct reviewer and a human oversight record beside the mapped 2026-09-06 source-distinct review. A second, method-distinct derivation would be shown beside the rung and would not improve the bound. This dilation limit is only the uniform fixed-B, single-core strict-containment supremum. Direction-specific cores, two-core endpoint averaging, or exact fixed-atom core shrinkage might extract more from the same data; the present argument does not establish \(s(11)\)$s(11)$ greater than the displayed bound.

  Significance

  The rubric's S5 anchor is movement on a central open case, and this raises the proved lower bound for the smallest open case by about 0.0000257236147034 beyond T-018. The movement derives from an exact support identity and unused strictness margin in an existing certificate; it is not a new certificate architecture and leaves a gap of about 0.0670578664 to Trump's packing.

  Novelty

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

  Records

  n = 11registerevidence 1evidence 2evidence 3source

  n = 11registerevidence 1evidence 2evidence 3source

• T-023 S3 V3 C3 Levy · 2026-09-08 · n = 11

  Conditional exclusion: no eleven-square packing in the four-owner branch at \(q = 96/25\)$q=96/25$

  Claim and records

  Claim

  At q = 96/25, if four distinct unit squares have selected strict cores of side B = 9977/10000 containing, respectively, the four closed rational patches in arms.endpoint.footprint_union of the retained exp143 receipt, at most five further unit squares fit. Thus the specified four-owner branch contains no eleven-square packing. The five saved rational dots meet every admissible remaining core on the complete 361-direction net; audited containment and boundary arguments transfer this exact check to arbitrary physical angles. This is a conditional exclusion and changes no global bound for \(s(11)\)$s(11)$.

  Composition

  Exact full-net coverage and frozen-data identities are machine-checked and replayed here. Universal owner footprint containment, extension to event boundaries, and strict-core selection for physical squares are audited analytic proof steps, so the composed theorem is V3. Exp145 adds an independent inclusion-exclusion computation of the same finite cover. The analytic owner and physical-angle transfer premises remain shared, and the composed theorem is C3; C4 would need two adversarial AI reviews by distinct reviewers and a human oversight record.

  Next rung

  Exp145 completes the independent finite-union check. Assemble a review packet for the shared analytic premises before revisiting confirmation. V4 for the whole theorem requires mechanizing the analytic transfer, and with C4 two adversarial AI reviews by distinct reviewers and a human oversight record.
  
  Exp146 enlarged twelve wall-aware footprints, but exp147 transferred no additional tuple. Exp149 refuted the selected five-dot extension and exp150 showed its escape survives individual owner-core constraints. Exp151 also refuted a fixed sixth-site extension. Exp152 found a nonempty two-core site region, but exp153 then refuted the entire fixed-D-plus-one-site family with 188 exact support directions.
  
  Next audit a short actual-core obstruction and determine whether it is a disjoint pair or only a higher-order obstruction before drawing weighted-mass conclusions. Wider owner-class coverage remains a new research result, not a rung change.

  Significance

  A substantive case exclusion at a central open size, demonstrating that forced occupied area can make a five-dot counting argument sufficient. It excludes one owner combination and does not move the global bound.

  Novelty

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

  Records

  n = 11registerevidence 1evidence 2evidence 3source

  n = 11registerevidence 1evidence 2evidence 3source

• T-024 S5 V3 C3 Levy after Burns, Massaccesi · 2026-09-09 · n = 11

  \(s(11) \ge 3175000\sqrt{518400042893309449}\mathbin{/}598960960743657 = 3.8166095\ldots\)

  Claim and records

  Claim

  \(s(11) \ge 3175000\)$s(11)\ge 3175000$*sqrt(518400042893309449)/598960960743657 = 3.816609502788862, proved by an exact dilation-limit corollary of T-018's retained atoms re-certified on a finer direction net.
  
  The 1121 atoms of the retained 381/100 certificate, on the same D4-symmetric sites and with every weight multiplied by 200000/198931, form a certificate of the retained form at side 381/100 on the 1440-step net with shrunken side 2494953/2500000, decided from its frozen bytes by the exact event-cell sweep and by the interval branch and bound, which agree at least cell mass exactly 1.
  
  For every positive rational q with q^2 below 3240000268083184056250000000000/3228788092454681596330191602841, common scaling preserves the source hypotheses other than containment, and the exact sharpened containment lemma rules out a packing at side q times 381/100. Rational density and upward embedding exclude every real side below the supremum, which proves the displayed lower bound. The direct certificate family covers strict rational sides below the supremum; the density-and-embedding step supplies the exact >= conclusion at the supremum.

  Composition

  Derived from a full replay of the 1440-step source certificate's five conditions, scaling equivariance for Condition 1, invariance of Conditions 2 and 3, inverse-dilation preservation of Condition 5, and the sharpened containment lemma T-022 proved by an exact rational-square comparison; rational density and upward embedding supply the limit step.
  
  The source certificate is decided by two distinct machine methods, the exact event-cell sweep and the interval branch and bound on its frozen bytes. The load-bearing dilation-limit step has one exact-algebraic decision. Both are machine-replayed here, so the whole result is C3 under the derived-claim minimum rule. No review has been mapped for this result.
  
  The 720-step certificate retained beside it is the rung the standalone reader also decides; its own limit, 38100000*sqrt(129600042893309449)/3594594251080001, is registered as evidence and is weaker.

  Next rung

  V4 and C4 need two adversarial AI reviews by distinct reviewers, of the corollary and the two frozen certificates, and a human oversight record. A method-distinct decision of the corollary itself, rather than a second decision of only the source certificate, would be shown beside the rung; T-022's review covered the argument at the 181-step net and this result reuses it unchanged with new B and D.
  
  The standalone reader verify_claim.py decides the 720-step rung and refuses the 1440-step rung by its declared 1000-direction ceiling; a new reader release that lifts the ceiling would let a stranger decide the registered rung without trusting this project, and that is a change to a retained verifier rather than to the mathematics. The shrink is a 10^-7 grid crossing, not a minimum, so a smaller passing shrink off the grid would move the endpoint by less than the grid step.
  
  Two limits are measured on the frozen atoms: at the original shrink the same atoms fail every finer net at an intermediate direction, so the gain is entirely the shrink the finer net admits, and the exact ceiling family at 191/50 caps every one-body point certificate at unit side 3.8288 on any net containing its six directions.
  
  The next movement is therefore a re-optimised certificate at a finer net (H-153), which the covering LP on the frozen sites already shows to be below eleven at 720 steps, and past the cap the threshold atoms of H-152. The displayed lower bound is proved by a dilation-limit argument rather than one individual-side certificate at the algebraic value.

  Significance

  The rubric's S5 anchor is movement on a central open case, and this raises the proved lower bound for the smallest open case by about 0.0065838 beyond T-022 and by about 0.0066095 beyond the T-018 certificate side, for about 0.0277551 beyond Stromquist in total. The movement comes from the shrink that a finer net admits under Condition 4, measured on the frozen T-018 atoms; it is not a new certificate architecture, no atom was re-optimised, and the gap to Trump's packing is still about 0.0604741. The same measurement shows where this route ends: the exact depth-one ceiling family at 191/50 caps every one-body point certificate at unit side 3.8288, and these certificates sit about 0.011 below it.

  Novelty

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

  Records

  n = 11registerevidence 1evidence 2evidence 3evidence 4evidence 5source

  n = 11registerevidence 1evidence 2evidence 3evidence 4evidence 5source

• T-025 S5 V3 C3 Levy · 2026-09-09 · n = 11

  \(s(11) \ge 191/50 = 3.82\)$s(11)\ge 191/50=3.82$, by a threshold certificate

  Claim and records

  Claim

  \(s(11) \ge 191/50\)$s(11)\ge 191/50$ = 3.82, by a threshold certificate: 584 point atoms of mass 271052551/31250000 and 320 threshold atoms, every one 2-of-3, of budget 143352577/62500000, on the D4-symmetric site set at shrunken side 9977/10000 and the 181-direction net.
  
  A threshold atom (S, k, w) charges w to every admissible core holding at least k points of S and costs w floor(|S| / k) of the budget, so the family's total budget is 685457679/62500000 = 10.967322864, strictly below 11, while every event cell at every net direction carries charge at least 100000203/100000000. The counting argument then rules out eleven unit squares with pairwise disjoint interiors in a container of side 191/50.

  Composition

  One certificate, decided twice. The certificate is instantiated at its named side, 191/50; no dilation family is part of T-025.
  
  Conditions 1, 1', 2', 3 and 4 are closed-form consequences of the frozen bytes and were recomputed without sqpack in the review; Condition 5' is decided by the exact event-cell sweep of sqpack.fractional.threshold, whose dense-grid and slab evaluations agree at every direction and whose witness charge is re-evaluated by membership counting, and independently by the interval branch and bound of sqpack.fractional.threshold_interval over the doubled net, which never invokes the D4 argument.
  
  The two share the loader, the conditions and the net, and no part of how Condition 5' is decided; the gate refuses the record unless both accept and agree on the least charge exactly.
  
  The result is C3 on those two machine routes. One adversarial AI review of the theorem is retained and mapped, by an agent of this project; it found no soundness defect, and its open items -- the second route, the controls, and a stranger-facing statement in a case directory -- this registration closes. It is not a human oversight record.

  Next rung

  Push the side with the same loop: the LP that produced these atoms is run again at a larger side, and the ceiling family says the answer cannot come from point atoms alone on the stated core domain. The finer-net and dilation continuation has now been measured and registered as T-026, proving \(s(11) \ge 3.826447410572939744\)$s(11)\ge 3.826447410572939744$ by an exact dilation-limit argument. That is a separate corollary. T-025 itself proves the ordinary lower bound \(s(11) \ge 191/50\)$s(11)\ge 191/50$ at V3/C3, and its certificate is instantiated at that named side; V4 and C4 need a second adversarial AI review by a distinct reviewer and a human oversight record. The self-contained T-025 claim embeds its standard-library verifier and certificate bytes. T-025 needs no limit argument, so no dilation record belongs at this rung.

  Significance

  The rubric's S5 anchor is movement on a central open case, and this raises the proved lower bound for the smallest open case by 0.0033905 beyond T-024 and by 0.0311456 beyond Stromquist, leaving the interval [3.82, 3.877084] and a gap of 0.057084. What earns the score beyond the arithmetic is the architecture: the exact depth-one ceiling family retained at this same side proves that no D4-symmetric point-atom measure of mass below eleven exists here, so no certificate of the earlier one-body form could have reached it, and the threshold atoms carry 2.293641 of this budget that the point method cannot have. It is the first certificate of a new kind in this project, decided from frozen bytes by two routes and reviewed adversarially before registration.

  Novelty

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

  Records

  n = 11registerevidence 1evidence 2source

  n = 11registerevidence 1evidence 2source

• T-026 S5 V3 C3 Levy · 2026-09-09 · n = 11

  \(s(11) \ge 955000\sqrt{518400042893309449}\mathbin{/}179696714646249 = 3.8264474\ldots\)

  Claim and records

  Claim

  \(s(11) \ge 955000\)$s(11)\ge 955000$*sqrt(518400042893309449)/179696714646249 = 3.826447410572939, proved by an exact dilation-limit corollary of T-025's threshold certificate re-certified on a finer direction net.
  
  The 584 point atoms and 320 threshold atoms of the retained 191/50 threshold certificate, on the same D4-symmetric sites and with every weight multiplied by 500000000/498684619, form a threshold certificate of the retained form at side 191/50 on the 1440-step net with shrunken side 249507/250000, decided from its frozen bytes by the exact event-cell sweep and by the interval branch and bound, which agree at least cell charge exactly 1. The rescaled total budget is 5483661432/498684619 = 10.996251384, still strictly below eleven.
  
  For every positive rational q with q^2 below 32400002680831840562500000000/32290909254655439869209770001, common scaling of the point atoms, the threshold atoms' points, the container side and the shrunken side preserves the source hypotheses other than containment, and the exact sharpened containment lemma rules out a packing at side q times 191/50. Rational density and upward embedding exclude every real side below the supremum, which proves the displayed lower bound. The direct certificate family covers strict rational sides below the supremum; the density-and-embedding step supplies the exact >= conclusion at the supremum.

  Composition

  Derived from a full replay of the 1440-step threshold source's Conditions 1, 1', 2', 3, 4 and 5' by the threshold theorem's own exact sweep, scaling equivariance for Conditions 1 and 1', invariance of Conditions 2' and 3, inverse-dilation preservation of Condition 5', and the sharpened containment lemma T-022 proved by an exact rational-square comparison; rational density and upward embedding supply the limit step.
  
  The confirmation rests on the two machine decisions of the source certificate, which fail differently: the exact event-cell sweep of sqpack.fractional.threshold, whose dense-grid and slab evaluations must agree at every direction, and the interval branch and bound of sqpack.fractional.threshold_interval over the doubled net, which never invokes the D4 argument.
  
  One adversarial AI review is retained and mapped, of the self-contained claim, by a separate agent from the implementation authors; it covers the threshold count, exact sweep, dilation, and endpoint inference. It is not a human oversight record, so the result is C3. T-025's earlier review covers the threshold theorem and T-022's covers the dilation argument; the new review checks their composition with the T-026 values and embedded data.
  
  The 720-step certificate retained beside it crosses at the same shrink and reaches 955000*sqrt(129600042893309449)/89874194646249 = 3.825347845913112, which isolates the remaining 0.0010996 as the effect of D halving alone.

  Next rung

  The rescaled 1440-step budget is 5483661432/498684619, leaving 1869377/498684619 below eleven. The measured 720- and 1440-step certificates have the same crossing shrink and least unscaled charge. These finite measurements do not decide another net or prove that frozen-atom refinement cannot improve the limit. Re-certification on another net, re-optimization on a finer net, changed site generation, and richer charge atoms remain distinct hypotheses. The retained plateau duals with depth above one are useful separation inputs but not globally feasible obstruction witnesses.
  
  The self-contained T-026 claim embeds the standard-library threshold verifier, the 1440-step certificate, and the exact dilation record; its mapped source-distinct review is the one adversarial AI review retained. V4 and C4 need a second adversarial AI review by a distinct reviewer and a human oversight record; rung 5 would require a proof-assistant formalization reviewed by human experts.

  Significance

  The rubric's S5 anchor is movement on a central open case, and this raises the proved lower bound for the smallest open case by about 0.0064474 beyond T-025's 191/50 and by about 0.0375930 beyond Stromquist's 2 + 4/sqrt(5), leaving the interval [3.826447410572939, 3.877084] and a bound gap of about 0.0506362.
  
  The movement is the shrink a finer net admits under Condition 4, measured on the frozen T-025 atoms; no atom was re-optimised and no new theorem was needed, since Conditions 1, 1', 2' and 3 are untouched by common scaling and Condition 5' is preserved by inverse dilation of placements exactly as Condition 5 is.
  
  For this fixed certificate, the rescaled budget is 5483661432/498684619 = 10.996251384 against the eleven a certificate may not reach, leaving about 0.0037 of budget. The measured 720- and 1440-step nets share the same crossing shrink and least unscaled charge. These finite measurements leave the effect of another net, a different core side, re-optimized weights, changed sites, and richer charge atoms unresolved.

  Novelty

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

  Records

  n = 11registerevidence 1evidence 2evidence 3evidence 4evidence 5source

  n = 11registerevidence 1evidence 2evidence 3evidence 4evidence 5source

• T-031 S2 V3 C3 Levy · 2026-09-20 · n = 11

  The octagon corner class (threshold \(1/2\)$1/2$) holds no eleven-square packing at side \(96/25\)$96/25$

  Claim and records

  Claim

  At L = 96/25 and B = 9977/10000 on the 181-direction net (half-tangents k*207107/90000000, k = 0..180), the D4-symmetric point measure of total mass 10868617/1000000 = 10.868617 in cases/n11_corner_class_certificate/certificate.json, the retained exp-220 covering, charges at least 2000013/2000000 to every closed B-square at a net direction whose minimum of x + y is at least 1/2 in each of the four corner frames, decided by the exact event-cell sweep and by the interval branch and bound, which agree at that value.
  
  Consequently every packing of eleven unit squares in [0, 96/25]^2 contains a unit square whose minimum of x + y in some corner frame is strictly below 1/2, that is, one that meets the open corner triangle x + y < 1/2 at that corner; equivalently, the all-free (octagon) class of lane-a Theorem B at threshold 1/2 contains no eleven-square packing at side 96/25.
  
  This is a conditional exclusion of one corner-bin class and changes no bound on \(s(11)\)$s(11)$; the all-deep class is separately known to be outside this language's reach (BC-366), so the corner tree cannot close at 96/25 by clipping alone.

  Composition

  The certificate is a weighted fractional unavoidable-set certificate of the retained form whose row domain is the D4-symmetric convex clip of the admissible core domain by the four corner triangles at depth 1/2, admitted as a domain predicate on the row generator and threaded through both gate routes and the ceiling readers in Session 145 with a residual-7 control on the transported 88-family.
  
  The declared C3 is what the two cited atoms derive. The exact event-cell sweep and the interval branch and bound are the two internal routes of one decide_certificate --corner-clip 1/2 invocation, which refuses the file unless both accept: they share the Certificate parser and the closed-form conditions, carry a byte-identical replay string, and the exact leg records relationship_to_generator: same-implementation, so the repository counts the pair as one confirmation and not as two method-distinct derivations. The Session 146 registration review says exactly that; a genuinely separate derivation of this clipped decision would be a second machine method, and none exists.
  
  The verification rests on the two machine decisions of the frozen bytes, which fail differently: the exact event-cell sweep with the clip as extra half-planes on the per-slab centre range, and the interval branch and bound whose boxes are dropped only when provably inside the excluded set; the two decide the same set only because the clip is D4-invariant and folded, which the instrument's tests check. Conditions 1 to 4 are decided exactly before either route runs.
  
  The conclusion transfers from the shrunken cores to the unit squares without loss in the direction that matters, because the kept domain is closed and a core lies strictly inside its square by Condition 4. The retained bytes declare variant class and the clip, and the gate refuses them without the flag, so the file cannot be read as a bound.

  Next rung

  The complementary class, in which some core meets a corner triangle, is the hard one: the all-deep class is a Lemma-D theorem for every site set (the transported 88-family keeps residual 7 against a requirement of 7, BC-366), so no point covering excludes it and the corner tree cannot make 96/25 unconditional by clipping. The four mixed D4 classes (fourteen bin vectors) are a bounded follow-up under BC-367 and need a box cut on the row domain. The instrument that could matter is a 2-of-3 threshold atom on ring-centre overlaps inside the all-deep class, which needs the clip wired into the threshold routes.
  
  V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained: the Session 146 registration review is not mapped under docs/project/reviews. The case directory and the gate control test in the T-022 pattern are retained.

  Significance

  The first decided item of the corner-conditioned point language at a central open size: one D4 class of the corner tree is excluded at 3.84 by a certificate on a clipped domain, with the structural consequence that every eleven-square packing in a square of side 96/25 has a square meeting an open corner triangle of depth 1/2. It moves no bound, and the registration review shows the tree it belongs to cannot close at this side in the point language alone, since the all-deep class is a Lemma-D theorem for every site set (BC-366); the mixed classes are a bounded follow-up.

  Novelty

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

  Records

  n = 11registerevidence 1evidence 2

  n = 11registerevidence 1evidence 2

• T-033 S3 V3 C3 Levy · 2026-09-22 · n = 11

  \(s(11) \ge 955000\sqrt{2073600042893309449}\mathbin{/}359341754646249 = 3.8269975\ldots\)

  Claim and records

  Claim

  \(s(11) \ge 955000\)$s(11)\ge 955000$*sqrt(2073600042893309449)/359341754646249 = 3.826997548829543624, proved by an exact dilation-limit corollary of T-025's threshold certificate re-certified on the 2880-step direction net.
  
  The 584 point atoms and 320 threshold atoms of the retained 191/50 threshold certificate, on the same D4-symmetric sites and with every weight multiplied by 500000000/498684619, form a threshold certificate of the retained form at side 191/50 on the 2880-step net with shrunken side 249507/250000, decided from its frozen bytes by the exact event-cell sweep and by the interval branch and bound, which agree at least cell charge exactly 1. The rescaled total budget is 5483661432/498684619 = 10.996251384, still strictly below eleven.
  
  The shrink is T-026's and does not move under refinement; what this net changes is the largest half-gap tangent, 207107/1440000000 over the 2881 directions of the net, exactly half the 1440-step value, and the bound rises with it.
  
  For every positive rational q with q^2 below 129600002680831840562500000000/129126496632245014779129770001, common scaling of the point atoms, the threshold atoms' points, the container side and the shrunken side preserves the source hypotheses other than containment, and the exact sharpened containment lemma rules out a packing at side q times 191/50. Rational density and upward embedding exclude every real side below the supremum, which proves the displayed lower bound. The direct certificate family covers strict rational sides below the supremum; the density-and-embedding step supplies the exact >= conclusion at the supremum.
  
  What that conclusion does not carry is stated with it. No individual certificate is supplied at the supremum, because the sharpened containment test is equality there; no strict inequality is established there; and 191/50 remains the largest side at which the retained T-025/T-026/T-033 fixed-core family holds an individual-side certificate, which is T-025's and not this result's.

  Composition

  Derived from a full replay of the 2880-step threshold source's Conditions 1, 1', 2', 3, 4 and 5' by the threshold theorem's own exact sweep, scaling equivariance for Conditions 1 and 1', invariance of Conditions 2' and 3, inverse-dilation preservation of Condition 5', and the sharpened containment lemma T-022 proved by an exact rational comparison of squares; rational density and upward embedding supply the limit step.
  
  The source certificate's own acceptance rests on two machine decisions of one frozen file that fail differently, the exact event-cell sweep of sqpack.fractional.threshold, whose dense-grid and slab evaluations must agree at every direction, and the interval branch and bound of sqpack.fractional.threshold_interval over the doubled net, which never invokes the D4 argument.
  
  The derived bound does not inherit that. The dilation step on top of them is decided by one exact-algebraic entry and by nothing else, and epistemics.md takes a derived claim to the minimum over its inputs and the derivation itself, and the derivation is machine-replayed here like its inputs, so the rung is C3. T-022 read its own case the same way. This reconciliation applies the same rule to T-024, whose earlier declaration counted only the source certificate's two routes.
  
  A method-distinct decision of the corollary itself, an interval enclosure of the strict factor test and of c squared recorded as its own interval-certified entry, not the source's two routes, would give the derivation a second machine method. No review has been mapped, so rung 4, which needs two adversarial AI reviews by distinct reviewers and a human oversight record, is not in reach.
  
  The step is T-022's argument reused unchanged, at the same B and a halved D, whose proof note is cited here rather than rewritten. T-026's 1440-step rung is the control at the coarser net -- the same atoms, the same weights and the same crossing shrink, the two records differing in direction_steps, in their id and provenance, and in no other field -- and the refinement run reproduced its registered surd exactly, so the 0.000550138 between the two rungs is the halving of D alone.

  Next rung

  V4 and C4 need two adversarial AI reviews by distinct reviewers, of this corollary and the frozen 2880-step certificate, each a document under docs/project/reviews/ entered in docs/project/document-map.yaml with role review, and a human oversight record. A method-distinct decision of the corollary itself would be shown beside the rung. T-026's mapped review is scoped to the 1440-step claim and reviewing that one is not reviewing this one, so it is not cited here.
  
  No self-contained verifiable-claim document is rendered for this rung either: devtools.render_verifiable_claim carries one branch per retained threshold claim and its T-026 branch is bound to that rung's witness direction, surd and proof note, so a third rung needs the branch parameterised and a proof note of its own.
  
  The rescaled budget is 5483661432/498684619, leaving 1869377/498684619 below eleven, and the side this rung reaches is within about 0.000550 of 955000/249507, which is all that any further refinement of the net can buy while the shrink stands where it does. Refinement is therefore near exhausted on these atoms, and re-optimization at a finer net, changed site generation and richer charge atoms remain distinct hypotheses rather than a continuation of this one. A further assurance step would require proof-assistant formalization, external review, or an independently reproduced full decision.

  Significance

  This is a substantive controlled case result and machine audit of this project's retained threshold family. It moves T-026 from 3.826447410572939744 to 3.826997548829543624 by halving D inside T-022's sharpened containment factor sqrt(1 + D^2)/(B(1 + D)), at T-026's own crossing shrink, which does not rise under refinement; Condition 4's own coarse test B(1 + D) < 1 has the lower ceiling 152800000000000/39926861627361 = 3.826997509248, which this value exceeds. The sharpened factor is what reaches; no atom was re-optimised and no new theorem was needed, since Conditions 1, 1', 2' and 3 are untouched by common scaling and Condition 5' is preserved by inverse dilation of placements exactly as Condition 5 is.
  
  The certificate is the same measure T-026 registered: the rescaled budget is unchanged at 5483661432/498684619 = 10.996251384, still strictly below the eleven a certificate may not reach, and only the net and the half-gap tangent differ.
  
  The unchanged family cannot reach the stronger current verified bound 31/8: its refinement ceiling 955000/249507 is about 3.82755, already below 3.875. The result therefore records controlled method and calibration evidence, rather than a current public-bound advance. Changed weights, sites, parent domains, and richer charge atoms remain unresolved.

  Novelty

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

  Records

  n = 11registerevidence 1evidence 2evidence 3evidence 4evidence 5source

  n = 11registerevidence 1evidence 2evidence 3evidence 4evidence 5source

• T-035 S3 V3 C3 Levy · 2026-09-24 · n = 11

  Six-plus-five packings near Trump's tilt with side \(\le U_{hi}\)$\le U_{hi}$ lie within rho of his pose

  Claim and records

  Claim

  Every packing of eleven unit squares in a square container, six at orientation 0 and five sharing one orientation modulo pi/2 with half-tangent in [91442076901/250000000000, 73154061521/200000000000] (an interval containing [t* - 10^-6, t* + 10^-6] for Trump's exact half-tangent t* = 0.365769307604677...), whose side is at most the rational U_hi of the certificate header (U_hi - U = 2.03e-45), lies, after the quarter turn that puts its tilted centroid in the closed upper-right quadrant and the relabelling that orders each class by x + y/4, strictly within rho = 808514697/200000000000 of Trump's labelled image (rotation 1, labels [3,4,2,5,0,1,8,10,6,9,7]) in every centre coordinate, with every tilted orientation within 2.0e-6 radians of Trump's; every other packing in the family has side greater than U_hi.
  
  The statement is a machine-verified reduction, not optimality: a closed exact cell tree of 139,441,005 records, replayed in full by an independent reader, puts every small packing in the family near Trump's pose. It does not invoke the BC-240 local theorem. T-036 composes it with that theorem's first clause.

  Composition

  Not compound. One certificate tree and one reader verdict carry the whole statement, with no local theorem, monotonicity or composition step between them. The reader closes a Trump-degenerate leaf by exact arithmetic, bounding every centre coordinate of the cell's packings within rho of the labelled image, which is why the statement stops at the rho-ball rather than at Trump's pose. The entry is C3 (repository-origin, exact-algebraic, a certificate, a replay and a passing status). One adversarial AI review is retained, the mapped 2026-09-24 closed-tree review: a Fable max W2 review by a different agent than the lanes that produced the tree, inside the same project. It is not an external review and not a human oversight record.

  Next rung

  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 cell-tree contract and its reader, reviewed by human experts. Three steps would strengthen the record without moving a rung. The certificate could be retained where a gate can reach it; until then the manifest is the record's only hold on it. The reader could compare the declared box with t* +- 10^-6 itself, a comparison only the review has made. A reader that accepts a non-root cell would make the \(n = 11\)$n=11$ negative control reader-checked. The mathematics beyond this result is rung 1 of the ladder, H-112, which H-242's pilot (BC-383) prices: a per-node bound that closes this box in far fewer than 1.7e8 nodes comes before more boxes.

  Significance

  A substantive case result and machine audit at the smallest open case: one certificate tree, closed with no unresolved leaf, reduces a whole restricted family to a neighbourhood of Trump's pose. It moves no bound on \(s(11)\)$s(11)$, its family is one box of half-tangents 2e-6 wide, and its cost, about 1.7e8 nodes for that one box, argues against S4's reusable technique. The 2026-09-24 closed-tree review scored the composed theorem S3 on the same grounds.

  Novelty

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

  Records

  n = 11registerevidence 1

  n = 11registerevidence 1

• T-036 S3 V3 C2 Levy · 2026-09-24 · n = 11

  Trump's pose is optimal among six-plus-five packings near its tilt, unique up to symmetry

  Claim and records

  Claim

  Every packing of eleven unit squares in a square container, six at orientation 0 and five sharing one orientation modulo pi/2 with half-tangent in [91442076901/250000000000, 73154061521/200000000000] (an interval containing [t* - 10^-6, t* + 10^-6] for Trump's exact half-tangent t*), has container side at least U = 3.877083590022814..., the exact side of Trump's packing, and a packing in the family has side exactly U only if it is a quarter-turn image of Trump's pose with the squares relabelled within the two classes.
  
  Reflections leave the family, since they send the tilt theta* to pi/2 - theta*, whose half-tangent 0.464 is outside the box, so that Z/4 x S6 x S5 orbit is the whole equality set. The statement is T-035's reduction composed with the first clause of the BC-240 local theorem at Trump's pose. It says nothing about any other tilt, about packings whose orientation classes are not six plus five, or about \(s(11)\)$s(11)$.

  Composition

  Compound, and the minimum is set by BC-240's first clause. The reduction, T-035 on E-n011-h236-rung0-reduction, is V3/C3. The first clause, on E-n011-trump-local-theorem-first-clause, is an audited proof whose steps are prose and whose radius computation alone is machine-checked, so method proof-audited with a proof block supports V3 and nothing higher, which fixes the composed theorem at V3. The checker derives C3 from the reduction's entry; this note is why the declared confirmation is C2.
  
  The composing step is the one the closed-tree review derived again: undoing the quarter turn carries a Trump-degenerate leaf's packing at side s' <= U to a translate by (0, U - s') inside [0,U]^2, a sup-norm isometry on centre differences, so the first clause forces Trump's labelled pose and the four wall contacts force s' = U. The angle window, 2.0e-6 radians, is below rho_row.
  
  Confirmation is C2 by the C table: the clause's replay command, the source-distinct BC-241 checker, passes at this head, and a proof-audited entry does not derive above C2.
  
  2026-10-02: the radius generator gained a replay mode, so rho_row = 808514697/200000000000 now carries an exact-algebraic entry of its own, E-n011-trump-isolation-radius (replayed-here, same-implementation, passed), and C3 for the radius is derived. It does not set the composed theorem's minimum, because the closed-tree review's question, whether BC-240's audited prose steps are load-bearing for confirmation, is answered yes.
  
  The replay and the BC-241 checker confirm the quantities the proof consumes (the moduli, the curvature constants, the stresses, the caps and their aggregate arithmetic) and not the steps that use them. Those steps are prose, and the first clause rests on each: that the second-order remainder of every active function is at most K/2 times the squared norm, so that the modulus forces the norm to be at least 2 kappa/K; that every packing in the ball selects one of the 128 branches, which needs the inactive-feature gap cap, itself a single-source computation; and the composing step through the quarter turn.
  
  A mutation or a perturbed radius is refused by the replay, but a wrong prose step would not be. So C2 stands until those steps are mechanised or reviewed again by a distinct reviewer with the oversight record the ladder asks for.

  Next rung

  The replay mode the closed-tree review asked for exists, and the radius has its own exact-algebraic entry, but the composition note judges BC-240's audited prose steps load-bearing, so C3 needs those steps mechanised or reviewed again by a distinct reviewer, not more replay of the radius. V4 would need BC-240's closing steps mechanised rather than only the quantities they consume, and with C4 a second adversarial AI review by a distinct reviewer and a human oversight record. Retaining the per-face dual witnesses and recomputing the gap cap from distinct source are the closure review's two bounded residual tasks.

  Significance

  A substantive case result and machine audit: the first optimality statement with an equality case for a family containing Trump's packing. Stromquist 2003's bound for squares at 0 and 45 degrees is an earlier restricted-orientation statement, and it is not attained and its family does not contain Trump's packing. It moves no bound on \(s(11)\)$s(11)$, and its cost, about 1.7e8 nodes for one box, argues against S4's reusable technique.

  Novelty

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

  Records

  n = 11registerevidence 1evidence 2evidence 3

  n = 11registerevidence 1evidence 2evidence 3

• T-037 S5 V3 C3 Kleddamag after Levy, Guzhou0806, Mira · 2026-09-29 · n = 11

  \(s(11) > 31/8 = 3.875\)$s(11)>31/8=3.875$

  Claim and records

  Claim

  \(s(11) > 31/8\)$s(11)>31/8$ = 3.875, by Kleddamag's 11-squares-certified-bound v1.0.2 release of 22 September 2026. It raised the case's verified lower bound by 0.048002 over T-033 and leaves 0.0020836 to Trump's 3.8770835900.
  
  The certificate is an exact nonnegative D4-invariant system of point and k-of-m threshold charges over 12,028 contiguous parent-angle intervals, each with a closed core strictly inside every parent of the interval, parents of side 764/775 in a container of side 191/50. Eleven disjoint cores would carry at least 11 x 999962528 against a budget of 10999479944, which they exceed by 107864 integer units, and compactness makes the bound strict.
  
  It was replayed here in full by the source's two exact event-cell sweeps, in Python and JavaScript, and decided a second time by this repository's native parent-core interval branch and bound (devtools.verify_kleddamag_n11_native), which accepted all 12,028 rows with no stalled box.
  
  Kleddamag, 11-squares-certified-bound, building on Squares Project (Joshua Levy): the release's ATTRIBUTION.md says the work builds on this project and that global-certificate.json was developed from T-026's certificate.

  Composition

  Primary at \(n = 11\)$n=11$: one certificate and the bound L/A, with no monotonicity step. Two evidence entries whose methods differ both passed on the retained certificate, which is C3 with the two methods shown beside the rung: the source's exact event-cell sweeps (exact-algebraic, replayed here; the Python and JavaScript scanners are one method) and this repository's directed-rounding interval coverage of every row (interval-certified). Both rest on the source's certificate and on the same counting and transfer theorem, which the two 2026-09-22 reviews read.

  Next rung

  V4 and C4 need two adversarial AI reviews by distinct reviewers of the complete claim and a human oversight record. The two 2026-09-22 reviews are mapped and each reads one route; neither is recorded in this entry's reviews, and whether a same-project review of another author's certificate qualifies is the owner's decision rather than missing work. Rung 5 needs a proof-assistant formalization of the transfer theorem and the counting argument, reviewed by human experts. Superseded on 2026-09-29 by Wang and Li's \(s(11) > 3875000000/999999999\)$s(11)>3875000000/999999999$ (T-061), which is this certificate reweighted and scaled, 3.9e-9 higher, and by T-060's exact \(s(11)\)$s(11)$ = T; stays true as stated.

  Significance

  Scored at S5 by the rubric's anchor, movement on a central open case. \(n = 11\)$n=11$ is a central open case of this project, and T-019 gave not being one as its first reason for staying below S5. The bound closes about 96 per cent of the gap the register held, from 0.0501 to 0.0021 below Trump's packing, and it is this project's T-026 certificate adopted and carried further outside it. The mathematics is Kleddamag's; this repository's part is the replay and the method-distinct second decision.

  Novelty

  previously-published Present in an identified source

  Records

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

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

• T-047 S4 V3 C3 Tokoharu after Levy, wand125, Stromquist, Nagamochi, Burns, Massaccesi · 2026-09-29 · 7 cases

  \(s(11) \ge 381/100\)$s(11)\ge 381/100$; \(s(n) \ge 1377/250\)$s(n)\ge 1377/250$ for \(n = 26\ldots28\)$n=26\dots 28$; \(s(n) \ge 571/100\)$s(n)\ge 571/100$ for \(n = 29\ldots31\)$n=29\dots 31$

• 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-059 S2 V3 C3 wand125 after Tokoharu, Daniel · 2026-09-29 · n = 11

  Reported equality of 12028 n11 row minima reproduced by a complete bound replay

  Claim and records

  Claim

  wand125/square-packing-tools reports that its exact general_pose_tree checker reproduces all 12028 per-row core minima of Kleddamag's n11 certificate, release v1.0.2, with global row minimum 999962528 units and all witnesses replayed. This is the source's row-scan equality claim only, not a new proof of the global counting theorem or independent rectangle-density coverage.
  
  wand125, square-packing-tools, 29 September 2026, building on Tokoharu's rectangle method, solver and verifier and on Evan Daniel's point verifier. The source discloses Codex and Claude assistance.

  Next rung

  V4 and C4 need a second, independent row-minimum method (the checker and the claim share one implementation, so no method diversity is claimed) and the review record the ladder requires. A separate branch-and-bound over the 12,028 rows is the natural second method; the existing native parent-core branch and bound already decides the same rows for the counting premise (T-037).

  Significance

  A reusable independent row-checking implementation worth replaying; the existing n11 bound does not change.

  Novelty

  previously-published Present in an identified source

  Records

  n = 11registerevidence 1evidence 2

  n = 11registerevidence 1evidence 2

• T-060 S5 V3 C3 Queuingtheorydotcom after Levy, Kleddamag · 2026-09-29 · n = 11

  Trump's eleven-square packing is globally optimal

  Claim and records

  Claim

  \(s(11) = T = (6u+4)/(1+2u-u^2) = 3.8770835900228141773078970601\ldots\)$s(11)=T=(6u+4)/(1+2u-u^2)=3.8770835900228141773078970601\dots$, where \(u\)$u$ is the unique root in \((9/25, 37/100)\)$(9/25,37/100)$ of \(5u^8-10u^7-2u^6+14u^5+12u^4-6u^3+2u^2+2u-1 = 0\)$5u^8-10u^7-2u^6+14u^5+12u^4-6u^3+2u^2+2u-1=0$. Independent rotations and boundary contact are allowed.
  
  The proof, published by Queuingtheorydotcom on 29 September 2026, is confirmed here by a re-implementation sharing components with the source -- complete repository geometric executions on kernels the source also bundles -- and a mapped mathematical audit.
  
  Queuingtheorydotcom, 11SquaresOptimal, Astra-assisted work building on Squares Project and Kleddamag. The matching construction is Trump's.

  Composition

  The complete 2184-pattern cover and 2180 exclusions leave four symmetric survivors. The D4 bridge reduces these to case 438; the 14-round root induction and complete 10-node capture graph eliminate all far branches and force the near state into the reviewed local region. Exact local isolation and the endpoint embedding argument exclude every side below \(T\)$T$. The exact Trump witness attains \(T\)$T$. All premises have completed exact executions, which is V3/C3. One adversarial AI review is retained and mapped, by GPT-6 Astra at max reasoning; it is not a human oversight record. No second machine method is claimed.
  
  The Lean 4 formalization in 11SquaresFormalized states the whole claim as one theorem, ElevenSquare.optimality, which the 6 October statement audit reads as this claim with the same exact \(T\)$T$. Its source reports that its full verification run, resumed from earlier validated receipts, passed with an axiom audit that trusts Lean's compiler for 13,308 native_decide axioms. That run is private and recorded as reported, so it sets no rung; the build here covers the statement closure and the upper half only.

  Next rung

  V5 needs two records the register lacks. One is a complete build of the 11SquaresFormalized proof that the record can rest on, with its axiom receipt: run here from the retained pin at its toolchain, or a third party's build retained here. The source's own run is private and is recorded as reported (E-n011-lean-formalization-report). The other is a retained formalization review by a named human expert who is not its author and states competence in Lean and in the mathematics, checking statement fidelity, the definitions, the axioms (the 13,308 native_decide axioms the theorem trusts to Lean's compiler among them) and that build.
  
  V4 and C4 need the owner's oversight record and a second adversarial AI review by a reviewer distinct from Astra. C5 needs that build made here at the pinned toolchain, an open_review pointer and two such expert reviews. Engineering follow-up think-e2ot will orchestrate fresh whole-ensemble replay through reviewed state-equivalence bindings. Simplification was to precede the n11 explainer, tracked separately, which is now the eleven-square optimality paper.

  Significance

  Resolves global optimality for \(n = 11\)$n=11$, a central case, by closing the gap to Trump's exact construction, beyond the previous strict T-037 lower bound.

  Novelty

  previously-published Present in an identified source

  Records

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

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

• T-061 S2 V3 C3 Wang, Li after Kleddamag, Levy · 2026-09-30 · n = 11

  \(s(11) > 3875000000/999999999 = 3.875000003875\ldots\)$s(11)>3875000000/999999999=3.875000003875\dots$, 3.9e-9 above \(31/8\)$31/8$

  Claim and records

  Claim

  \(s(11) > 3875000000/999999999\)$s(11)>3875000000/999999999$ = 3.875000003875000003875..., by Ke Wang and Can Li's Zenodo record of 29 September 2026, reported on jlevy/squares#247. The step over 31/8 is exactly 31/7999999992, about 3.9e-9.
  
  The certificate is Kleddamag's v1.0.2 global-certificate.json (T-037) with thirteen threshold-charge orbits raised, which puts the minimum core charge at 1000047559 on every one of the 12,028 parent-angle intervals, and with the parent and every core side scaled by 999999999/1000000000, so that the container over the parent is (31/8) times 1000000000/999999999. Eleven disjoint cores exceed the budget 11000095024 by 428125 integer units.
  
  One more step of the scale factor, 1 - 2*10^-9, already fails at row 615, so these data admit at most about twice the step. Scaling Kleddamag's certificate alone already passes a full sweep, so the reweighting enlarges the surplus but is not needed for the bound.
  
  It was replayed here in full by the authors' two verifiers and by Kleddamag's own Python and JavaScript event-cell sweeps, and decided a second time by this repository's native parent-core interval branch and bound, which accepted all 12,028 rows with no stalled box.
  
  Ke Wang and Can Li, Zenodo record 23038546, building on Kleddamag and this project. The record makes no statement about AI assistance.

  Composition

  Primary at \(n = 11\)$n=11$: one certificate and the bound L/A', with no monotonicity step. Two evidence entries whose methods differ both passed on the retained certificate, which is C3 with the two methods shown beside the rung: the event-cell sweeps (exact-algebraic: the authors' primary, Kleddamag's Python and JavaScript, and the authors' re-implementation are one method) and this repository's directed-rounding interval coverage of every row (interval-certified). Both rest on the certificate and on T-037's counting and transfer theorem, whose hypotheses were re-checked at the scaled sides.

  Next rung

  V4 and C4 need two adversarial AI reviews by distinct reviewers of the complete claim and a human oversight record; the 2026-09-30 review is a same-project read and is not recorded in this entry's reviews. Rung 5 needs a proof-assistant formalization of the transfer theorem and the counting argument, reviewed by human experts. The reweighting is not needed for the bound: Kleddamag's own weights at the scaled sides pass Kleddamag's full event-cell sweep with the same minimum 999962528 and surplus 107864 (the packet's scale-only receipt), so the scaling alone carries the step and the thirteen raised orbits only enlarge the surplus to 428125.

  Significance

  It strictly raises the verified lower bound at a central case, which the S5 anchor names, but by 31/7999999992, about 3.9e-9, spending the slack of T-037's certificate after a reweighting; the release itself calls it a proof-of-slack result, and these data admit at most about twice the step. The case's gap to Trump's packing, 0.0020836, does not change at any printed digit, so it is scored as a citable detail rather than movement; T-042 is the precedent for scoring a true, fully replayed step by what it changes.

  Novelty

  previously-published Present in an identified source

  Records

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

  n = 11registerevidence 1evidence 2evidence 3source 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-112 S3 V3 C2 Levy after Queuingtheorydotcom · 2026-10-06 · n = 11

  Trump's packing is the only optimal packing of eleven squares, up to symmetry

  Claim and records

  Claim

  Every packing of eleven unit squares in a square of side T = 3.8770835900228141773…, the least side T-060 proves possible, is Walter Trump's 1979 packing after one of the eight symmetries of the container and a relabelling of the squares. Independent rotations and boundary contact are allowed. A quarter-turn reparametrization of one square is the same physical square and does not count as another packing. No symmetry of the container maps Trump's packing to itself, so there are exactly eight optimal packings as unlabelled configurations, the images of one another.
  
  This is a direct corollary of T-060 and adds no computation. T-060's proof embeds any packing of side S <= T concentrically in the rational cap U > T, where its 2,180 exclusions, the D4 reduction to case 438, the closed capture partition and pose inclusion all apply, and maps it rigidly into the fixed side-T frame, where the local isolation lemma forces the exact construction. For S < T the construction's span T is a contradiction, which is T-060. For S = T nothing is contradicted: the packing is the construction after the alignment, a D4 element composed with the case-438 quarter turn, which is this result.
  
  It is T-036's equality clause without T-036's restriction to six squares at angle 0 and five near Trump's tilt, and with reflections, which leave that family.

  Composition

  One entry, E-n011-optimum-uniqueness, proof-audited, which cites the completed exact executions of E-n011-global-optimality-independent unchanged and adds one prose step, that every premise of T-060's endpoint is stated for side S <= T and at S = T yields the construction rather than a contradiction. Proof-audited with a proof block supports V3. The step is prose and not mechanised, so the declared confirmation is C2, as for T-036's composing step, though every quantity it consumes is T-060's and re-implemented sharing named components.
  
  T-060's evidence, E-n011-global-optimality-independent, is a premise of the entry and is not cited here beside it: it claims the exact value, which would give this result a bound's standing that it does not have.

  Next rung

  C3 needs the step at S = T mechanised, or reviewed again by a distinct reviewer with the oversight record the ladder asks for. The Lean theorem ElevenSquare.optimality in 11SquaresFormalized, whose statement the project's audit of 6 October reads as \(s(11)\)$s(11)$ = T, states the lower bound and the construction and no equality case; a Lean statement of the equality case would be the route to rung 5, once a formalization is reviewed here. Rung 4 needs what T-060's rung 4 needs: the owner's oversight record and a second adversarial review of the global chain.

  Significance

  A substantive case result: it completes the classification at eleven squares, the optimum being a single rigid packing up to symmetry, with no sliding family and no second contact type at T, in the case T-060 settled. It moves no bound and adds no method, since it is T-060's argument read at equality, which is what an S4 would need; it is one step above T-036's restricted equality case.

  Novelty

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

  Records

  n = 11registerevidence 1

  n = 11registerevidence 1

In the frontier survey On GitHub