n = 11, End to End

n = 11, End to End

This section preserves the former open-case account as of Session 156 on 2026-09-23. For the settled result, see T-060 and the proof review. The linked artifacts are authoritative where the historical text and current case record differ. Claims keep the distinctions epistemics.md draws: proved, machine-verified at a stated V/C rung, numerically observed, or conjectured.

As of 2026-09-23, the verified bracket was $3.875<s(11)\le 3.87708359002281417\dots$$3.875<s(11)\le 3.87708359002281417\dots$, a gap of $0.002083590022814177\dots$$0.002083590022814177\dots$ (n-011). The lower end is Kleddamag’s external certificate, replayed here by two complete methods; the upper end is Trump’s 1979 packing, verified exactly. Every first-party counting family is capped below $3.875$$3.875$, no counting certificate can reach the upper end, and the first measured step toward settling the value by verified global optimization built a search tree about a thousand times larger than estimated.

What a proof has to do

An upper bound is a witness. One packing in a container of side $L$$L$ proves $s(11)\le L$$s(11)\le L$. Trump’s packing, six axis-aligned squares and five sharing a tilt of about 40.18∘${40.18}^{\circ }$, fits at $U=3.87708359002281417730789706010096\dots$$U=3.87708359002281417730789706010096\dots$, the root of the degree-8 polynomial under The Problem. T-011 verifies it exactly over $\mathbb{Q}(u)$$\mathbb{Q}(u)$ at V4/C3, and Why exactness is not optional explains why its 14 zero-gap contacts put it beyond any floating-point checker.

A lower bound excludes every packing at some side, and at $n=11$$n=11$ only counting arguments have done that. A weighted certificate places atoms of total weight below eleven in the container and shows that every admissible shrunken copy of a unit square captures weight at least one; disjoint squares capture disjoint weight, so eleven cannot fit. The weighted-certificate objects fixes the terms, and the tutorial proves the point-atom version from first principles. Two refinements carry the rest of the story:

• Threshold atoms, from T-025 onward, charge a core that captures at least $k$$k$ of a finite point set $S$$S$. Disjoint cores divide $S$$S$ between them, so at most $\lfloor |S|/k\rfloor$$\lfloor \left|S\right|/k\rfloor$ cores are charged and the atom costs that multiple of its weight: a 2-of-3 atom buys two points’ coverage for one point’s budget. The charge is not additive in the points a core captures.
• Parent-core charges, Kleddamag’s form, replace one shrink and one direction net by a catalogue of rows. Each row fixes a half-angle interval for the parent square, a core direction and a core side chosen so that the core fits strictly inside every parent in the interval, and the charge is required only at centres a legal parent can occupy (Kleddamag review).

Point certificates have a proved ceiling. An exact depth-one family of eighty-eight closed shrunken squares at six net directions, of total weight exactly eleven, shows that no D4-symmetric point-atom measure of mass below eleven exists at $191/50$$191/50$ for the retained shrink; scaled to unit squares, the same family caps the one-body point method at $38200/9977\approx 3.8288$$38200/9977\approx 3.8288$ (n-011). Threshold charges are not bound by it: T-025 proves $191/50$$191/50$ where point atoms are foreclosed, and Kleddamag’s certificate reaches $3.875$$3.875$.

Trump’s pose is machine-verified to be locally optimal, and that says nothing far from it. Exp-013 certifies all 128 derivative-distinct fixed-side linearized cones to be zero, so the pose is locally isolated and strictly locally side-optimal. The BC-240 isolation theorem quantifies this in one labelled, anchored 33-coordinate sup-norm chart: within ρ_row = 808514697/200000000000 ≈ 0.0040426 of Trump’s pose, the only labelled packing at side at most $U$$U$ is Trump’s own. The source-distinct BC-241 review accepted the packet, and a full radius-generator replay on 2026-09-24 reproduced it value-for-value, with the method-distinct capture_radius control agreeing on every face; its first clause is verified and exact (BC-241 closure). It does not bear on a different contact class.

Settling $s(11)=U$$s(11)=U$ is a different kind of statement. Trump’s packing is feasible at $U$$U$, so a counting certificate can only exclude sides strictly below $U$$U$. Equality needs every part of the feasible set $\{S\le U\}$$\{S\le U\}$, over eleven centres and eleven angles, closed by infeasibility, a side inequality, a feasible descent, or capture in Trump’s ball. That is verified global optimization (PR 230 review, findings 1 and 2). The Cell Decomposition is why the centres are the easy half: at fixed angles and separating axes the problem is a linear program, so the eleven angles are the bottleneck.

The first-party ladder, and where it stopped

