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

V3 C3 lower bound confirmed

2026-10-05 published · squarepacker after Daniel, Levy · $n = 12$

$s (12) \geq 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$ 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$ . squarepacker's own indep_check.cpp, replayed here at $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).

Significance, composition and next rung

Significance: Raises the verified lower bound at $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.
Composition: Primary at $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, reproduced with the producer's code, 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$ , 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$ .
Novelty: previously-published Present in an identified source

The case

Case record

3.974

345

3.4644.464

\sqrt{n}

\sqrt{n} + 1

Proven

$3.97150$ $\leq s (12) \leq$ $4$

exact

Citation record n-012

lowersquarepacker after Daniel, Levy 2026, GitHub (confirmed T-095)

Open

optimality

The case record

LowerUpper

Verified

\frac{7943}{2000}

Reported

\frac{7943}{2000}

Gap

\frac{57}{2000}

= 0.0285

Results on the case

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

2005 published T-007
$s (n) \geq min (⌈ \sqrt{n} ⌉, \sqrt{n - 2 ⌊ \sqrt{n} ⌋ + 1} + 1)$ for $4 \leq n \leq 324$
V0 C1 lower bound incomplete on this case, superseded by T-095
Nagamochi · Nagamochi 2005 · source · register
2026-08-25 published T-049
$s (12) \geq 15680 / 3951 = 3.9686155 \dots$
V3 C3 lower bound confirmed superseded by T-095
Daniel after Burns, Massaccesi · evand square-packing 2026 · packet · source 1 · source 2 · review 1 · review 2 · register
2026-09-04 established T-017
$s (12) \geq 99 / 25 = 3.96$
V3 C3 lower bound confirmed superseded by T-095
Levy after Burns, Massaccesi · register
2026-09-04 published T-085
Nagamochi 2005, Lemma 1 is false for every container with $a > 3$ and $b > 2$
V3 C3 correction confirmed
Karakuş; chelokot · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register
2026-09-29 published T-058
Rectangle-certificate ceiling α·UB(n) proved for $n = 1$ ..100; B·UB(n) on 64 grid rows
V3 C3 method limit confirmed
wand125 after Tokoharu, Daniel · wand125 tools 2026 · packet · register
2026-09-29 published T-083
$s (n) \geq 1 / 2 + \sqrt{n - ⌊ \sqrt{n} ⌋ + 1 / 4}$ for every nonsquare $8 \leq n \leq 324$
V3 C3 lower bound confirmed on this case, superseded by T-095
Karakuş · Karakuş 2026 · source · register
2026-10-02 published T-078
$s (12) \geq 31360 / 7901 = 3.9691178 \dots$ , Daniel's certificate rescaled by $7902 / 7901$
V3 C3 lower bound confirmed superseded by T-095
squarepacker after Daniel · squarepacker s12 2026 · packet · packet · source 1 · source 2 · review 1 · review 2 · register
2026-10-02 established T-079
$s (12) \geq 15680000 / 3949423 = 3.9702002 \dots$ , Daniel's points re-weighted
V3 C3 lower bound confirmed superseded by T-095
Levy after Daniel · source 1 · source 2 · review · register
2026-10-05 published T-095 this result
$s (12) \geq 7943 / 2000 = 3.9715$ , Daniel's points dilated and re-weighted
V3 C3 lower bound confirmed
squarepacker after Daniel, Levy · squarepacker s12 2026-10-05 · packet · packet · source 1 · source 2 · review 1 · review 2 · register
2026-10-07 published T-124
Reported non-strict local minima for 178 source configurations
V0 C0 restricted optimality recorded
Daniel after Couzo · Daniel exact and local reports 2026 · packet · register

Links

On this site: Case record, $n = 12$ · Frontier row, $n = 12$ · T-095 in the results table

On GitHub, at main

Register: T-095 in results.yaml, line 9397
Evidence: E-n012-squarepacker-7943-2000-report · E-n012-squarepacker-7943-2000-source-replay · E-n012-squarepacker-7943-2000-native-parent-core · E-n012-squarepacker-7943-2000-audit
Proofs and certificates: certificate s12_lower_3.9715.txt.gz · proof s12_lower_3.9715.tex · audit review-2026-10-05-s12-v11-certificate.md · proof parent_core.py · audit review-2026-09-22-native-n11-parent-core.md
Sources: squarepacker s12 2026-10-05 (its own site, retained copy)
Source packet: resources/web/squarepacker-s12-lower-bound-2026-10-05/README.md · resources/web/evand-square-packing-2026-09-26/README.md
Artifacts: 19 artifacts and controls
resources/web/squarepacker-s12-lower-bound-2026-10-05/README.md resources/web/squarepacker-s12-lower-bound-2026-10-05/s12-lower-bound/s12_lower_3.9715.txt.gz resources/web/squarepacker-s12-lower-bound-2026-10-05/s12-lower-bound/README.md resources/web/squarepacker-s12-lower-bound-2026-10-05/s12-lower-bound/paper/s12_lower_3.9715.pdf resources/web/squarepacker-s12-lower-bound-2026-10-05/receipts/preflight.json resources/web/squarepacker-s12-lower-bound-2026-10-05/receipts/daniel-verify-ovf-N96000.log resources/web/squarepacker-s12-lower-bound-2026-10-05/receipts/indep-check-N96000.log resources/web/squarepacker-s12-lower-bound-2026-10-05/receipts/native-parent-core-N96000.json resources/web/evand-square-packing-2026-09-26/square-packing/s12/certificates/s12_lower_3.9686.txt.gz devtools/audit_s12_v11_certificate.py devtools/verify_evand_angle_net_native.py docs/project/reviews/review-2026-10-05-s12-v11-certificate.md tests/test_s12_v11_certificate.py resources/web/squarepacker-s12-lower-bound-2026-10-05/receipts/controls/native-lowered-orbit.json resources/web/squarepacker-s12-lower-bound-2026-10-05/receipts/controls/native-regrid-3999600.json resources/web/squarepacker-s12-lower-bound-2026-10-05/receipts/controls/indep-check-N96000-lowered-orbit.log resources/web/squarepacker-s12-lower-bound-2026-10-05/receipts/controls/indep-check-N96000-regrid-3999600.log resources/web/squarepacker-s12-lower-bound-2026-10-05/receipts/controls/daniel-verify-N96000-lowered-orbit-bin-0.log resources/web/squarepacker-s12-lower-bound-2026-10-05/receipts/controls/daniel-verify-N96000-regrid-3999600-bin-0.log
Case file: frontier/n-012.md (verified lower, verified upper, reported lower, reported upper)

T-095: s(12)≥7943/2000=3.9715s(12)≥7943/2000=3.9715, Daniel's points dilated and re-weighted

The case

Results on the case

Links

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