A Review of the Certified Lower Bound \(s(11) > 31/8\)$s(11)>31/8$ for 11 Squares

This paper explains the computer-assisted proof of a lower bound of 31/8 for eleven unit squares, published by Kleddamag in 11-squares-certified-bound: the proof, certificate and reproduction at the reviewed release, v1.0.2, retained in this project’s archive. The source’s AUTHORS.md says OpenAI Codex developed the mathematics and computation under Kleddamag’s direction; the certificate develops this project’s T-026 certificate, the subject of Part I, and the result is registered here as T-037.¹

The Result

A unit square is a square of side one, placed anywhere in the plane at any angle. A packing of unit squares in a container, a larger square with sides parallel to the axes, is a placement in which every unit square lies inside the container and no two unit squares have a common interior point; their boundaries may touch. Write \(s(11)\)$s(11)$ for the smallest container side that admits a packing of eleven unit squares, and \(L_0\)$L_0$ for the side of a container under test, both as Part I does; the Attainment lemma shows that a smallest side exists. A square is unchanged by a quarter-turn, so its angle is only defined modulo \(\pi/2\)$\pi /2$, and this paper takes every angle in \([0,\pi/2)\)$[0,\pi /2)$.

Theorem. \(s(11)>31/8=3.875\)$s(11)>31/8=3.875$: no packing of eleven unit squares fits in a container of side \(31/8\)$31/8$, and so none fits in any smaller container.²

The method is Part I’s: weighted positions in the container, arranged so that a small square placed anywhere must enclose at least a fixed amount of weight while the total available is less than eleven times that amount, so eleven squares with disjoint interiors cannot all be paid. The source changes three things:

1. five-site k-of-m charges: charges of the kinds 2-of-5 and 3-of-5 beside Part I’s 2-of-3, each paying a core that holds at least \(k\)$k$ of its \(m\)$m$ sites (defined in From Points to k-of-m Charges);
2. k-of-m charges on shrunken parents with strict cores: the squares are shrunk to side \(A=764/775\)$A=764/775$ in a container of side \(191/50\)$191/50$, each with a core strictly inside it, defined in Parents and the One Inequality;
3. a reoptimized certificate over 12,028 adaptive angle rows, each with its own core, replacing T-026’s net, Part I’s finite list of core directions (defined in Parents, Cores and the Angle Catalogue).

The proof gives no better packing and does not find the exact minimum. Write \(T=3.8770835900\ldots\)$T=3.8770835900\dots$ for the side of Walter Trump’s packing of 1979, the best packing known; the bound gap, the distance between the best upper and lower bounds, was \(0.0020836\)$0.0020836$ after this proof.³ The result was superseded within a week: on 2026-09-29 Ke Wang and Can Li reweighted and scaled this same certificate to \(s(11)>3875000000/999999999\)$s(11)>3875000000/999999999$, a step of about \(3.9\times10^{-9}\)$3.9\times {10}^{-9}$ (T-061), and Queuingtheorydotcom proved \(s(11)=T\)$s(11)=T$ by different machinery (T-060), which Part III reviews. With T-061’s reweighting of it, it is the furthest the charge method reached, and Part III’s field certificates, which also charge cores, are easiest to follow against it.

From Points to k-of-m Charges

A site is a position in the container, and a point charge, which Part I calls an atom, is a site with a nonnegative weight.⁴ A core is a closed square strictly inside a packed square, and a core captures a site when the site lies in the core. The total weight of the point charges a core \(Q\)$Q$ captures is what Part I calls its mass \(\mu(Q)\)$\mu (Q)$. Part I’s Conditions 1 to 5 say that the point charges are symmetric under the container’s symmetries, that their total is below eleven, that a finite net of directions reaches \(\pi/4\)$\pi /4$, that the core is small enough to fit at every angle between net directions, and that every core at every net direction captures mass at least one.

A k-of-m charge \((S,k,w)\)$(S,k,w)$ is Part I’s threshold atom under the series’ name: a set \(S\)$S$ of \(m=|S|\)$m=|S|$ distinct sites, an integer threshold \(1\le k\le m\)$1\le k\le m$, and a nonnegative weight \(w\)$w$; it pays \(w\)$w$ to a core that captures at least \(k\)$k$ sites of \(S\)$S$, and nothing otherwise. Part I defines it for any \(k\)$k$ and \(m\)$m$, and its certificates use only 2-of-3. A point charge is the case \(m=k=1\)$m=k=1$. The charge \(C(Q)\)$C(Q)$ of a core \(Q\)$Q$ is the sum over all point and \(k\)$k$-of-\(m\)$m$ charges of what each pays it; for point charges alone it is the mass.⁵ The charge at index 72 of the source’s list, the heaviest in the certificate, is a 3-of-5 charge of weight 0.067038144 on the five sites (1.1938, 1.7190), (1.0314, 1.5280), (0.9858, 1.4579), (0.4584, 1.4898), (0.4966, 1.4898), rounded here from their exact coordinates: a core that captures any three of them is paid the whole weight, and one that captures two is paid nothing.

