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

2026-09-24 established · Levy · $n = 11$

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)$ .

Superseded in part by T-060. The first clause, that every packing in the family has side at least U, which T-060 gives for every packing of eleven squares. The equality clause, that a packing in the family attains U only as a quarter-turn image of Trump's pose with the squares relabelled within the two classes, is not implied, since T-060 makes no claim of uniqueness.

Superseded in part by T-112. The equality clause: a packing in the family at side U is Trump's packing after a container symmetry and a relabelling, by T-112, and reflections leave the family, so it is a quarter-turn image with the squares relabelled within the two classes.

Significance, composition and next rung

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)$ , and its cost, about 1.7e8 nodes for one box, argues against S4's reusable technique.
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.
Unfinished confirmations: C3: BC-240's audited prose steps, which the composition note judges load-bearing, mechanised or reviewed again by a distinct reviewer. 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 this result
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
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-036 in the results table · The $n = 11$ optimality paper · The $n = 11$ explainer

On GitHub, at main

Register: T-036 in results.yaml, line 3104
Evidence: E-n011-h236-rung0-reduction · E-n011-trump-local-theorem-first-clause · E-n011-trump-isolation-radius
Proofs and certificates: certificate bc-240-trump-local-theorem.json · certificate bc-199-trump-isolation-radius.json
Artifacts: 17 artifacts and controls
campaign/series/series-000-smoke-and-calibration/results/agenda-042/exp-232-h236-reader-final2.json.gz campaign/series/series-000-smoke-and-calibration/results/agenda-042/exp-232-h236-tree-manifest.sha256 campaign/series/series-000-smoke-and-calibration/results/agenda-042/exp-232-h236-frozen.txt cases/trump11/fixed_angle_tree.py cases/trump11/fixed_angle_tree_check.py campaign/series/series-000-smoke-and-calibration/experiments/exp-232-h236-rung-zero-closed.md cases/trump11/isolation-theorem.md campaign/series/series-000-smoke-and-calibration/results/bc-240-trump-local-theorem.json campaign/series/series-000-smoke-and-calibration/results/bc-199-trump-isolation-radius.json campaign/series/series-000-smoke-and-calibration/results/agenda-042/bc382-isolation-radius-replay.json.gz campaign/series/series-000-smoke-and-calibration/results/agenda-042/bc382-capture-radius-replay.json.gz campaign/series/series-000-smoke-and-calibration/results/bc-199-isolation-radius-replay-receipt.json cases/trump11/isolation_radius_replay.py docs/project/reviews/review-2026-09-24-bc241-closure.md tests/test_fixed_angle_tree.py tests/test_trump_isolation_radius.py tests/test_review_trump_local_theorem.py
Case file: frontier/n-011.md (verified lower, verified upper, reported lower, reported upper)