T-017: $s (12) \geq 99 / 25 = 3.96$

V3 C3 lower bound confirmed superseded by T-095

2026-09-04 established · Levy after Burns, Massaccesi · $n = 12$

$s (12) \geq 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$ in the retained corpus: the case previously held 2 + 4/sqrt(5) = 3.788854..., which is Stromquist's $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 (11)$ strictly, by at least 0.082916. Monotonicity gives only $s (12)$ >= $s (11)$ ; the strict inequality did not follow from anything on record before, because $n = 12$ 's previous lower bound was $s (11)$ 's own 3.788854 and sat below Trump's packing.

Significance, composition and next rung

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$ 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$ rather than inherited from $n = 11$ : the frontier case body had recorded that nothing specific to $n = 12$ had been proved there.

Held below S5 because $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.
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$ 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) \leq 4$ , the ceiling sits strictly below 4, and 4 is the conjectured value -- so no single certificate of this shape certifies $s (12) \geq 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.
Novelty: apparently-novel Not found in the recorded search, subject to its stated gaps

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 this result
$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
$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-017 in the results table

On GitHub, at main

Register: T-017 in results.yaml, line 895
Evidence: E-n012-fractional-certificate · E-fractional-interval-decision
Proofs and certificates: certificate certificate.json · certificate certificate.json
Sources: Burns–Massaccesi n17
Artifacts: 11 artifacts and controls
cases/n12_fractional_certificate/certificate.json cases/n12_fractional_certificate/certificate-79-20.json cases/n12_fractional_certificate/certificate-197-50.json cases/n12_fractional_certificate/certificate-19-5.json cases/n12_fractional_certificate/certificate-77-20.json cases/n12_fractional_certificate/certificate-97-25.json cases/n12_fractional_certificate/certificate-39-10.json cases/n12_fractional_certificate/certificate-393-100.json src/sqpack/fractional/certificate.py src/sqpack/fractional/generate.py tests/test_fractional_certificate.py
Case file: frontier/n-012.md (verified lower, verified upper, reported lower, reported upper)

T-017: s(12)≥99/25=3.96s(12)≥99/25=3.96

The case

Results on the case

Links

T-017: $s (12) \geq 99 / 25 = 3.96$