Budget lemma. Let \(r\)$r$ pairwise disjoint cores each capture at least \(k\)$k$ sites of a \(k\)$k$-of-\(m\)$m$ charge. The captured subsets are disjoint, so together they hold at least \(rk\)$rk$ distinct sites of \(S\)$S$, and \(rk\le m\)$rk\le m$. The charge therefore pays at most \(\lfloor m/k\rfloor\)$\lfloor m/k\rfloor$ of any family of pairwise disjoint cores, and at most \(w\lfloor m/k\rfloor\)$w\lfloor m/k\rfloor$ in total, its budget.⁵

Part I leaves two consequences of the lemma implicit. First, the inequalities add when charges share sites: each one is valid on its own, so the total paid to any family of disjoint cores is at most the sum of the budgets, with no requirement that the charges have disjoint supports. Second, the 2-of-5 charge has \(\lfloor 5/2\rfloor=2\)$\lfloor 5/2\rfloor =2$: it is the first family in the series’ certificates that can pay two disjoint cores, and its budget is \(2w\)$2w$. The 2-of-3 and 3-of-5 charges have budget \(w\)$w$.

Why k-of-m charges pay. Suppose one wants every core that captures \(k\)$k$ of the \(m\)$m$ sites to be guaranteed \(w\)$w$. Point weights of \(w/k\)$w/k$ at the \(m\)$m$ sites do it, at a budget of \(mw/k\)$mw/k$; the \(k\)$k$-of-\(m\)$m$ charge does it at a budget of \(\lfloor m/k\rfloor w\)$\lfloor m/k\rfloor w$. The ratio of the two prices is \(3/2\)$3/2$ for 2-of-3, \(5/3\)$5/3$ for 3-of-5 and \(5/4\)$5/4$ for 2-of-5. When \(k\)$k$ divides \(m\)$m$ there is no saving: a 2-of-4 charge costs \(2w\)$2w$ either way, which is why this project’s threshold code notes that only the families with \(k\)$k$ not dividing \(m\)$m$ add anything.⁶ The price of the saving is that a core capturing fewer than \(k\)$k$ sites is paid nothing, where the point weights would have paid it something.

Single points carry 79% of T-026’s budget and 20% of T-037’s. There is also a reason the points could not have done it alone: T-025’s exact ceiling family shows that no point measure of mass below eleven with the container’s full symmetry exists at the side \(191/50\)$191/50$ on T-025’s core domain, so no point certificate of Part I’s form on that domain reaches even \(3.82\)$3.82$.³

What Is New, and What It Inherits

Three labels sort the proof’s ingredients. An ingredient is inherited when a registered or cited antecedent has the idea; it is new data when it is the source’s instance of an inherited idea, chosen afresh; and it is new when no antecedent is registered. The source’s own attribution claims no invention of the weighted-covering or threshold-counting methods.⁷

The inventory:

• The general \(k\)$k$-of-\(m\)$m$ charge and its budget \(w\lfloor m/k\rfloor\)$w\lfloor m/k\rfloor$ are inherited from Part I, where T-025 states them as the general threshold atom and uses the case 2-of-3; T-025’s proof sums the budgets over all atoms, shared sites included, without remarking on it, and the source states the rule.⁷
• The signed inclusion–exclusion of a \(k\)$k$-of-\(m\)$m$ indicator into rectangle terms, and the integer difference sweep that evaluates it, are T-025’s; the source’s coefficients are the same.⁷
• 2-of-3 charges beside point charges over contiguous intervals of parent angles are inherited from Kleddamag’s own proof for seventeen squares (T-038); point charges over such intervals are older (next item), and T-037 is the first certificate of that form at eleven squares.³
• The shrunken parent of side \(A<1\)$A<1$, the bound \(L_0/A\)$L_0/A$, one closed core per angle interval, and coverage required only over the centers a parent may legally occupy are inherited through the Levy/Guzhou0806/Mira line of parent certificates; the first registered certificate of that form is Guzhou0806’s R012 (T-032, 2026-09-20).⁸
• New: 2-of-5 and 3-of-5 charges in a retained certificate. The families are named in this project’s threshold code, and a study of 2026-09-10 weighed five-site charges, but no earlier registered certificate uses them: T-025, T-026 and T-038 are 2-of-3 only, and the next, R052’s 3-of-5 at seventeen squares (T-039), is dated 2026-09-25.⁷
• New data: the certificate reoptimized from T-026’s, with sites rounded and added, families added, weights reoptimized, and the catalogue replaced.⁷
• New: the bound \(31/8\)$31/8$ itself, strict by attainment.²
• Not claimed: external review, priority, or how the certificate was found.²

