A Review of the Optimality Proof of the Trump Packing of 11 Squares

This paper explains the computer-assisted optimality proof published by Queuingtheorydotcom in 11SquaresOptimal. The original mathematical argument, verification driver, certificate data, and reproduction instructions are pinned to the source revision reviewed here. Queuingtheorydotcom’s announcement credits Astra’s work building on the Squares Project and Kleddamag.

The components have distinct provenance:

• Attaining construction: Walter Trump’s packing, with David Ellsworth’s reconstruction and exact formulas, retained in the construction source record.
• Mathematical antecedents: the Squares Project’s threshold-certificate method, which Part I of this series explains, and its local-isolation theorem, together with Kleddamag’s earlier proof of a lower bound of 31/8 (retained source), which Part II explains. The original proof’s third-party notices identify its incorporated Squares Project revision.
• Verification and exposition here: the Squares Project’s T-060 result record, retained proof and verification packet, and mathematical acceptance review document the confirmation explained in this paper.¹

For a technical review, start with the T-060 validation guide. It links the published proof, certificate inputs, independent checks, and accepted evidence for each obligation. The guide distinguishes checking retained evidence from a fresh geometric replay and states the remaining work needed for a standalone executable package.

The Result

Place eleven unit squares inside a larger square. Each small square may rotate independently. Their edges may touch, but their interiors may not overlap. How small can the container be? Write \(s(11)\)$s(11)$ for the smallest such side and \(L_0\)$L_0$ for the side of a container under test, as Part I does; the theorem below shows that a smallest side exists.

The answer is the side length of Trump’s construction in Figure 1:

\(T\)$T$ is an algebraic number of degree eight. Let \(u\)$u$ be the unique positive real root of

it lies in \((9/25,37/100)\)$(9/25,37/100)$, and the proof’s exact arithmetic uses that interval to tell it apart from the polynomial’s other roots. Then

The polynomial is a contact condition between two of the eleven squares; the construction section says which.

Theorem. Eleven unit squares with arbitrary independent rotations and pairwise disjoint interiors fit in a square of side \(T\)$T$, and do not fit in any square of side \(L_0<T\)$L_0<T$. The smallest side is therefore attained, and \(s(11)=T\)$s(11)=T$.²

The evidence behind the lower bound is a set of component computations, each observed and reviewed separately. Each accepted execution is retained as a receipt: its verdict, a hash of every input object and of the checker’s own bytes, the command and commit that produced it, and a replay script. A program called the composer reads a fixed set of receipts by hash and checks the joins between them without rerunning the geometry; no single fresh run of the whole proof has yet been made. The closing section states that scope exactly.

An upper bound needs one example: the packing drawn above. A lower bound must exclude every arrangement in a smaller container, including unfamiliar contact patterns and eleven independently chosen angles. Numerical search can suggest a good packing, but failing to find a better one does not exhaust those possibilities.

Suppose a packing fits in a smaller square, of side \(L_0<T\)$L_0<T$. The proof must handle that packing without knowing any of its positions or angles. It first classifies the centers and uses exact certificates to eliminate impossible classes. Every survivor, after a symmetry of the container, enters a capture argument that encloses its positions and angles near the known construction.

The last step connects this global restriction to a local theorem. The same smaller packing can be placed inside the exact side-\(T\)$T$ container, within a checked neighborhood where only the construction is feasible. But the construction spans \(T\)$T$, so it cannot fit inside the smaller container. Figure 2 shows both halves of the proof.

The geometric steps are center classification, safe exclusions, symmetry, and capture. The local estimate and exact frame change complete the contradiction.

From Weighted Points to a Global Proof

Part I of this series develops the lower-bound method from weighted points. Select a small core strictly inside each packed square; the charge a core receives is the weight it collects. If every possible core must receive a charge of at least one, eleven disjoint cores must receive at least eleven units. A certificate with less than eleven units available proves a contradiction. Exact coverage checks turn that idea into a theorem about every position and orientation. Part I explains the point certificate T-018, the threshold certificate T-025, whose \(k\)$k$-of-\(m\)$m$ charges pay a core holding at least \(k\)$k$ of its \(m\)$m$ charge sites, and T-026’s dilation bound \(s(11)\ge3.8264474\ldots\)$s(11)\ge 3.8264474\dots$. Part II explains Kleddamag’s T-037, \(s(11)>31/8=3.875\)$s(11)>31/8=3.875$, and what it changes in T-026’s certificate.³ Figure 3 places these bounds in order.

The bound gap between \(3.875\)$3.875$ and \(T\)$T$ is small, but closeness of two numbers supplies no geometric information about a hypothetical packing in between. The optimality proof adds two kinds of information. It conditions geometric and charge arguments on occupied center regions, so they can eliminate individual patterns. For the pattern that survives, it proves where every square must be, then applies a quantitative local theorem at the exact endpoint. The earlier bounds are antecedents of the method, not premises of the proof: the proof does not infer equality from a sequence of improving lower bounds, and the separate tools that check related certificates, wand125’s row-minimum check of T-037 (T-059, in Part II) and Tokoharu’s rectangle-density verifier, do not verify this argument.⁴

The Construction Gives One Half of the Answer

The algebraic parameter \(u\)$u$ determines a rotation:

Here \(c\)$c$ and \(s\)$s$ are the cosine and sine of the common tilt \(a\)$a$ of the five tilted squares in Figure 1, and \(u=\tan(a/2)\)$u=\tan (a/2)$, with \(a=2\arctan u\approx40.18^\circ\)$a=2\arctan u\approx {40.18}^{\circ }$. The same half-angle parameter later describes the orientation of an arbitrary square. Appendix A gives the placement formulas; number the squares 0 to 10 in the order listed there. Because a rotation preserves length and right angles, those formulas produce eleven unit squares.

