The Problem

The Problem

A packing of $n$$n$ unit squares in a container square of side $s$$s$ is a placement of the $n$$n$ squares, each free to translate and rotate, whose interiors are pairwise disjoint and which all lie inside the container. $s(n)$$s(n)$ is the infimum of the $s$$s$ for which one exists. Touching is allowed, and in good packings it is pervasive.

For most $n$$n$ the answer is uninteresting: s(m2)=m$s(m^2)=m$ by the grid. It becomes interesting just above a perfect square, where the leftovers must be tilted in.

At $n=11$$n=11$ Walter Trump’s 1979 construction still supplies the exact upper bound. T-060’s independently audited global proof supplies the matching lower bound. The earlier lower-bound program passed Stromquist’s bound on 2026-09-04:

The exact optimum: a certified degree-8 construction with a matching global lower bound. The segment and dot contact marks are exact, not tolerance-based visual guesses.

The value T-018 displaces is Stromquist’s 2+4/5​=3.788854382…$2+4/\sqrt{5}=3.788854382\dots$, stated in Memo III, p. 10 on November 15, 1984, and published in 2003. The memo states the unrestricted bound without supplying its proof. The memo review records the source distinctions and the helper-argument followup. The current audit found an explicit strict box avoiding all twelve printed Figure 14 points, so the paper’s unavoidability subclaim is false as printed (D-152). Exp-017 independently certifies the same numerical inequality by moving only $G=(.8,1.85)$$G=(\mathrm{.8},1.85)$ to the source-distinct G′=(.79,1.85)$G^{\prime }=(\mathrm{.79},1.85)$ and replaying the complete finite cover and capacity argument (T-010). The repaired coordinate and certificate are results of this repository, not claims attributed to Stromquist.

Trump’s packing is six axis-aligned squares plus a block of five tilted at a∗≈40.181937290329714∘$a^{*}\approx {40.181937290329714}^{\circ }$. The container side is an algebraic number of degree 8, the root of

s⁸ − 20s⁷ + 178s⁶ − 842s⁵ + 1923s⁴ − 496s³ − 6754s² + 12420s − 6865 = 0

lying in $[3.87,3.88]$$[3.87,3.88]$. Exp-013 exactly certifies every complete branchwise fixed-side linearized cone and proves the pose locally isolated by a finite-branch subsequence argument. This qualitative local theorem does not provide an explicit radius or explain the global search difficulty.

Why exactness is not optional

Disjoint interiors means touching is legal, and record packings touch a great deal. In Trump’s packing 14 of the 55 pairs are separated by exactly zero, and 20 corner coordinates lie exactly on the container boundary.

Floating-point evaluation can certify a strict inequality when a sound error bound stays away from zero. It cannot infer that an unrecognised near-contact is exactly equal to zero merely because a computed residual is small. A tolerance-based f64 verifier therefore needs a tolerance to accept Trump’s rounded algebraic contacts, and that tolerance is a blind spot that also accepts overlaps smaller than itself; setting it to zero rejects this true packing instead. Both failure modes are demonstrated by cases.trump11.verifier_limits.

The fix is representational rather than numerical: express the configuration in the real algebraic number field it actually lives in, where equality is decidable. That is what the exact sqpack path does. A rigorous outward-rounded interval certificate can also be formal; a finite point evaluation cannot. This is why the campaign permits beat_record: true only under verified assurance.

This is not an abstract concern. The same failure reappeared inside the refiner eight rounds later: an LP solver at its default tolerance returned a packing violating its own separation constraint, and so a side below Trump’s (D-014, critical, caught by the pre-registered rule that beating the record means you have a bug).