The audit notes that the certificate changes several ingredients at once, with no ablation that attributes the gain to any one of them.⁹

Parents and the One Inequality

A parent is a square of side \(A=764/775\)$A=764/775$ inside the container \([0,L_0]^2\)$[0,L_0{]}^2$, whose side is \(L_0=191/50\)$L_0=191/50$. Parents may rotate independently and touch; their interiors must be disjoint.¹⁰

Scaling lemma. Eleven parents fit in a container of side \(L_0\)$L_0$ exactly when eleven unit squares fit in a container of side \(L_0/A\)$L_0/A$, and

because \(764=4\cdot191\)$764=4·191$ and \(775=31\cdot25\)$775=31·25$. Scaling a packing by \(1/A\)$1/A$ about the container’s corner sends parents to unit squares and preserves containment and disjoint interiors, and scaling by \(A\)$A$ sends them back.¹⁰

This is Part I’s rational dilation read the other way: Part I scales the certificate up by \(q\)$q$ and leaves the squares at side one; here the squares are scaled down to side \(A\)$A$ and the certificate stays at \(191/50\)$191/50$.

Every parent is given an assigned core, a closed square strictly inside it whose side and angle depend only on the parent’s angle; how is the subject of Parents, Cores and the Angle Catalogue. \(\Gamma\)$\Gamma$ is the least charge of any assigned core of any parent anywhere in the container, and \(M\)$M$ is the sum of the budgets of all the charges. Eleven parents with disjoint interiors hold eleven pairwise disjoint assigned cores, each of charge at least \(\Gamma\)$\Gamma$, so the cores collect at least \(11\Gamma\)$11\Gamma$; by the Budget lemma, summed over all charges, they collect at most \(M\)$M$. If \(11\Gamma>M\)$11\Gamma >M$, there is no packing of eleven parents, and by the Scaling lemma no packing of eleven unit squares in side \(31/8\)$31/8$.¹¹

The certificate has \(\Gamma=0.999962528\)$\Gamma =0.999962528$ and \(M=10.999479944\)$M=10.999479944$, so \(11\Gamma=10.999587808>M\)$11\Gamma =10.999587808>M$, a surplus of 107,864 units of \(10^{-9}\)${10}^{-9}$. Neither number is normalized: \(\Gamma\)$\Gamma$ is a little below one and \(M\)$M$ a little below eleven, their ratio \(M/\Gamma\)$M/\Gamma$ about 10.99989, and the inequality, not either value alone, is what is checked.

The Certificate’s Charges

The container has eight symmetries, the four rotations and four reflections of the square, which form the group \(\mathbf{D}_4\)${𝐃}_4$ of Part I’s Condition 1. The orbit of a site is the set of its images under the eight symmetries, of size one, four or eight, and the orbit of a \(k\)$k$-of-\(m\)$m$ charge is the set of its images under the eight symmetries, eight or fewer. A certificate is \(\mathbf{D}_4\)${𝐃}_4$-invariant when every point charge and every \(k\)$k$-of-\(m\)$m$ charge appears with its whole orbit at equal weights. The source file lists one site per site orbit and, for each charge orbit, every image set under one weight; both checkers rebuild each orbit from its first member and confirm that the listed images are exactly those.¹²

The certificate’s 679 site orbits expand to 5,284 distinct sites. Point weight is positive on 66 orbits, 496 sites; 144 of those also belong to \(k\)$k$-of-\(m\)$m$ charges, and the other 4,788 sites belong to \(k\)$k$-of-\(m\)$m$ charges only, so 4,932 sites are in some \(k\)$k$-of-\(m\)$m$ charge and none is unused.¹²

Point weight concentrates where a parent’s inner edge can lie. An axis-aligned parent touching a wall has its inner edge on one of the four lines \(x=A\)$x=A$, \(x=L_0-A\)$x=L_0-A$, \(y=A\)$y=A$ or \(y=L_0-A\)$y=L_0-A$. Of the 66 point orbits, 22 lie within \(0.005\)$0.005$ of one of those lines and carry 58% of the point weight; 78% of it lies within \(0.05\)$0.05$. The largest point weight, 0.026140599, sits at (0.9596, 0.9858), within \(10^{-5}\)${10}^{-5}$ of the line \(y=A\)$y=A$ and \(0.026\)$0.026$ short of the corner \((A,A)\)$(A,A)$ where two of the lines cross.¹²

The families, as the source tabulates them and the audit recomputed them; each image of a charge orbit, which the source calls a physical feature, counts as one charge:¹²

Parents, Cores and the Angle Catalogue

Angles are kept in half-angle coordinates. For an angle \(\theta\)$\theta$, write \(t=\tan(\theta/2)\)$t=\tan (\theta /2)$; then

