T-112: Trump's packing is the only optimal packing of eleven squares, up to symmetry

V3 C2 uniqueness confirmed

2026-10-06 established · Levy after Ahmed · $n = 11$

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.

Significance, composition and next rung

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.
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)$ = 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.
Unfinished confirmations: C3: the step at S = T mechanised, or reviewed again by a distinct reviewer with the oversight record the ladder asks for. Not priced.
Novelty: apparently-novel Not found in the recorded search, subject to its stated gaps

The case

Case record

3.877

345

3.3174.317

\sqrt{n}

\sqrt{n} + 1

Proven

$s (11) =$ $3.877084$

optimal
exact
rigid

Citation record n-011

lowerAhmed after Levy, Kleddamag 2026, GitHub (confirmed T-060)

upperTrump 1979, Squares in Squares (confirmed T-011)

The case record

LowerUpper

Verified3.87708359…3.87708359…

Reported3.87708359…3.87708359…

Gap0 solved: the verified bounds meet

Results on the case

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

1979 published T-011
Trump's 1979 packing is exactly valid, so $s (11) \leq 3.877083590022814 \dots$
V3 C3 upper bound confirmed
Trump · Trump 2023 · register
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-060
Nagamochi · Nagamochi 2005 · source · register
2026-08-24 established T-010
$s (11) \geq 2 + 4 / \sqrt{5}$ , by a repair of Stromquist 2003's Figure 14 point set
V3 C3 lower bound confirmed superseded by T-060
Levy after Stromquist · register
2026-09-04 established T-018
$s (11) \geq 381 / 100 = 3.81$
V3 C3 lower bound confirmed superseded by T-060
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-06 established T-022
$s (11) \geq 38100 \sqrt{8100042893309449} / 899996306539 = 3.8100257 \dots$
V3 C3 lower bound confirmed superseded by T-060
Levy after Burns, Massaccesi · source · register
2026-09-08 established T-023
Conditional exclusion: no eleven-square packing in the four-owner branch at $q = 96 / 25$
V3 C3 case exclusion confirmed superseded in part by T-060
Levy · source · register
2026-09-09 established T-024
$s (11) \geq 3175000 \sqrt{518400042893309449} / 598960960743657 = 3.8166095 \dots$
V3 C3 lower bound confirmed superseded by T-060
Levy after Burns, Massaccesi · source · register
2026-09-09 established T-025
$s (11) \geq 191 / 50 = 3.82$ , by a threshold certificate
V3 C3 lower bound confirmed superseded by T-060
Levy · source · register
2026-09-09 established T-026
$s (11) \geq 955000 \sqrt{518400042893309449} / 179696714646249 = 3.8264474 \dots$
V3 C3 lower bound confirmed superseded by T-060
Levy · source · register
2026-09-20 established T-031
The octagon corner class (threshold $1 / 2$ ) holds no eleven-square packing at side $96 / 25$
V3 C3 case exclusion confirmed superseded by T-060
Levy · register
2026-09-22 established T-033
$s (11) \geq 955000 \sqrt{2073600042893309449} / 359341754646249 = 3.8269975 \dots$
V3 C3 lower bound confirmed superseded by T-060
Levy · source · register
2026-09-22 published T-037
$s (11) > 31 / 8 = 3.875$
V3 C3 lower bound confirmed superseded by T-060
Kleddamag after Levy, Guzhou0806, Mira · Kleddamag n11 2026 · packet · source 1 · source 2 · review 1 · review 2 · register
2026-09-22 published T-047
$s (11) \geq 381 / 100$ ; $s (n) \geq 1377 / 250$ for $n = 26 \dots 28$ ; $s (n) \geq 571 / 100$ for $n = 29 \dots 31$
V3 C3 lower bound confirmed superseded by T-060
Tokoharu after Levy, wand125, Stromquist, Nagamochi, Burns, Massaccesi · Tokoharu density 2026 · packet · source · review · register
2026-09-24 established T-035
Six-plus-five packings near Trump's tilt with side $\leq U_{h i}$ lie within rho of his pose
V3 C3 case exclusion confirmed
Levy · register
2026-09-24 established T-036
Trump's pose is optimal among six-plus-five packings near its tilt, unique up to symmetry
V3 C2 restricted optimality confirmed superseded in part by T-060 and T-112
Levy · 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-059
Reported equality of 12028 n11 row minima reproduced by a complete bound replay
V3 C3 audit confirmed
wand125 after Tokoharu, Daniel · wand125 tools 2026 · packet · register
2026-09-29 published T-060
Trump's eleven-square packing is globally optimal
V3 C3 optimality confirmed
Ahmed after Levy, Kleddamag · Ahmed n11 optimality 2026 · packet · packet · source 1 · source 2 · review 1 · review 2 · register
2026-09-29 published T-061
$s (11) > 3875000000 / 999999999 = 3.875000003875 \dots$ , 3.9e-9 above $31 / 8$
V3 C3 lower bound confirmed superseded by T-060
Wang, Li after Kleddamag, Levy · Wang Li n11 2026 · packet · source 1 · source 2 · review · 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-060
Karakuş · Karakuş 2026 · source · register
2026-10-06 established T-112 this result
Trump's packing is the only optimal packing of eleven squares, up to symmetry
V3 C2 uniqueness confirmed
Levy after Ahmed · packet · 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 = 11$ · Frontier row, $n = 11$ · T-112 in the results table · The $n = 11$ optimality paper · The $n = 11$ explainer

On GitHub, at main

Register: T-112 in results.yaml, line 11640
Evidence: E-n011-optimum-uniqueness
Proofs and certificates: certificate final-composition.json
Sources: Ahmed n11 optimality 2026 (its own site, retained copy)
Source packet: resources/web/n11-optimality-2026-09-29/README.md
Artifacts: 9 artifacts and controls
resources/web/n11-optimality-2026-09-29/source/PROOF.md resources/web/n11-optimality-2026-09-29/receipts/final-composition.json devtools/templates/n11-optimality-review-article.md docs/project/reviews/review-2026-10-03-n11-optimality-adversarial-gpt6-pro-unified.md docs/project/reviews/review-2026-10-03-n11-optimality-upstream-delta.md docs/project/reviews/review-2026-10-06-n11-uniqueness-adversarial.md docs/project/reviews/review-2026-10-06-n11-uniqueness-fix-check.md tests/test_n11_composition_joins.py tests/test_trump11_symmetry.py
Case file: frontier/n-011.md (verified lower, verified upper, reported lower, reported upper)