Feasibility has two finite checks. Each of the 44 vertices must lie in \([0,T]^2\)$[0,T{]}^2$. Each of the 55 pairs of squares must have disjoint interiors. For two convex polygons, project both onto a direction and call the distance between the two projection intervals the gap in that direction, negative when the intervals overlap. The polygons have disjoint interiors exactly when some edge normal of one of them has a nonnegative gap, a weak separating axis; a gap of zero in that direction means the polygons touch, which is legal. Fourteen pairs touch in the construction, and the other 41 are separated by a positive gap.

The calculations take place in the number field \(\mathbb Q(u)\)$\mathbb{Q}(u)$, the polynomial expressions in \(u\)$u$ with rational coefficients. Expressions are reduced using the equation defining \(u\)$u$, and because \(p\)$p$ is irreducible, division is exact there too; the selected root is isolated by rational bounds. Exact identities establish zero, while rational interval refinement determines the signs of nonzero expressions. A small floating-point error is never substituted for an equality.⁵

These checks prove \(s(11)\le T\)$s(11)\le T$. Twenty vertex coordinates are exactly \(0\)$0$ or \(T\)$T$, with vertices on all four walls, so the construction’s horizontal and vertical spans are both exactly \(T\)$T$; the last step of the proof uses this fact.

The defining polynomial of \(u\)$u$ is itself one of the fourteen contacts. If \(u\)$u$ is treated as a free parameter in Appendix A, every wall contact (a square touching a side of the container) and thirteen of the square contacts hold identically. The remaining one, between square 2, \(A(x_0,T-1)\)$A(x_0,T-1)$, and square 10, the image of \(A(\eta+2,-\zeta)\)$A(\eta +2,-\zeta )$, has gap \(p(u)/\bigl(2u(1-u^4)(1+2u-u^2)\bigr)\)$p(u)/(2u(1-u^4)(1+2u-u^2))$, which vanishes exactly at the root; for smaller \(u\)$u$ the two squares overlap.⁶ On the interval \([9/25,37/100]\)$[9/25,37/100]$ the derivative \(p'\)$p^{\prime }$ exceeds \(4\)$4$, so the root there is unique.⁷

Sixteen Regions Cover All Possible Centers

Most of the global calculations use the rational number

This cap is slightly larger than the proposed optimum. If a packing existed in a square of side \(L_0<T\)$L_0<T$, we could translate its container concentrically into \([0,U]^2\)$[0,U{]}^2$. Its unit squares would keep their sizes, angles and relative positions. Thus excluding possibilities in the cap also excludes them for every smaller container. One storage convention needs a name. The certificate files record a center \(p\)$p$ as the scaled file coordinates \(p_f=(191/50)\,p/U\)$p_f=(191/50)p/U$, so that the container has side \(191/50\)$191/50$ in the files; this paper states every quantity in physical units, and the checkers undo the scale wherever they read the files.

A unit square contains an open disk of radius \(1/2\)$1/2$ about its center. Two packed squares therefore have centers at least one unit apart: otherwise those disks, and hence the square interiors, would overlap. Also, each center \(p\)$p$ lies in \([1/2,U-1/2]^2\)$[1/2,U-1/2{]}^2$. Normalize this center domain by writing

Choose sixteen rational cover sites. Assign each point of \([0,1]^2\)$[0,1{]}^2$ to any nearest cover site, keeping ties. The resulting closed Voronoi cells cover the whole square. They are the polygons in Figure 4, rather than the squares of a uniform grid: a grid cell would have physical diameter \(1.017\)$1.017$, too large for the lemma below, while the largest of these cells has physical diameter \(0.975\)$0.975$. The exact checker reconstructs them from nearest-site halfplanes and proves

Center-cover lemma. A physical cell contains at most one packed-square center. Indeed, two centers in it would be less than one unit apart, contradicting the disk argument. A center’s label is the index of a cell containing it; at a cell boundary either containing label may be chosen, and the same argument still prevents two centers from receiving one label. A packing on a boundary therefore admits more than one labeling, and each labeling it admits is excluded on its own below.⁸

An eleven-square packing therefore chooses eleven different labels among sixteen. There are

possible subsets, called masks. The cover sites are symmetric under the half-turn \((x,y)\mapsto(1-x,1-y)\)$(x,y)\mapsto (1-x,1-y)$ of the center square, which maps cell \(j\)$j$ to cell \(15-j\)$15-j$; they have no other symmetry, which matters later. No eleven-element mask is fixed by this pairing, since a fixed mask would have even size. Choosing one representative from each half-turn pair leaves 2,184 cases, each a representative mask together with everything the proof derives for it. These representatives are sorted and numbered starting at zero.

The center-cover reduction permits every orientation. A square’s orientation is defined only up to a quarter-turn, so take its angle \(\theta\)$\theta$ in \([0,\pi/2]\)$[0,\pi /2]$, where both endpoints describe the same square. For each square separately, write \(t=\tan(\theta/2)\)$t=\tan (\theta /2)$. Then

This rational parameterization makes interval calculations exact; the tilted squares of the construction have \(t=u\)$t=u$. Both endpoints are retained, even though they describe the same square orientation. A certificate never samples angles: it works in rows, each a closed interval of \(t\)$t$ for one square together with the centers allowed over that interval.

The frames and units used below, for reference:

One Geometric Invariant Supports the Certificates

Fix a case. A pose is a square’s center and angle. An owner is the square assigned to an occupied cell. Although the packing is unknown, two kinds of rigorous information can be maintained about each owner:

• An outer pose cover contains every pose still possible for that square: a set of rows, closed angle intervals with their center polygons. It may also retain artificial poses that no valid packing realizes.
• An owned hull is a convex polygon that lies strictly inside the square in every valid packing under the current assumptions, even while the square’s position is uncertain.

The first is an overestimate of possibilities; the second is a guaranteed interior. Together they are the invariant, stated row by row: in every valid packing under the current assumptions, for every row of an owner whose angle interval contains the owner’s actual angle, the owner’s actual center lies in that row’s center polygon; and the rows’ angle intervals together cover the whole allowed angular range. This is stronger than saying the pose lies in the union of the rows, and the difference matters at a seam: two rows that share an endpoint angle both enclose a pose at that angle, so a branch, an argument that assumes one side of a closed split, may restrict the angle to one side and drop the other row’s single shared angle, because the retained row already carries the guarantee there. A branch may never drop a point or a segment of a center polygon on that ground; those have their own exact treatment. Initial owned points need their own proofs, using open inscribed disks or wall inequalities, or come from a seed, a set of points whose ownership has its own checked proof. Ownership is quantified the same way, over valid packings: an owned hull need not lie inside the artificial poses that a deliberately loose outer cover retains, and one retained row of the capture proof contains such a pose, in which a seed point falls outside an artificial square that the walls already forbid.⁷ An update (the proof data say step) takes one owner’s rows, removes centers that an argument below forbids, and records what remains as the residual of each row; a row with a nonempty residual is live. Search programs propose rows, residuals and cuts (closed half-plane conditions on a center); the checker proves or refuses them. The same invariant supports case exclusion and, later, capture near the construction.

Removing poses that force overlap

Suppose another square must contain a small inner region. A proposed position of our square is impossible if it forces their interiors to overlap. We can reject a whole region of centers at once, provided the collision is guaranteed for every angle in the row. All other positions remain available until a further argument excludes them.

For an angle interval, choose a convex core \(Q\)$Q$ around the origin that lies strictly inside the centered unit square at every angle in the interval. After substituting the half-angle formulas, the needed inequalities reduce to signs of rational quadratic polynomials. Checking endpoints and any interior minimum establishes the inequality over the entire interval, as the independent control beside Part II’s Strict-core lemma does for square cores.

Let \(K\)$K$ be an owned hull of another square. A proposed center \(x\)$x$ is forbidden if

For such a center, \(k=x+q\)$k=x+q$ belongs to both squares’ interiors. This proves overlap. The strict interior guarantees justify rejecting even the boundary of this closed forbidden region. If the cores merely touched the squares’ boundaries, the same rejection could incorrectly remove a legal touching configuration.

A second collision check compares a region of proposed centers, over one angle row, against every row of another square’s pose cover, its partner rows. It may exclude the region only when collision is forced for every partner row, including the endpoints of its angle intervals.

Keeping everything else

Removing a list of forbidden polygons is insufficient unless the remainder is accounted for. The checker first computes the domain it must cover: the row’s domain in the accepted predecessor state, the state the update starts from, cut down by two necessary conditions, that the square lies inside the container and that it contains its own owned hull, which bounds where its center can be. It then checks that this required domain is covered by the verified forbidden regions together with the proposed residual regions. A proposal may describe a larger domain; only the required domain must be covered. Exact arrangement checks include segments, singleton points and zero-area intersections. An area sum alone cannot detect a missing segment where a touching packing might live. One historical helper deserves a named caveat: the one-dimensional interval test inside the frozen checkers of charge certificates and of capture accepts a singleton target \([a,a]\)$[a,a]$ when a supplied interval lies entirely below \(a\)$a$, so it is not a general closed-interval checker. Its use there is sound for a different reason: the target is a convex polygon of positive area, the sweep examines every interior slice, which has positive length and cannot trigger the defect, and a finite union of closed covering regions contains the limits of those slices and hence the boundary. Zero-area domains never reach that helper: the charge-certificate checkers refuse them, and the capture and generic checkers send them to an exact point and segment check. New callers use a corrected kernel that treats \([a,a]\)$[a,a]$ as covered exactly when some supplied closed interval contains \(a\)$a$; the faster cover kernel that the center partition uses was already correct.⁷

After the complete surviving angle cover has been checked, the points that lie strictly inside the square for every surviving pose, the common core, can be added to the owned hull; their convex hull is also strictly inside. The hull may then be compressed to fewer vertices by exact convex combinations, which only shrinks it. These points constrain the other squares.

Pose-preservation lemma. Starting from a valid outer cover and valid ownership, each accepted update preserves every actual packing under its stated assumptions. If an occupied square’s complete pose cover becomes empty, the case is impossible. If two independently established owned hulls intersect, the two square interiors overlap and the case is again impossible.⁹

The order of updates matters. A point cannot be used as owned before the check establishing its ownership. Each update names the state it starts from, which must be the state its predecessor produced; when several owners are updated in parallel, all of them start from the same declared common prior, and their results are joined only after every one succeeds. The certificate consumers check these dependencies as well as the local inequalities.

Charge Budgets Exclude Many Patterns at Once

The weighted-point idea becomes more selective when the occupied cells are known. A field certificate assigns a charge to every strict inner core; the charges it assigns, as a function of the core, form its charge field. It proves that a square centered in cell \(i\)$i$ must receive charge at least \(\Gamma_i\)${\Gamma }_i$, unless it would collide with an already proved owned hull. In a legal packing the collision alternative is unavailable, so the charge lower bound must hold.

One useful charge is defined by five charge sites. For each projection direction, consider the median of the five projected sites. A core receives charge one when its projection interval contains that median in every direction. Equivalently, every closed half-plane that contains the core contains at least three of the five sites; the two supporting half-planes of each direction give the equivalence. A third form is the one to picture: the core meets the convex hull of every three of the five sites (a three-site hull that misses the core is strictly separated from it by a line, and the half-plane of that line containing the core then holds at most two sites). None of the three forms says that the core contains three sites. With sites at \((\pm1/2,0)\)$(\pm 1/2,0)$, \((0,\pm1/2)\)$(0,\pm 1/2)$ and \((1/2,1/2)\)$(1/2,1/2)$, the square core \([-3/10,3/10]^2\)$[-3/10,3/10{]}^2$ contains none of them, yet every three of them include two of the four axial sites, whose midpoint lies in the core, so the core receives the charge.⁷ The certificate reduces the condition to finitely many direction inequalities. For the square cores used by these field certificates, directions parallel to the core’s axes and normals to site-pair lines divide the directions into sectors. Within each sector the median site and the signs in the core’s support function stay fixed, so the inequalities are linear in the direction normal; because both axes are among the dividing directions, no sector exceeds a quarter-turn, and the two bounding directions suffice.

Two disjoint strict cores cannot both receive that charge. A strictly separating direction gives them disjoint projection intervals, which cannot both contain the same median; in the half-plane form, the two closed half-planes on either side of a separating line would each contain three of the five sites, which is impossible. The charge therefore has capacity one: over any family of disjoint cores it sums to at most one. A checked example forces the squares in two occupied cells each to receive charge one, giving \(2>1\)$2>1$. Owned-point collision regions help prove that each cell must be charged, but those collision regions pay no charge.¹⁰ Other certificates use three or seven charge sites, add weighted charges at single points, or combine several such charges; each charge contributes its weight to at most one core, and the budget \(b\)$b$ is the sum of the weights. A k-of-m charge of Part II can pay as many as \(\lfloor m/k\rfloor\)$\lfloor m/k\rfloor$ disjoint cores; when \(2k>m\)$2k>m$, a core holding \(k\)$k$ of its sites also receives the median-type charge on them, which has capacity one.

The accepted certificate for mask 0, which Figure 8 draws, is the smallest example. It requires owners in cells 0, 1, 2, 3 and 6, whose 55 owned points have their own proofs, and requires a charge of one in each of cells 1 and 2 against a budget of one. Cell 1 is covered by 67 rows and cell 2 by 69. In the first row of cell 1, over the half-angle interval \([0,1/64]\)$[0,1/64]$, every center in the cell’s legal domain either activates the five-site charge or places the core over a point owned by square 0 or square 2, which no valid packing allows; the accepted proposal covers the row with the charge’s region and four such points, and two already suffice. So each of the two cells receives charge one, the total is \(2>1\)$2>1$, and the certificate excludes every case whose mask or half-turn contains its five owner cells: 459 of them.¹⁰

A certificate requires certain owner cells \(O\)$O$ to be present, because their owned hulls supply its collision regions, and assigns lower bounds \(\Gamma_i\)${\Gamma }_i$ to the cells in a set \(P\)$P$. It excludes a mask \(J\)$J$ when

and likewise when the half-turn image of \(J\)$J$ satisfies the same two conditions, since that image is the same case. This explains why one checked certificate can exclude many masks: its antecedent is only that the cells of \(O\)$O$ are occupied, so it applies to every mask containing them. Equality with the budget excludes nothing. In every accepted certificate the charged cells lie in \(O\)$O$ and their bounds already exceed the budget, so in practice the rule reads: a certificate excludes every case whose mask, or its half-turn, contains its owner set.⁶

The accepted exclusion inventory combines 1,904 cases excluded by field certificates and 276 cases excluded one at a time by the pose-cover updates above, which the proof data call generic certificates. Its conclusion is the exact set equality

The check compares case identities and dependencies, not only the number 2,180. The publisher groups the same excluded set by provenance as \(1931+76+173\)$1931+76+173$: its original baseline, 76 prior-family cases that extend it, and 173 cases returned later. The two groupings divide the same obligation; they are not different totals or additional exclusions.¹¹

Some exclusions have extra assumptions that must be discharged. Cases 2175 and 2176 use cuts on center positions that are justified by symmetry, and that justification assumes the 1,931 exclusions of the publisher’s original baseline: the cuts are checked only against the 253 cases the baseline leaves. Cases 2175 and 2176 are two of the publisher’s 76 prior-family cases, and the only two whose accepted certificates carry this premise; it is a premise of those certificates.¹² wand125 reports a Lean proof of all 76 prior-family cases that does not use it.¹³ The four-survivor reduction below assumes these two exclusions in turn, so their cuts may not use it; the dependency runs one way. Case 1383 requires both sides of a closed center split at \(y_{13}=4/3\)$y_{13}=4/3$. Here \(y_{13}=p_y-U/2\)$y_{13}=p_y-U/2$ is the centered physical height of the square assigned to cell 13. Both sides of the split and the state they split remain part of the accepted proof, even though the common geometric invariant lets us describe them briefly.

Symmetry Reduces the Four Survivors to One

Rotating or reflecting the entire container preserves feasibility. The four surviving masks are the construction’s own center pattern seen under the eight symmetries of the square: the identity and the half-turn give mask 1462, the two reflections in the axes give 999, the two reflections in the diagonals give 1659, and the two quarter-turns give 438 (no center of the construction lies within \(0.0079\)$0.0079$ of a cell boundary in normalized units, so these labels are unambiguous).⁶ It is tempting to rotate the cell labels and declare the four masks equivalent, but the irregular Voronoi cover does not permit that shortcut. The half-turn is the cover’s only symmetry; a quarter-turn or reflection need not send a whole cell to another cell.

Instead, consider four views of each normalized center:

Together with half-turns these represent the eight symmetries of a square, usually called \(\mathbf{D}_4\)${𝐃}_4$ (Part I). Intersect the inverse images of the cells in the four views. The result is a finite overlay of 220 nonempty closed regions: 212 polygons and eight singleton points. A center in one overlay region has a specified allowable label in each view.

For two overlay regions, exact vertex calculations sometimes prove that every pair of points, one in each region, is less than one unit apart in physical coordinates. Such a pair cannot contain two centers. The check retains 1,572 strict distance bans; a distance equal to one is not banned.

Symmetry lemma. Once the 2,180 exclusions hold, every remaining packing has a symmetry image that admits case 438, the pattern of the quarter-turned construction. To prove this, suppose every view avoids 438 and its half-turn. Each view must then have a mask from the other three candidates and their half-turns. Exhaustive finite enumeration tries the compatible overlay assignments, requiring distinct occupied labels in each view and respecting all distance bans. None exists.¹⁴

Every genuine packing would supply such an assignment by choosing containing closed cells in each view. Their nonexistence proves the lemma, including all boundary ties. The enumeration may allow geometric arrangements that no real packing realizes; that only makes its impossibility conclusion stronger.

The same conclusion has a shorter proof that needs only one distance ban. A retained checker carries it beside the accepted one, but the composed proof rests on the exhaustive search above, and the shorter proof is not one of its premises. Fix the mask of the identity view and consider the 216 ways to assign one of the six non-438 masks to each of the other three views. Propagating the cell labels through the overlay, each owner keeps only the regions whose labels in every view agree with that view’s mask, and an owner left with no region, or a mask label that no owner carries, ends the triple at once. That leaves 47, 17 and 20 triples for the identity masks 999, 1462 and 1659, and forcing, an owner reduced to one region reserving its labels, leaves one, one and none. In the survivor for 999, the owners of cells 1 and 2 are each confined to one overlay region, inside \([23/50,27/50]\times[0,11/100]\)$[23/50,27/50]\times [0,11/100]$ and \([11/25,14/25]\times[23/100,7/25]\)$[11/25,14/25]\times [23/100,7/25]$ in normalized coordinates, so their centers differ by at most \(1/10\)$1/10$ horizontally and \(7/25\)$7/25$ vertically and lie less than one unit apart, since \((U-1)^2\bigl((1/10)^2+(7/25)^2\bigr)<1989/2500<1\)$(U-1{)}^2((1/10{)}^2+(7/25{)}^2)<1989/2500<1$. The survivor for 1462 is the reflection of that one through the first view, and the same pair of regions closes it.⁷

Capture Forces Case 438 Near the Construction

Case 438 specifies the occupied cells

The pose-preservation invariant now serves a different purpose. Rather than emptying every pose domain, the checks progressively enclose surviving poses near the quarter-turned construction. The proof is a tree of nodes. Each node is a checked state, the pose covers and owned hulls of all eleven owners, together with the branch assumptions it inherits; each leaf ends either in a contradiction, a far leaf, or in an enclosure, the near leaf. The root carries no assumption. Before the tree, fourteen root rounds, each a parallel update of all eleven owners from a common prior, establish the root’s ownership; the root node then completes thirteen further updates of its own. A fourteenth step covers only part of its angle range; it is checked but changes no ownership. All of this is replayed here, in the capture receipts cited below, before the local theorem is invoked.

Three closed splits produce four branches. Here square subscripts denote owner-cell labels; \(y_{15}\)$y_{15}$ is a centered physical height and \(t_i\)$t_i$ is the half-angle parameter of the square assigned to cell \(i\)$i$.

Equality belongs to both sides of every split. The overlap is harmless and prevents a missing boundary branch.

The final near state contains 136 live rows and 1,542 center vertices. The pose-inclusion check proves that all their center polygons and all their angle intervals lie inside the same local rectangle, which the next section describes. Convexity extends center bounds from vertices to whole polygons. Exact bounds for \(2\arctan(t)\)$2\arctan (t)$ convert interval endpoints to angular displacements in radians. For an axis-aligned square, an interval near \(t=1\)$t=1$ describes the same orientations as one near \(t=0\)$t=0$, and the chart change \(t\mapsto(t-1)/(t+1)\)$t\mapsto (t-1)/(t+1)$, which equals \(\tan((\theta-\pi/2)/2)\)$\tan ((\theta -\pi /2)/2)$, measures its displacement from that side. A half-angle parameter is never substituted for a radian angle. The root rounds, the accepted ten nodes and their nine parent edges together bind this enclosure to the original unconditional case, rather than to an assumed favorable starting pose.¹⁵

The Local Argument Excludes Every Nonzero Motion

Fix the container as \([0,T]^2\)$[0,T{]}^2$ and label the eleven squares as in the exact construction. A perturbation has 33 coordinates:

The checked local neighborhood is a rectangle \(|h_j|\le r_j\)$|h_j|\le r_j$, with positive coordinate radii \(r_j\)$r_j$. Different coordinates have different radii, allowing the rectangle to fit the captured domains: the largest radius is \(0.0068\)$0.0068$ and the smallest \(0.00065\)$0.00065$, and each was chosen to fit its captured domain with almost no slack. All radii lie within the working box \(|h_j|\le1/64\)$|h_j|\le 1/64$, the region over which the curvature constants of Appendix B were bounded.

The local theorem excludes any nonzero displacement in this rectangle that remains feasible in the fixed-\(T\)$T$ container. Its mechanism is quantitative: the linear gap constraints obstruct motion, and an exact bound on their curvature proves that the nonlinear terms cannot overcome that obstruction anywhere in the rectangle.

Write \(\tau\)$\tau$ for the largest displacement as a fraction of its allowed coordinate radius. A nonzero displacement has \(0<\tau\le1\)$0<\tau \le 1$. The certificate for a coordinate attaining that maximum forces \(\tau\le c_j\tau^2\)$\tau \le c_j{\tau }^2$, with \(c_j<1\)$c_j<1$. This is impossible: throughout that interval, \(c_j\tau^2<\tau\)$c_j{\tau }^2<\tau$.

Covering all possible local contact patterns

Nearby squares can change which edges separate them, so the proof must consider more than one contact pattern. The construction has fourteen contacting pairs. A separation feature of a pair chooses which square supplies the axis, one of its two edge-normal directions, and which square lies on the positive side; the pair is separated by the feature when all four corners of the other square satisfy the corresponding projection inequality. Written out, with \(g_{f,k}\)$g_{f,k}$ the gap of corner \(k\)$k$ under feature \(f\)$f$, the pair has disjoint interiors exactly when

a disjunction over features of a conjunction over corners. Each pair has eight features, 112 altogether. A feature is available when its conjunction holds at the construction; exact signs show 24 available and 88 unavailable, each of the 88 having a corner with a strictly negative gap, which disables the whole feature.⁷ Taylor bounds prove that those 88 remain unavailable throughout the full rectangle.

A feasible perturbation separates each contacting pair by one of its available features, so the check enumerates the 512 combinations of available features. Coincident corners in the two pairs of axis-aligned squares that meet along a full edge give identical inequalities, which leaves 128 distinct linear systems, the contact branches. A contact branch keeps only the inequalities that are tied at the construction, those whose gap is exactly zero there: 22 corner inequalities from the chosen features and 20 wall inequalities, 42 in all. Omitting the constraints of pairs that do not touch at the construction, and the inequalities with positive gap, weakens this necessary system; it cannot discard a feasible packing. No new contact can form inside the rectangle in any case: the 41 non-contacting pairs keep a clearance of at least \(0.015\)$0.015$ throughout it.⁶ Conversely, every feasible perturbation must select one of the checked contact branches.¹⁶

From a linear obstruction to a finite neighborhood

Let \(g_i(h)\)$g_i(h)$ be a gap that must be nonnegative in a chosen contact branch, with \(g_i(0)=0\)$g_i(0)=0$. Write its linear part as \(A_i h\)$A_{i}h$. A linear calculation alone would describe only infinitesimal motion. To control an actual displacement, the proof bounds the quadratic remainder.

Normalize the size of a hypothetical nonzero displacement by

The checked curvature bounds \(K_i\)$K_i$ give the necessary inequalities

Choose a coordinate \(j\)$j$ attaining \(|h_j|=\tau r_j\)$|h_j|=\tau r_j$, and choose the sign \(\sigma\)$\sigma$ opposite to \(h_j\)$h_j$. A certificate supplies nonnegative rational weights \(\lambda_i\)${\lambda }_i$, and the weighted combination of the gap rows nearly isolates that coordinate: write

where \(e_j\)$e_j$ selects coordinate \(j\)$j$. Multiplying the gap inequalities by the weights and using \(|h_k|\le\tau r_k\)$|h_k|\le \tau r_k$ gives

A certificate with

therefore leaves no \(\tau\)$\tau$ in \((0,1]\)$(0,1]$: dividing by \(\tau\)$\tau$ and using \(\tau\le1\)$\tau \le 1$ would give \(r_j\le\eta+M_j/2\)$r_j\le \eta +M_j/2$. The checker bounds the residual more coarsely, by \(\|e\|_1\le\epsilon_j\)$\Vert e{\Vert }_1\le {ϵ}_j$ with \(R=\max_k r_k\)$R={max}_k{r}_k$, so that \(\eta\le\epsilon_jR\)$\eta \le {ϵ}_{j}R$, and verifies for every one of the \(128\times33\times2=8,448\)$128\times 33\times 2=8,448$ certificates the strict margin

which is the same conclusion in the form \(\tau\le c_j\tau^2\)$\tau \le c_j{\tau }^2$ with \(c_j=M_j/(2(r_j-\epsilon_jR))<1\)$c_j=M_j/(2(r_j-{ϵ}_{j}R))<1$, the form Figure 11 draws. The largest certified \(c_j\)$c_j$ is approximately \(0.676505208\)$0.676505208$; the proof uses exact strict comparisons, not this rounded display value, and the two ratios \((\eta+M_j/2)/r_j\)$(\eta +M_j/2)/r_j$ and \(c_j\)$c_j$ are different numbers.⁷

Local-isolation lemma. The zero perturbation is the only feasible packing in the declared labeled rectangle inside the fixed container \([0,T]^2\)$[0,T{]}^2$. The quadratic bounds make this a theorem about a finite neighborhood, including its boundary. Appendix B describes the curvature and negative-feature checks.

Closing the Gap Between the Rational Cap and the Exact Optimum

The global geometry was computed at \(U>T\)$U>T$, while isolation holds at the exact side \(T\)$T$. The conclusion needs a precise connection between the two frames.

Start from a hypothetical packing \(P\)$P$ in a square of side \(L_0<T\)$L_0<T$, centered in the cap. The symmetry lemma supplies a symmetry \(g\)$g$ of the square for which \(g(P)\)$g(P)$ admits case 438; because \(g\)$g$ fixes the cap’s center, \(g(P)\)$g(P)$ still lies in the concentric side-\(L_0\)$L_0$ container, and its squares are unchanged. Case 438 is the pattern of the quarter-turned construction, so let \(\operatorname{rot}(x,y)=(-y,x)\)$rot(x,y)=(-y,x)$ be that quarter-turn and undo it. In physical coordinates, the local center corresponding to a captured center \(p\)$p$ is

the certificate files store \(p_f=(191/50)\,p/U\)$p_f=(191/50)p/U$, so the checker first multiplies by \(U/(191/50)\)$U/(191/50)$. This is a rigid rotation and translation, and a quarter-turn leaves every orientation unchanged modulo \(\pi/2\)$\pi /2$, so the captured angle rows carry over unchanged. The side-\(L_0\)$L_0$ container centered inside \(U\)$U$ becomes

Its small squares are still unit squares. The complete capture and inclusion checks place their labeled poses in the local rectangle, and they are feasible in the fixed-\(T\)$T$ container. The local-isolation lemma forces them to be the exact construction. But that construction spans \(T\)$T$, so it cannot lie in a square of side \(L_0<T\)$L_0<T$. This contradiction excludes every smaller side directly. Together with the exact witness, it proves \(s(11)=T\)$s(11)=T$.¹⁷

This deduction does not rule out perturbations in the larger cap \(U\)$U$. It needs only the impossibility of a smaller packing. The same premises apply when \(L_0=T\)$L_0=T$: a packing of side exactly \(T\)$T$ also enters the cap, the symmetry lemma, capture and inclusion, and the local theorem then makes its aligned image the construction. So, on the same complete exclusion and capture ensemble, every optimal packing is the construction up to the eight symmetries of the container and relabeling of the squares.⁷ The Squares Project registers this corollary separately as T-112. It rests on T-060’s evidence and adds no computation; its one new step, that each premise is stated for a side at most \(T\)$T$, is prose. Trump called his packing rigid, meaning that no square can move; that is a local property, and no earlier source found states that the optimum is unique. Uniqueness is not automatic at a solved count: Stromquist gives three different optimal packings of ten squares.¹⁸

What Was Verified, and What the Verification Means

The public proof source is Queuingtheorydotcom/11SquaresOptimal, linked at the revision that was confirmed. The Squares Project’s confirmation uses independently written consumers of its proposed certificate data and a mathematical review of the implications above. The accepted computation covers the required proof ensemble, including all 2,180 exclusions and all ten capture nodes.¹⁹

Search programs may choose promising cuts, cores or dual weights. They need not be trusted to find correct ones: a certificate checker recomputes the finite conditions that make each proposal sound. The review must still establish why those conditions imply the continuous geometric claim. Reexecution tests reproducibility; it does not, by itself, prove that a checker implements a sound mathematical rule.

The independence has limits. The local construction, derivative calculations and exact arithmetic include shared first-party primitives. The confirmation follows the same mathematical argument, rather than supplying a distinct proof method. The Squares Project therefore records the result as T-060, S5/V3/C3, rungs on the significance, verification and confirmation axes of its epistemics guide: significance 5, movement on a central open case, with a machine certificate replayed here and its review record pending on both the verification and the confirmation axes. Under the ladder of 2026-09-30, rung 4 on either axis also needs a second adversarial review by a distinct reviewer and a retained human oversight record; the reviews linked from this paper that record V4/C5 were written under the ladder in force before that date. Neither distinct-method confirmation nor proof-assistant formalization is claimed. The trust base includes the reviewed mathematical reductions, checker source, arithmetic libraries, runtime and executing system.

Lean 4 formalizations of the proof are in progress elsewhere, in wand125/n11-optimality-lean and Queuingtheorydotcom/11SquaresFormalized. wand125 reports that the 76 prior-family cases and the 173 returned cases are already kernel-checked using only Lean’s standard axioms; an independent replay of the 173 against the 11SquaresFormalized assembly is recorded in an open pull request to that repository, not merged as of October 4.¹³ On October 6 Queuingtheorydotcom reported the formalization in 11SquaresFormalized complete: 7,920 Lean modules with no admitted goal, its numerical certificates checked by native_decide, so that it trusts Lean’s compiler as well as its kernel.²⁰ The Squares Project’s statement audit of October 6 reads its theorem, ElevenSquare.optimality, as exactly \(s(11)=T\)$s(11)=T$; the full run is private, so T-060 records it as the source’s report, and no rung rests on either formalization.

The final composition receipt reconciles the completed geometric executions and their reviewed dependencies. It does not rerun those calculations. Four stale final-state digest bindings in the publisher’s packet prevented accepting its unchanged full runner as a successful replay; the independent confirmation uses freshly observed component executions and checked state joins instead. A fresh one-command rerun of the entire independent ensemble still needs a reviewed way to rebind newly generated parent receipts, whose timing fields change their bytes. That automation issue is tracked separately from the completed mathematical obligations.²¹

The composer reads its receipts by hash, and each receipt names its inputs by hash, so a reader can verify at three depths: that every retained object still decodes to its hash; that the composition’s joins agree over the retained executions, which takes seconds; or that a component’s geometry recomputes afresh from the retained inputs, for which the validation guide gives one portable command per checker. The packet also keeps the ancestry each accepted receipt cites as its input, the controls that measure what a partial or refused run reports, and the superseded attempts beside their replacements, so the record says why each accepted run exists; the receipts register states the purpose of every one and who reads it.

The two adversarial reviews of October 3 added four checked components that stand beside the accepted ones rather than in their place: a corrected closed-interval kernel for new callers; the incidence propagation that shortens the symmetry lemma; the two-radius local box; and the selection of 44 of the 46 accepted field certificates whose union already excludes every case the field certificates exclude, a reading aid and a replay shortcut rather than a deletion. Each has its own receipt or manifest and its own tests. None is a premise of the composed proof, and none changes a frozen checker or an accepted receipt.

The T-060 validation guide separates fast checks of retained evidence from fresh geometric replay, and links each checker, source binding and recorded execution. It is the place to reproduce a component; merely rerunning the final composer is not an independent end-to-end proof run.

Appendix A: Exact Placement Formulas

For a direct construction, let \(A(a,b)=[a,a+1]\times[b,b+1]\)$A(a,b)=[a,a+1]\times [b,b+1]$, and define

The six axis-aligned squares are

Define the rigid map

The remaining five squares are the images under \(F\)$F$ of

All quantities are elements of \(\mathbb Q(u)\)$\mathbb{Q}(u)$. These formulas, together with the isolated root, specify the construction without relying on coordinates read from a drawing.⁵

The squares, numbered as above, correspond to the cells that case 438 assigns their quarter-turned images; the inclusion check and the local theorem use this correspondence.

Appendix B: The Nonlinear Estimates

For a pair gap, let square \(o\)$o$ supply the separating axis and square \(p\)$p$ supply the tested corner. Put \(w_i=r_{3i+2}\)$w_i=r_{3i+2}$ for square \(i\)$i$’s angular radius. A bound on the second derivative along any direction in the coordinate rectangle is

Here \(D_{op}\)$D_{op}$ bounds center separation throughout the working box. The terms bound the rotation of the center projection, the mixed translation–rotation derivative and the relative rotation of the corner. A wall gap has \(K=w_i^2/\sqrt2\)$K=w_i^2/\sqrt{2}$. Checked rational upper bounds replace the square roots. When several elementary gap functions share one gradient, the checker uses the largest applicable curvature bound.

An unavailable separation feature has a corner gap \(g\)$g$ with \(g(0)<0\)$g(0)<0$. The checker establishes

Taylor’s theorem then keeps that corner gap negative throughout the closed rectangle. The feature cannot become available there. These 88 exclusions, the exhaustive remaining feature choices, and the curvature-weighted dual inequalities supply the nonlinear premises of local isolation.¹⁶

Appendix C: Retained Data of the Local Rectangle and the Cover

The 33 radii of the local rectangle, as the accepted inclusion and isolation receipts bind them, by construction square: \(r_x\)$r_x$ and \(r_y\)$r_y$ in units of the small square’s side and \(r_\theta\)$r_{\theta }$ in radians.

The sixteen sites of the center cover, in normalized coordinates: each pair of integers is divided by \(2{,}000{,}000\)$2,000,000$, and site \(15-i\)$15-i$ is \((1,1)\)$(1,1)$ minus site \(i\)$i$.

A box with two radii isolates the construction as well, and more simply: \(1/256\)$1/256$ for every coordinate except the angles of squares 9 and 10, which get \(1/128\)$1/128$. Every accepted radius is at most its replacement, the tightest being square 6’s angle at \(0.904\)$0.904$ of \(1/256\)$1/256$, so the accepted pose inclusion places the captured poses in this box too. Over it the quadratic remainders of the gap functions have six curvature bounds of the form \(K/r^2\)$K/r^2$: \(21/2\)$21/2$, \(57/4\)$57/4$, \(99/4\)$99/4$ and \(30\)$30$ for a contacting pair, by the two squares’ multiplicities, and \(3/4\)$3/4$ and \(3\)$3$ for a wall contact. Run with the repository’s finer curvature bounds, the accepted dual weights and the same 128 contact branches, the isolation checker accepts this box with worst ratio \(0.8667\)$0.8667$ over its 8,448 signed-coordinate margins, against \(0.6765\)$0.6765$ for the fitted radii; the review’s six constants alone give \(0.9515\)$0.9515$. The result is retained as a checked component beside the accepted one; the proof’s rectangle remains the fitted one.⁷

Sources and Verification Record

The simplification review freezes the dependency map used in this exposition. It consolidates repeated geometric rules and the endpoint argument without claiming fewer necessary cases, rounds or branches. The figures are explanatory renderings of retained data; their rounded screen coordinates are not inputs to certificate acceptance. Two adversarial reviews of October 3, 2026, the project’s own and GPT-6 Pro’s, recomputed the paper’s numbers independently and found no mathematical error; the integration record dispositions every finding of the second, and the retained components it added stand beside the accepted ones rather than in their place.

Version History

• v0.1.6 — October 6, 2026. The uniqueness corollary is registered as T-112 and no longer called unreviewed, with its prior art: Trump's rigidity claim is local, and Stromquist's three optimal packings of ten squares show uniqueness is not automatic; and Queuingtheorydotcom's report of a complete Lean 4 formalization of October 6 is cited, with its native-compiler trust base and the project's statement audit.
• v0.1.5 — October 5, 2026. The series revision: the paper is Part III of three, its lineage names Part II's three changes from T-026 and draws the series bound ladder as Figure 3, Charge Budgets contrasts capacity one with \(\lfloor m/k\rfloor\)$\lfloor m/k\rfloor$, a test holds every term to a definition before its first use, and the notation follows the series: \(L_0\)$L_0$, \(\Gamma_i\)${\Gamma }_i$, \(\operatorname{rot}\)$rot$, \(\mathbf{D}_4\)${𝐃}_4$ and \((191/50)/U\)$(191/50)/U$.
• v0.1.4 — October 4, 2026. wand125's comment of October 4 is answered: the in-progress Lean 4 formalizations are named, with their status as wand125 reports it; the root node completes thirteen further updates, not fourteen; Figure 8 and the text agree that the symmetry lemma rests on the exhaustive search; and the 1,931-case premise of cases 2175 and 2176 is stated as a premise of their accepted certificates, beside wand125's report of a Lean proof of all 76 prior-family cases that does not use it.
• v0.1.3 — October 3, 2026. The closing section explains what a receipt is, the three depths at which a reader can verify the retained evidence, and the four checked components the reviews of October 3 added beside the accepted ones; the receipts register is linked.
• v0.1.2 — October 3, 2026. The second reviewed revision: GPT-6 Pro's unified adversarial review of October 3 is applied. The invariant is stated row by row with ownership quantified over valid packings, the field citation names the original's §12 and a worked mask-0 certificate, the separation features are written as a disjunction of conjunctions, the isolation lemma carries the weighted residual, the five-site charge gains its ten-hull form, the root is certified unique on its interval, the uniqueness corollary is stated conditionally, and the frames, roles, radii and cover sites are tabulated.
• v0.1.1 — October 3, 2026. The reviewed revision: the adversarial review of October 3 is applied, every term is defined before its first use, the transfer rule states the half-turn, the final deduction names the symmetry image, and the paper explains the tilt \(u=\tan(a/2)\)$u=\tan (a/2)$, the polynomial as one contact and the four survivors as the construction under the eight symmetries.
• v0.1.0 — September 30, 2026. The first edition: the explainer of T-060's proof, with its figures.

The Squares Project · github.com/jlevy/squaresFormatted and typeset with Flowmark and KPress