so a rational \(t\)$t$ gives a rational cosine and sine, and every comparison the checkers make is between rational numbers. A parent’s angle is written \(\varphi\)$\phi$, as Part I writes a packed square’s, and its half-tangent \(\tan(\varphi/2)\)$\tan (\phi /2)$ ranges over \([0,1)\)$[0,1)$ as \(\varphi\)$\phi$ ranges over \([0,\pi/2)\)$[0,\pi /2)$.¹³

Folding lemma. Every parent may be assumed to have angle in \([0,\pi/4]\)$[0,\pi /4]$, one parent at a time, without assuming anything about the packing. Part I’s contradiction argument proves this for unit squares: a square whose angle lies past \(\pi/4\)$\pi /4$ is reflected across the container’s diagonal, which is one of the eight symmetries; the image is a square in the container with angle in \([0,\pi/4]\)$[0,\pi /4]$; its core is chosen there and reflected back; and because the certificate is \(\mathbf{D}_4\)${𝐃}_4$-invariant the reflected core captures a site exactly when the original captures the site’s image, so its charge is unchanged. Here the same reflection is applied to a parent, and the core it brings back is a closed square strictly inside the original parent, because reflection preserves containment. Two parents may be folded by different symmetries. The source states this in one sentence.¹⁴

A row \((a,b,t,B)\)$(a,b,t,B)$ is a closed interval \([a,b]\)$[a,b]$ of parent half-tangents together with a core half-tangent \(t\in[0,1)\)$t\in [0,1)$ and a core side \(0<B<A\)$0<B<A$: every parent with \(\tan(\varphi/2)\in[a,b]\)$\tan (\phi /2)\in [a,b]$ is assigned the concentric closed core of side \(B\)$B$ at angle \(2\arctan t\)$2\arctan t$. The catalogue is the certificate’s list of 12,028 rows, contiguous from \(0\)$0$ to \(207107/500000\)$207107/500000$. The last endpoint \(b\)$b$ satisfies \(b^2+2b-1=309449/(2.5\times10^{11})>0\)$b^2+2b-1=309449/(2.5\times {10}^{11})>0$, so it lies past \(\tan(\pi/8)=\sqrt2-1\)$\tan (\pi /8)=\sqrt{2}-1$ and the rows cover every folded angle. Row widths run from \(3.6\times10^{-9}\)$3.6\times {10}^{-9}$ to \(4.8\times10^{-4}\)$4.8\times {10}^{-4}$, and \(B\)$B$ from 0.98537 to 0.98581; the two cores of Figure 4 are row 6600’s.¹³

The mismatch \(d\)$d$ between a parent and its core is the angle \(\varphi-2\arctan t\)$\phi -2\arctan t$. A concentric square of side \(B\)$B$ at angle \(d\)$d$ to a square of side \(A\)$A$ lies strictly inside it exactly when

since \(B(\cos d+|\sin d|)\)$B(\cos d+|\sin d|)$ is the width of the tilted square’s projection on the parent’s axes. Part I meets the same expression as \(B(\cos d+\sin d)<1\)$B(\cos d+\sin d)<1$ under its Condition 4.

Strict-core lemma. For every row and every parent angle \(\varphi\)$\phi$ with \(\tan(\varphi/2)\in[a,b]\)$\tan (\phi /2)\in [a,b]$, \(B(\cos d+|\sin d|)<A\)$B(\cos d+|\sin d|)<A$: every assigned core lies strictly inside its parent. The checker evaluates \(\cos d\)$\cos d$ and \(|\sin d|\)$|\sin d|$ at the two endpoint angles \(2\arctan a\)$2\arctan a$ and \(2\arctan b\)$2\arctan b$ as rational dot and cross products of the parent’s and the core’s direction vectors, and checks three things: that \(\cos d>0\)$\cos d>0$ and \(\cos d\ge|\sin d|\)$\cos d\ge |\sin d|$ at both endpoints, which puts \(d\)$d$ in \([-\pi/4,\pi/4]\)$[-\pi /4,\pi /4]$ there; and that the inequality holds at both. The endpoint checks suffice for the whole row. Since \(2\arctan\)$2\arctan$ is increasing, \(d\)$d$ is a monotone function of the parent’s half-tangent and so stays between its endpoint values, in \([-\pi/4,\pi/4]\)$[-\pi /4,\pi /4]$; and on that range \(\cos d+|\sin d|=\sqrt2\cos(|d|-\pi/4)\)$\cos d+|\sin d|=\sqrt{2}\cos (|d|-\pi /4)$ increases with \(|d|\)$|d|$, so its maximum over the row is at an endpoint. The margin \(A-B(\cos d+|\sin d|)\)$A-B(\cos d+|\sin d|)$ is at least \(10^{-12}\)${10}^{-12}$ over the whole catalogue. Independently, the source’s controls and this project’s audit check 48,112 rational quadratic inequalities, four per row, one for each vertex of the core projected on a parent axis, minimized over the whole interval including any interior critical point, and all are strictly positive.¹⁵