Stromquist’s published 2+4/5​=3.788854…$2+4/\sqrt{5}=3.788854\dots$, independently restored here as T-010, was the bound until 2026-09-04. Every rung of the first-party ladder beyond it is machine-verified (results register, n-011):

Together they moved the bound about $+0.038143$$+0.038143$ past Stromquist. By mid-September three ceilings bounded the retained languages, and the verified bound now sits above all three:

1. The frozen family’s refinement ceiling, $955000/249507\approx 3.82755$$955000/249507\approx 3.82755$. T-033 moved T-026 by $0.000550$$0.000550$, half of what the previous net doubling bought.
2. The point-only ceiling, $38200/9977\approx 3.8288$$38200/9977\approx 3.8288$, about $0.00236$$0.00236$ above T-026.
3. The retained 181-direction fixed-core point model’s packing-side cap, about $3.869$$3.869$ (certificate reach).

A structural program at $96/25=3.84$$96/25=3.84$ split packings by corner class. It produced two conditional exclusions — T-023, one four-owner class, at V3/C3, and T-031, the all-free octagon class, at V4/C3 — and showed the all-deep class to lie outside the point language, so the corner tree cannot close at that side by clipping alone. No packing was excluded at $3.84$$3.84$ unconditionally.

The owner’s 2026-09-14 strategy reset turned this into policy. Agenda 036 keeps paused incremental lanes out of the execution queue unless new evidence changes their expected value; Current Handoff names them, and Session 156 carried the hold forward as a stop condition. The routes chosen after the reset did not move the bound: Route A, a complete physical corner root at $3.84$$3.84$, stopped at its representation boundary with no target run, and Route S’s exp-161 encode-only run timed out unresolved (route selection, Research Program Status and Roadmap). The agenda-040 loop registered T-031 and H-232 and moved no bound. At the intake the verified bracket was $3.826997548829543\dots \le s(11)\le U$$3.826997548829543\dots \le s(11)\le U$, a gap of about $0.0501$$0.0501$.

What the external intake changed

Kleddamag’s certificate proves $s(11)>31/8=3.875$$s(11)>31/8=3.875$. Session 152 retained the pinned v1.0.2 source on 2026-09-22. The container side is $L=191/50$$L=191/50$ and the parent side $A=764/775$$A=764/775$, so the bound is $L/A=31/8$$L/A=31/8$. 679 site orbits expand to 5,284 sites, and 350 positive feature orbits to 2,716 physical features of four kinds: ordinary points, 2-of-3, 2-of-5 and 3-of-5. In units of 10−9${10}^{-9}$ the budget is $10,999,479,944$$10,999,479,944$; every core must receive at least $999,962,528$$999,962,528$, so eleven cores need $107,864$$107,864$ units more than the budget holds. The 12,028 parent half-angle intervals run from $0$$0$ to $207107/500000$$207107/500000$, past $\tan (\pi /8)$$\tan (\pi /8)$. A 2-of-5 feature costs twice its weight, and the review checked that the source’s proof and its budget computation both charge it so (Kleddamag review). The source credits this repository’s T-026.

Which ingredient beat the first-party ceilings is not established. The threshold principle was already here, in T-025 and in sqpack.fractional.threshold. The certificate changes five-site features, movable supports, the parent-centre restriction and the adaptive angle catalogue together, and the review states that no ablation attributes the improvement to any one of them.

It is verified here in three layers:

The case record holds verified_lower_bound: 31/8 on both evidence entries and states that this confirms Kleddamag’s published bound (n-011). The existing T-037 registers that published result at V4/C4; this review adds no new result or C5 claim. The certificate closes 95.89% of the interval from T-026 to $U$$U$; the review is explicit that the percentage is not a probability of optimality.

The other external results bear on $n=11$$n=11$ only lightly. Tokoharu’s rectangle-density certificate proves the weaker $381/100$$381/100$ here, fully replayed (integration review); wand125’s ten point certificates concern other $n$$n$; and Guzhou0806’s R038 scanner enters only as the pinned lineage of Kleddamag’s JavaScript sweep.

The first-party record was reconciled to it. Session 154 kept T-033 registered at V4/C3, rescored from S5 to S3 as method and calibration evidence, and corrected T-024 from C4 to C3, because a derived dilation claim takes the minimum rung over its single exact-algebraic derivation. The integration review’s instruction for research is that a first-party rung below $3.875$$3.875$ is controlled evidence or a simpler certificate, not a public lower-bound advance.

After the intake: explorations, reviews, and the settlement ladder

PR 230 published three explorations and moved no bound. Session 155 retained three diagnostic tools, seven receipts and 31 shaped idea rows, and registered no hypothesis.

