T-060: Trump's eleven-square packing is globally optimal

V3 C3 optimality confirmed

2026-09-29 published · Ahmed after Levy, Kleddamag · $n = 11$

$s (11) = T = (6 u + 4) / (1 + 2 u - u^{2}) = 3.8770835900228141773078970601 \dots$ , where $u$ is the unique root in $(9 / 25, 37 / 100)$ of $5 u^{8} - 10 u^{7} - 2 u^{6} + 14 u^{5} + 12 u^{4} - 6 u^{3} + 2 u^{2} + 2 u - 1 = 0$ . Independent rotations and boundary contact are allowed.

The proof, published by Ahmed 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.

Ahmed, 11SquaresOptimal, Astra-assisted work building on Squares Project and Kleddamag. The matching construction is Trump's.

Significance, composition and next rung

Significance: Resolves global optimality for $n = 11$ , a central case, by closing the gap to Trump's exact construction, beyond the previous strict T-037 lower bound.
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$ . The exact Trump witness attains $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$ . 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.
Novelty: previously-published Present in an identified source

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 this result
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
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-060 in the results table · The $n = 11$ optimality paper · The $n = 11$ explainer

On GitHub, at main

Register: T-060 in results.yaml, line 5201
Evidence: E-n011-global-optimality-report · E-n011-global-optimality-independent · E-n011-lean-formalization-report
Proofs and certificates: certificate final-composition.json · proof PROOF.md · audit review-2026-09-29-n11-optimality-census-contract.md · certificate Optimality.lean · proof Optimality.lean · audit review-2026-10-06-n11-lean-formalization-statement-audit.md
Sources: Ahmed n11 optimality 2026 (its own site, retained copy) · Ahmed 11SquaresFormalized 2026
Source packet: resources/web/n11-optimality-2026-09-29/README.md · resources/web/queuingtheorydotcom-n11-lean-2026-10-06/README.md
Artifacts: 12 artifacts and controls
resources/web/n11-optimality-2026-09-29/source/PROOF.md resources/web/n11-optimality-2026-09-29/README.md resources/web/n11-optimality-2026-09-29/receipts/final-composition.json resources/web/n11-optimality-2026-09-29/receipts/exclusion-inventory.json resources/web/n11-optimality-2026-09-29/receipts/completion-inventory.json docs/project/reviews/review-2026-09-29-n11-optimality.md resources/web/queuingtheorydotcom-n11-lean-2026-10-06/README.md resources/web/queuingtheorydotcom-n11-lean-2026-10-06/receipts/lean/axioms-public-theorems.json docs/project/reviews/review-2026-10-06-n11-lean-formalization-statement-audit.md tests/test_n11_composition_joins.py tests/test_n11_completion_inventory.py tests/test_n11_exclusion_inventory.py
Case file: frontier/n-011.md (verified lower, verified upper, reported lower, reported upper)