The lemma is what lets parents touch. Two parents with disjoint interiors may share an edge, but their closed cores lie in the two disjoint interiors, so the cores are disjoint, and the Budget lemma applies to them.

Every Legal Center Collects Enough Charge

Fix a row. Its core has a fixed side and angle, so the charge of an assigned core is a function of its center alone, and the question is where the center can be.

A parent at angle \(\varphi\)$\phi$ fits in the container exactly when its center lies in the legal center domain

because \(A(\cos\varphi+\sin\varphi)\)$A(\cos \phi +\sin \phi )$ is the width of the parent’s projection on either axis.¹⁶

Envelope lemma. The union of the legal center domains over a row, the row’s envelope, is the square \([\rho,L_0-\rho]^2\)$[\rho ,L_0-\rho {]}^2$ with inset \(\rho=\tfrac{A}{2}\min(\cos\varphi+\sin\varphi)\)$\rho =\frac{A}{2}min(\cos \phi +\sin \phi )$ taken over the two endpoint angles of the row. On \([0,\pi/2)\)$[0,\pi /2)$, \(\cos\varphi+\sin\varphi=\sqrt2\cos(\varphi-\pi/4)\)$\cos \phi +\sin \phi =\sqrt{2}\cos (\phi -\pi /4)$ has one stationary point, a maximum at \(\varphi=\pi/4\)$\phi =\pi /4$, so it has no interior minimum on any interval, and its minimum over a row is at one of the two endpoint angles; in the half-tangent the same derivative has the sign of \(1-2\tan(\varphi/2)-\tan^2(\varphi/2)\)$1-2\tan (\phi /2)-{\tan }^2(\phi /2)$, which is how the checkers see it. The domains are nested squares about the container’s center, so their union is the largest of them, which is the one with the least inset. The source scans the whole envelope for the row’s fixed core, so a center that is legal for some parent angle of the row is checked whether or not it is legal for the others. The lemma holds past \(\tan(\pi/8)\)$\tan (\pi /8)$ as well, which the last row needs.¹⁶

Work in the core frame, the coordinates with axes parallel to the core’s edges. A core of side \(B\)$B$ captures a site \(p\)$p$ exactly when its center lies in the closed axis-aligned square of side \(B\)$B$ about \(p\)$p$; call this the site’s capture rectangle. A core captures every site of a set exactly when its center lies in the intersection of their capture rectangles, which is again a closed axis-aligned rectangle, possibly degenerate or empty. So the set of centers at which a \(k\)$k$-of-\(m\)$m$ charge pays is a finite union of rectangles, one for each \(k\)$k$-subset of its sites, and the charge of a core is a nonnegative sum of indicators of closed sets.¹⁷

A union is awkward to scan; a signed sum of rectangles is easy. The source uses an identity that T-025 introduced for the same purpose.

Signed-expansion lemma. Let \(x_1,\ldots,x_m\)$x_1,\dots ,x_m$ be the capture indicators of the \(m\)$m$ sites, each \(0\)$0$ or \(1\)$1$. Then

the inner sum over the \(j\)$j$-element subsets \(J\)$J$ of the sites. Each product is the indicator of the intersection of \(j\)$j$ capture rectangles, so the right side is a signed sum of rectangle indicators, and the \(k\)$k$-of-\(m\)$m$ charge is \(w\)$w$ times it.¹⁷

Proof. Let \(h\)$h$ be the number of captured sites. A product over \(J\)$J$ is \(1\)$1$ exactly when \(J\)$J$ is a subset of the captured sites, so the inner sum is the number of \(j\)$j$-subsets of an \(h\)$h$-set, and the right side is

which is \(0\)$0$ for \(h<k\)$h<k$, as the left side is. For \(h\ge k\)$h\ge k$ take the first difference \(S(h)-S(h-1)\)$S(h)-S(h-1)$. Pascal’s identity \(\binom hj-\binom{h-1}j=\binom{h-1}{j-1}\)$\left(\genfrac{}{}{0ex}{}{h}{j}\right)-\left(\genfrac{}{}{0ex}{}{h-1}{j}\right)=\left(\genfrac{}{}{0ex}{}{h-1}{j-1}\right)$ gives

The two binomial coefficients combine. Writing both as factorials,

which is the step the source’s proof leaves out. Substituting and setting \(i=j-k\)$i=j-k$,