• X-043 lays out six architectures for stronger counting bounds, from charge-deficit counts on a certificate’s own low-charge poses and co-designed core menus to group budgets, a capture theorem ending in Trump’s ball, a positive-semidefinite kernel, and small higher-order exclusions. Its token-group spike on Kleddamag’s ten 2-of-5 orbits found zero budget saving in all four eligible unions.
• X-044 maps what transfers between the low open cases, keeps $n=11$$n=11$ first and makes $n=12$$n=12$ the next mathematical target.
• X-045 aims at the exact value. Its cutoff composition theorem: given a witness at $U$$U$, attainment, a verified $s(11)\ge L$$s(11)\ge L$, and every local side minimum with side in $[L,U]$$[L,U]$ having side $U$$U$, then $s(11)=U$$s(11)=U$. It proves that there are finitely many local-minimum side values, since the local minimizers form a semialgebraic set with finitely many components on each of which the side is constant, so some cutoff $L<U$$L<U$ exists, with no effective value. Throughout $[31/8,U]$$[31/8,U]$, at most three squares touch any wall. An exact audit adds two negatives: Trump’s top-right corner is empty, so an all-four-corners premise is false, and Kleddamag’s first row already fails at $U$$U$, its unchanged core capping that row near $3.8750124$$3.8750124$.

Session 156’s reviews changed what counts as progress. Four independent reviews of PR 230 found no fatal error (PR 230 review):

1. No counting certificate can prove $s(11)=U$$s(11)=U$. With $31/8$$31/8$ known, X-045’s cutoff statement is equivalent to $s(11)=U$$s(11)=U$ rather than a partial result; its operational residue is that first-order descent is an admissible leaf.
2. Settling $n=11$$n=11$ is verified global optimization, and the angles are the bottleneck; the X-045 reviewer proposed a rigorous H-112 as the first theorem milestone.
3. Kleddamag’s certificate has no side headroom. Its least core collar $A-B$$A-B$ is 3.26×10−9$3.26\times {10}^{-9}$, so the unchanged-core ceiling is 31/8+10−8$31/8+{10}^{-8}$, and 11,981 of its rows attain their minimum at the corner-flush parent pose. Any certificate gain at $n=11$$n=11$ needs an adaptive parent-core producer with 2-of-5 and 3-of-5 features, which the record does not have; the cheapest sound next form is H-155’s corner two-band count. Session 156 records these collar and corner-pose figures as exploratory computations.
4. Frozen-weight low-n transfers are arithmetically dead at the old direction nets.
5. The retained evidence is sound: all seven receipts replay to identical exact values.

X-046 turns settlement into a ladder. X-046 finds no dimension-reduction lemma that is both provable with current tools and strong enough to remove angle dimensions. The angle-merging normal form H-121 is the conjecture in another form, not a lemma on the way to it. What can be proved is a ladder of restricted-family theorems, each strengthening Stromquist’s Theorem 3, which puts every packing oriented only at 0∘$0^{\circ }$ and 45∘${45}^{\circ }$ at side at least 2+(4/3)2​≈3.885618$2+(4/3)\sqrt{2}\approx 3.885618$, $U+0.008534$$U+0.008534$:

Each box is decided by replacing every square with its rotational core, the intersection of the square over its angle window, so that each leaf is an exact rational Farkas or dual certificate with no interval arithmetic inside the linear program. A full search is priced by two constants: $c$$c$, the side lost per radian of box width by the relaxation, and $V(\epsilon )$$V(\epsilon )$, the volume of $\{f\le U+\epsilon \}$$\{f\le U+\epsilon \}$ modulo symmetry. Until both are measured, X-046 prices “settle by search” as between a week and never. Its four unretained f64 probes include one showing that Kleddamag’s per-row minimum charge falls by 68.2% at the axis angle when the container grows to ratio $3.877084$$3.877084$, so the certificate carries no transferable slack to $U$$U$.

Three experiments ran the ladder’s first lanes the same night.