and the alternating sum is \((1-1)^{h-k}\)$(1-1{)}^{h-k}$: it is \(1\)$1$ when \(h=k\)$h=k$ and \(0\)$0$ when \(h>k\)$h>k$. So \(S(k)=S(k-1)+1=1\)$S(k)=S(k-1)+1=1$ and \(S(h)=S(h-1)=1\)$S(h)=S(h-1)=1$ for every \(h>k\)$h>k$, which is the left side.

Appendix B tabulates the coefficients of the three families. This project’s threshold code proves the same identity for its own checker.¹⁷

The exact sweep. Clear denominators so that every rectangle edge and every vertex of the envelope, which is a square turned by the core’s angle in the core frame, has integer coordinates, and drop the rectangles of zero area, the degenerate intersections. The vertical lines through the remaining coordinates are the event lines; they cut the frame into vertical slabs, and the horizontal lines cut each slab into y-cells, which are Part I’s event cells. On an open y-cell no retained rectangle edge is crossed, so the sweep’s signed sum is constant there; a center in an open y-cell that lies on no dropped rectangle is a generic center, and at a generic center the signed sum is the charge. The sweep walks the slabs from left to right. Entering a slab, it adds each rectangle that begins there and removes each that ends, as a range addition of its signed weight over its range of y-cells; a lazy segment tree holds the running sum per y-cell and answers the least value over any range of y-cells. Within a slab the envelope’s boundary is linear, so its vertical extent is known from the two edge values at the slab’s ends, and the sweep queries the least charge over exactly the open y-cells that meet the envelope, and takes the least over all slabs and rows. All weights are integers in units of \(10^{-9}\)${10}^{-9}$, and the sum of the absolute expanded weights over the whole certificate is 184,231,386,320, below \(2^{50}\)$2^{50}$, so no partial sum can leave the range of a signed 64-bit integer in Python or of an exactly represented integer in JavaScript. The Python scan has 86,299,918 slabs and certifies 511,649,694,680 open y-cells; the y-cells are counted by the range queries, never enumerated one by one.¹⁸

The range query is exact, though the source says so only in code. The envelope’s vertical extent at a slab’s end is a rational number, the ratio of two integers from the edge equation, while the y-cell boundaries are integers. The query asks for the open y-cells whose lower edge is below the extent’s upper end and whose upper edge is above its lower end. Comparing an integer with a rational is the same as comparing it with the rational’s floor or ceiling, so the first y-cell is found by a binary search for the floor of the lower end and the last by one for the ceiling of the upper end, and the range is exactly the open y-cells that meet the envelope on that slab. This project’s audit rebuilt the envelope as a polygon and clipped it on all 34,909 slabs of five rows, including row 11962, where \(\Gamma\)$\Gamma$ is attained, and found the same ranges and the same minimum.¹⁹

The sweep sees only generic centers, and the signed sum is only a formula for the charge there. Two things remain: centers on event lines or on dropped zero-area rectangles, where rectangles touch, and centers on the envelope’s boundary.

Boundary lemma. If the charge is at least \(\Gamma\)$\Gamma$ at every generic center of the envelope, it is at least \(\Gamma\)$\Gamma$ at every center of the closed envelope. The unexpanded charge is a nonnegative sum of indicators of closed sets, the capture rectangles and their finite intersections and unions, and such a sum is upper semicontinuous: at a limit of centers it is at least the limit of the values, because a closed set contains the limit of any sequence of its points. Every center of the closed envelope is a limit of generic centers, since the envelope has positive area and the event lines and dropped rectangles are finitely many. So the charge at any center is at least the limit superior of the charges at generic centers approaching it, which is at least \(\Gamma\)$\Gamma$. Dropping zero-area rectangles from the sweep is harmless for the same reason: they change the signed sum only on themselves, sets of zero area, so generic centers stay dense and the lemma, not the sum, gives the bound there.²⁰

The source backs this with controls: 5,586 exact centers on event lines and envelope boundaries of 14 rows, charged by direct membership rather than by rectangles, all at least \(1.000047518\)$1.000047518$. None of the 14 is one of the three rows whose minimum is below one (8844, 8845 and 11962).²⁰

The Contradiction and the Strict Bound

Suppose eleven unit squares fit in a container of side \(31/8\)$31/8$. By the Scaling lemma, eleven parents of side \(A\)$A$ fit in \([0,L_0]^2\)$[0,L_0{]}^2$. Fold each parent separately into \([0,\pi/4]\)$[0,\pi /4]$ (Folding lemma); its half-tangent lies in exactly one row, or on the shared endpoint of two, and either row’s assigned core is a closed square strictly inside the parent (Strict-core lemma), with its center in the row’s envelope (Envelope lemma). The sweep and the Boundary lemma give every such core a charge of at least \(\Gamma\)$\Gamma$; they are pairwise disjoint, and the Budget lemma caps their total charge at \(M\)$M$. Then \(11\Gamma\le M\)$11\Gamma \le M$, against \(11\Gamma>M\)$11\Gamma >M$. So no eleven parents fit, and no eleven unit squares fit in side \(31/8\)$31/8$.¹¹