• exp-227, H-237: the growth-cone route cannot beat Trump’s radius. The exact minimum growth of the side over the whole direction sphere is $0.0517714532056682325\dots$$0.0517714532056682325\dots$, 4.5 times the isolation packet’s uniform modulus $\kappa \approx 0.01148$$\kappa \approx 0.01148$. But an exhaustion lemma shows that any certificate bounding each row’s second-order remainder separately is capped by the BC-199 weighted modulus, which is where $\rho$$\rho$ came from; the computation confirms it on all 8,448 faces. Along the binding direction 36 of 42 rows do not recover at second order, so what binds is the remainder model, not the geometry. H-237 is exhausted; its successor is idea 246.
• exp-228, H-238: the census found no third orientation below Stromquist’s value. 1,000 jolted starts about Trump’s and Stromquist’s packings were quenched and passed through a new descent filter, which rejects an endpoint only with an exact rational packing verified at least 10−8${10}^{-8}$ below it. It refuted all 85 quench stops with three or more orientation classes below $3.885618$$3.885618$. Two descent-stable minima within $U+0.02$$U+0.02$ are new to the record: a two-orientation packing at 0∘$0^{\circ }$ and 41.56∘${41.56}^{\circ }$ with side $3.8867460286$$3.8867460286$, and a three-orientation packing with no free squares at $3.8943218738$$3.8943218738$. Only 94 quenches converged under host load, and the census cannot be replayed bit for bit. H-238 is confirmed at its declared census scope only: numerical observation, not proof.
• exp-231, H-236: rung 0 is mostly closed, at a thousand times its estimated cost. The producer fixed_angle_tree.py and the independent reader fixed_angle_tree_check.py passed their controls, among them the $n=5$$n=5$ family closing at s(5)−10−3$s(5)-{10}^{-3}$ in 229 nodes. A W2 review found the certificate contract sound, with one material finding: the registered $n=11$$n=11$ negative control is met only at producer level (rung-0 review). In about 6.4 hours of wall, 198 of 256 subtrees closed on 1.19×108$1.19\times {10}^8$ nodes; 58 remain at the wall cap. The reader accepted all 84,777,070 exact leaf certificates and 14,041,104 branch nodes, the three Trump-degenerate leaves close through the BC-240 local theorem, and no leaf below $U$$U$ has appeared. Exp-232 then ran the last 58 with the same bytes, and the reader closed the complete tree: 119,556,859 leaf certificates and 19,883,887 branch nodes, three Trump-degenerate leaves, no unresolved leaf. H-236 is confirmed: at Trump’s own angle, within 10−6${10}^{-6}$ in the half-tangent, no packing beats $U$$U$; its terminal leaves use BC-240’s first clause, verified and exact since the BC-241 closure. After a Fable max review it is registered as T-035, the machine-verified reduction to the BC-240 ball, and T-036, the composed optimality theorem. The whole tree cost about 1.7×108$1.7\times {10}^8$ nodes. Each added square multiplies the tree by roughly six or seven, so rung 1 is out of reach with this relaxation; the lever is a stronger bound per node, not more boxes.

What worked and what did not

One dependency sits outside the record: the rung-0 tree is 5.5 GB in the Session 156 worktree’s attic/rung0/, so resuming it depends on that directory surviving.

Identified but not pursued

The owner’s 2026-09-14 hold still stands, and the owner’s decision on retiring H-121 as a route, which X-046 recommends, is open. Statuses below are the ledger’s and the idea board’s; blockers and next steps are those the records name.

Registered $n=11$$n=11$ hypotheses that are open, blocked or stopped:

Idea-board rows not yet registered, from X-043, X-045, X-046 and exp-227, with the older $n=11$$n=11$ rows they touch:

Three directions the PR 230 review lists as missed are not yet rows: symmetry canonicalization on the cover side of a verified search; a threshold-language ceiling family near $3.876$$3.876$, to bound how far counting can reach; and the pruning tests of the verified-global-optimization literature, from Markót and Csendes’s circle packings to Montanher and coauthors’ unit squares in a circle.

The exact n = 11 result

Established. $s(11)=T=3.877083590022814\dots$$s(11)=T=3.877083590022814\dots$, the exact side of Walter Trump’s packing. T-011 verifies the algebraic witness and T-060 supplies the matching global lower bound for arbitrarily rotated unit squares with disjoint interiors and boundary contact allowed. The latter is Ahmed’s Astra-assisted proof, building on this project and Kleddamag, independently replayed and mathematically audited here at V3/C3/S5.

The proof review maps the 2,184 canonical patterns, 2,180 exclusions, four symmetric survivors, exact D4 bridge, complete capture tree and fixed-side local isolation. The replay uses pinned source inputs and shares the mathematical geometry primitives disclosed in the review; it is an exact computational proof audit, not a proof-assistant formalization or a second independent method. Four final-state digests in the publisher’s cached audits are stale, so those cached PASS records do not establish the claim; the fresh source-bound replay and final composition do.

Kleddamag’s $s(11)>31/8$$s(11)>31/8$ (T-037) remains an earlier, independently verified lower bound. The restricted six-plus-five theorem and local Trump theorem (T-035 and T-036) retain their own scopes. The separate wand125 ceiling and row-minimum reports (T-058 and T-059) have not been promoted by T-060’s verification. Global optimality of the side does not assert uniqueness of the optimal arrangement. The earlier research program and its unpriced routes are retained in X-046 as the history of how the gap was approached before this proof.