That excludes side \(31/8\)$31/8$ exactly; the strict bound needs attainment.

Attainment lemma. Among the containers that admit a packing of eleven unit squares there is a smallest, so \(s(11)\)$s(11)$ is a minimum and not only an infimum. Eleven of the sixteen cells of a 4-by-4 grid hold eleven unit squares in a container of side \(4\)$4$, so a packing exists at side \(4\)$4$ and \(s(11)\le4\)$s(11)\le 4$. A packing in a container of side at most \(4\)$4$ is described by its side and the eleven centers and angles; each center lies in \([0,4]^2\)$[0,4{]}^2$, each angle in \([0,\pi/2]\)$[0,\pi /2]$, where both endpoints describe the same square, and the side in \([0,4]\)$[0,4]$, so the descriptions form a bounded closed set of \(\mathbb R^{34}\)${\mathbb{R}}^{34}$, which is compact. Containment is a closed condition, since every vertex is a continuous function of the description and lies in a closed square. Disjoint interiors is also closed: two squares whose interiors meet have a common interior point with a neighborhood inside both, which persists under every small enough change of the description, so the set of descriptions with overlapping interiors is open and its complement is closed. The feasible descriptions therefore form a compact set, the side is continuous on it, and it attains its minimum.¹¹

A packing exists at side \(s(11)\)$s(11)$, and none exists at side \(31/8\)$31/8$, so \(s(11)\ne31/8\)$s(11)\ne 31/8$; and since any packing at a side below \(31/8\)$31/8$ would also fit in side \(31/8\)$31/8$, \(s(11)>31/8\)$s(11)>31/8$. Part I states its bounds with \(\ge\)$\ge$ because that is what its verifier’s theorem states, and remarks that compactness gives the strict form; here the source states the strict form and the lemma above is its proof.²

What Was Verified, and What the Verification Means

The source supplies two checkers, a Python scanner (exact_mixed.py with integer_sweep.py) and a JavaScript scanner reconstructed from R038’s, with independent controls in standard-library rational arithmetic; this project replayed both in full, audited the premises with its own instrument, and decided the coverage a second time by a different method.⁹²¹

\(\Gamma\)$\Gamma$ is computational only: no human-readable argument explains why every assigned core of every row collects at least \(0.99996\)$0.99996$, and the value is known because two complete sweeps computed it and a third method bounded it from below.²

The register counts the two source checkers as one method, an exact event-cell sweep with signed rectangle terms, in two code lineages, the Python generalizing Kleddamag’s seventeen-square checker and the JavaScript adapting R038’s: the Python geometry uses polygon edges and the JavaScript geometry clamped extrema, and the two partition the frame differently, 86,299,918 slabs against 86,275,862, exactly two fewer per row, yet return identical per-row minima.³ The method-distinct decision is this project’s native verifier, an interval branch and bound over boxes of centers that counts captured sites with directed rounding, never forms the signed expansion, and refuses any box it cannot resolve; it certified all 12,028 rows with 136,081,500 boxes, none stalled, and a least certified lower bound of exactly \(\Gamma=0.999962528\)$\Gamma =0.999962528$.²¹ T-059 is a computation of another kind: wand125’s checker reproduces all 12,028 exact row minima with replayed witnesses, which audits the source’s row-scan claim and is not a new proof of the bound.²²

The JavaScript source is not in the archive: no code license was identified for the pinned R038 file, so prepare_secondary.py reconstructs the checker from hash-pinned upstream bytes and published edits, and verifies both hashes.⁷

The register records the result as T-037, S5/V3/C3: significance 5, movement on a central open case; verification 3, machine-checked here; confirmation 3, decided by two methods, the source’s sweeps and the native branch and bound, with the review record pending. It held V4/C4 under the ladder in force until 2026-09-30, whose fourth levels now also need two adversarial reviews by distinct reviewers and a human oversight record. Whether a same-project review of another author’s certificate counts toward confirmation is not yet decided.³

How Part III’s Certificates Relate to This One

Four facts connect this certificate to those of Part III. First, when \(2k>m\)$2k>m$ a core that captures \(k\)$k$ of \(m\)$m$ sites holds more than half of them, so in every direction its projection contains the median of the projected sites: it receives Part III’s median-type charge on the same sites, whose budget is also \(w\)$w$, and that charge pays every core the \(k\)$k$-of-\(m\)$m$ charge pays. The 2-of-3 and 3-of-5 charges are such cases; the 2-of-5 charge, with budget \(2w\)$2w$, has no counterpart there. Second, this paper’s \(\Gamma\)$\Gamma$ and \(M\)$M$ play the roles of Part III’s per-cell floors \(\Gamma_i\)${\Gamma }_i$ and budget \(b\)$b$. Third, this paper folds every angle into \([0,\pi/4]\)$[0,\pi /4]$ because its certificate has the whole \(\mathbf{D}_4\)${𝐃}_4$ symmetry; Part III works on \([0,\pi/2]\)$[0,\pi /2]$ because its cover of the centers has only the half-turn symmetry. Fourth, Part III’s rows are also closed intervals of the half-tangent, but each carries a polygon of allowed centers rather than a core.

Appendix A: Certificate Schema

The retained file global-certificate.json, whose digest the release’s manifest and the register’s evidence entry record, has ten fields: L and A, the container and parent sides as rational strings; coordinate_denominator (\(10^{10}\)${10}^{10}$) and weight_denominator (\(10^9\)${10}^9$); point_orbits, a list of 679 triples \((x,y,w)\)$(x,y,w)$ of integers, one site per orbit with its point weight, 613 of them zero; charge_orbits, a list of 284 objects each with a threshold, an integer weight and sets, the index lists of the whole orbit of one \(k\)$k$-of-\(m\)$m$ charge, eight or fewer; entries, the 12,028 rows \((a,b,t,B)\)$(a,b,t,B)$ as rational strings; and minimum_units, budget_units and bound. This project reads it with load_kleddamag_parent_core, which refuses duplicate keys, inexact numbers, a container other than \(191/50\)$191/50$, and a declared budget that the charges do not sum to. The family census is the table in The Certificate’s Charges; in the file’s units every budget there is an integer count of \(10^{-9}\)${10}^{-9}$.¹²

Appendix B: Coefficient Tables

The coefficient of the \(j\)$j$-subsets in the signed expansion of a \(k\)$k$-of-\(m\)$m$ charge is \((-1)^{j-k}\binom{j-1}{k-1}\)$(-1{)}^{j-k}(\genfrac{}{}{0ex}{}{j-1}{k-1})$, and the absolute coefficient sum is \(\sum_j\binom mj\binom{j-1}{k-1}\)${\sum }_j\left(\genfrac{}{}{0ex}{}{m}{j}\right)\left(\genfrac{}{}{0ex}{}{j-1}{k-1}\right)$, which is 5, 49, 31 for the three families the certificate uses:

The count of subsets of each size is in parentheses. The source checks the identity exhaustively on every pattern of captured sites for three and five sites and every threshold; its record also lists the other thresholds, 1-of-3 (sum 7), 3-of-3 (1), 1-of-5 (31), 4-of-5 (9) and 5-of-5 (1), none of which the certificate uses.¹⁷

Appendix C: Reproduction

The source’s README gives the commands: with Python 3.12 and Node.js, check out tag v1.0.2, install requirements.txt, run check_integrity.py, then verify.py --output-dir <fresh directory>, and finally verify_threshold_algebra.py. A complete run reports PASS_FRESH_PORTABLE_FULL_VERIFICATION, bound \(31/8\)$31/8$, 12,028 intervals and a counting surplus of \(107{,}864\)$107,864$ units. The two scans took about 9.5 minutes (Python) and 7.6 minutes (JavaScript) on the source’s machine, and 1,501 and 1,790 seconds in this project’s replay under concurrent load; the native decision took 6,197 seconds with two workers. The first run downloads one commit-pinned R038 source file and checks its hash; run with assertions enabled, since the entry points refuse -O. verify_threshold_algebra.py rewrites the committed threshold-algebra.json beside it, so run it in a copy, not in the archive.⁹

Evidence files, all retained: the source’s evidence/portable/ directory (the launcher RESULT.json, the Python scan’s per-row python.json, the JavaScript ranges under secondary/, and controls.json); this project’s full-replay receipt and independent audit; the native receipt with its row journal and reconciliation; and T-059’s row-minimum summary. The native verifier is python -m devtools.verify_kleddamag_n11_native --all, and the receipt reconciliation is python -m devtools.audit_kleddamag_n11_native, both from packing/ in the project environment.²¹

Appendix D: Series Glossary

The terms the three papers share, with the paper that derives each in full.

Sources and Verification Record

The mathematical audit of 2026-09-22 read the proof, both checkers, the controls and the attribution files, and found no blocking defect; the native parent-core review records the method-distinct decision and its receipt. The archived source tree is immutable upstream material; the receipts cited here are repository-generated. The figures are explanatory renderings of retained data, drawn from hash-pinned files, and their rounded coordinates are not inputs to any check. Every number in this paper is read from the archived source, the register or the retained receipts, and the renderer refuses a caption value the figure modules do not supply.

Version History

• v0.1.0 — October 5, 2026. The first edition: Part II of the series, the review of T-037's proof, with its figures.

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