\documentclass[11pt]{article}
\usepackage[margin=1in]{geometry}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{graphicx,booktabs,longtable,array}
\usepackage{xcolor,microtype,enumitem}
\usepackage{xurl}
\usepackage[colorlinks=true,linkcolor=blue!45!black,citecolor=blue!45!black,urlcolor=blue!45!black]{hyperref}
\usepackage[nameinlink,noabbrev]{cleveref}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{certified}[theorem]{Certified computation}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newcommand{\R}{\mathbb R}
\newcommand{\Q}{\mathbb Q}
\newcommand{\conv}{\operatorname{conv}}
\newcommand{\Int}{\operatorname{int}}
\newcommand{\diag}{\operatorname{diag}}
\newcommand{\norm}[1]{\left\lVert #1\right\rVert}
\newcommand{\abs}[1]{\left\lvert #1\right\rvert}
\newcommand{\inner}[2]{\left\langle #1,#2\right\rangle}
\newcommand{\repo}[1]{\nolinkurl{#1}}
\newcommand{\formalref}[2]{\href{https://github.com/Queuingtheorydotcom/11SquaresFormalized/blob/cdc746ed907d258057c283aeb6d077cb2c27e349/#1}{#2}}
\newcommand{\optimalref}[2]{\href{https://github.com/Queuingtheorydotcom/11SquaresOptimal/blob/4262f07c7723428c1725bb757ed06d0c4d28be1a/#1}{#2}}
\setlist[enumerate]{itemsep=3pt,topsep=6pt}
\setlength{\emergencystretch}{2em}
\renewcommand{\topfraction}{.9}
\renewcommand{\bottomfraction}{.8}
\renewcommand{\textfraction}{.08}
\renewcommand{\floatpagefraction}{.85}
\numberwithin{equation}{section}
\title{Optimal Packing of Eleven Unit Squares:\\The Formalized Voronoi-Cell Proof}
\author{By GPT-6 Astra}
\date{}
\hypersetup{pdftitle={Optimal Packing of Eleven Unit Squares: The Formalized Voronoi-Cell Proof},pdfauthor={GPT-6 Astra},pdfsubject={Expository manuscript with exact arithmetic supplements}}
\begin{document}
\maketitle
\begin{center}
Submitted by Manasseh Ahmed
\end{center}
\medskip
\begin{center}
\textbf{Contributors and acknowledgements}\\[3pt]
\small From the \href{https://github.com/Queuingtheorydotcom/11SquaresFormalized/blob/cdc746ed907d258057c283aeb6d077cb2c27e349/ACKNOWLEDGEMENTS.md}{repository acknowledgements}
and \href{https://github.com/Queuingtheorydotcom/11SquaresOptimal/blob/4262f07c7723428c1725bb757ed06d0c4d28be1a/README.md}{construction credits}
\end{center}
\begin{quote}
\small
\begin{itemize}[leftmargin=1.2em,itemsep=7pt,topsep=2pt]
\item \href{https://github.com/EvolvingPrograms}{EvolvingPrograms} and
\href{https://github.com/ctjlewis}{@ctjlewis}: verification infrastructure,
runner improvements, resumable evidence collection, and the complete replay
in \href{https://github.com/EvolvingPrograms/11SquaresEvolving}{11SquaresEvolving}.
\item \href{https://github.com/wand125}{@wand125}: the
\href{https://github.com/wand125/n11-optimality-lean}{n11-optimality-lean}
development, certificate checking, generated proofs, integration, and Lean ports.
\item \href{https://github.com/Benjamin-Gurevitch}{Benjamin Gurevitch
(@Benjamin-Gurevitch)}: T03 and returned-case formalization.
\item \href{https://github.com/Julian-JJ}{@Julian-JJ}: preparing the proof
to run on a high-performance computing cluster.
\item \href{https://github.com/Guzhou0806}{@Guzhou0806}: proof development,
transport, and independent verification.
\item \href{https://github.com/Queuingtheorydotcom}{Manasseh Ahmed
(@Queuingtheorydotcom)}: the underlying
\href{https://github.com/Queuingtheorydotcom/11SquaresOptimal}{computer-assisted proof}
and development and integration of its formalization.
\item Walter Trump: the eleven-square packing; David Ellsworth:
the reconstruction diagram credited by the bundled construction;
\href{https://github.com/jlevy/squares}{jlevy/squares} contributors:
exact construction formulas and related mathematics;
\href{https://github.com/evand}{Evan Daniel}: upstream
\href{https://github.com/evand/square-packing}{square-packing} definitions
and containment checking.
\item The \href{https://github.com/leanprover/lean4}{Lean} and
\href{https://github.com/leanprover-community/mathlib4}{Mathlib} communities:
the proof assistant, mathematical library, and supporting tools.
\end{itemize}
Also credited are all contributors, reviewers, testers, and collaborators
across 11SquaresFormalized, 11SquaresEvolving, and their upstream projects,
including contributions made outside GitHub pull requests.
\end{quote}
\begin{center}
October 30, 2026
\end{center}
\clearpage
\begin{abstract}
We explain the computer-assisted proof that eleven independently rotated unit
squares require a square container of side at least
$T=3.8770835900228141773\ldots$, the side attained by the known construction
attributed to Walter Trump. The proof reduces arbitrary packings to 2,184
patterns of occupied closed Voronoi cells. Exact geometric certificates exclude
2,180 patterns, a square-symmetry argument reduces the remaining four to one,
and a complete subdivision of that case places every possible smaller packing
inside an explicitly certified isolation neighborhood. We give the geometric
definitions, prove the continuous soundness rules underlying the finite
calculations, and explain the common-cone local isolation argument used in the
Lean development. The large certificate instances are identified by pinned
source references; they are not replaced by numerical experiments. The reported
formal verification uses Lean's kernel together with its native compiler for
specified numerical certificates.
\end{abstract}
\tableofcontents
\clearpage
\section{The problem and the structure of the proof}\label{sec:framework}

The question concerns congruent squares in the Euclidean plane, with no
restriction that their sides be parallel. A drawing of a very dense packing
proves an upper bound on the required container size. Optimality requires the
opposite inequality for \emph{every} placement and every independent choice of
orientation. This distinction is responsible for most of the work below.

This paper follows the closed-Voronoi-cell route in \cite{optimal,formal}.
It does not follow the later marker and support-chain manuscript also present
in \cite{optimal}. The current formal development simplifies two parts of the
original Voronoi route: its symmetry bridge uses four collision tests, and its
local isolation theorem uses a common system of 40 linear rows and 66 dual
certificates. We explain those versions in \cref{sec:symmetry,sec:local}.

\subsection{Squares, interiors, and admissible packings}

For $x=(x_1,x_2)$ and $y=(y_1,y_2)$ in $\R^2$, write
$\inner{x}{y}=x_1y_1+x_2y_2$, $\norm{x}=\sqrt{\inner{x}{x}}$, and
$x^\perp=(-x_2,x_1)$. An axis is a vector of length one.

\begin{definition}\label{def:square}
For a center $p\in\R^2$ and an axis $a$, define the closed unit square
\begin{equation}
 S(p,a)=\{p+\xi a+\eta a^\perp: |\xi|\leq\tfrac12,
                       |\eta|\leq\tfrac12\}
\end{equation}
Its open interior $S^\circ(p,a)$ is the set defined by replacing both weak
inequalities with strict inequalities. A packing of $n$ unit squares in side
$s\geq0$ is a list $S(p_i,a_i)$, $0\leq i<n$, such that
\begin{equation}
 S(p_i,a_i)\subseteq[0,s]^2,\qquad
 S^\circ(p_i,a_i)\cap S^\circ(p_j,a_j)=\varnothing\quad(i\ne j)
\end{equation}
Write $\mathcal A_{11}$ for the set of sides admitting such a packing, and
$s_{11}=\inf\mathcal A_{11}$ for its infimum.
\end{definition}

Thus squares may touch each other and the container. Reflection is already
allowed by this definition, and changing $a$ to $-a$ or $a^\perp$ describes
the same set. A rotation of the whole container lets us take its sides to be
parallel to the coordinate axes without restricting the problem.

Let
\begin{equation}\label{eq:P}
 P(X)=5X^8-10X^7-2X^6+14X^5+12X^4-6X^3+2X^2+2X-1
\end{equation}
Let $u$ be its unique zero in $(9/25,37/100)$; uniqueness is proved in
\cref{lem:root}. Define
\begin{equation}\label{eq:T}
 T=\frac{6u+4}{1+2u-u^2}
\end{equation}

\begin{theorem}[Optimality]\label{thm:main}
There is a packing of eleven unit squares in $[0,T]^2$. Every packing of
eleven unit squares in $[0,s]^2$ satisfies $s\geq T$. Consequently the
minimum, not just the infimum, is
\begin{equation*}
 s_{11}=T=3.8770835900228141773078970601\ldots
\end{equation*}
\end{theorem}

The decimal is informative; \cref{eq:P,eq:T} specify the exact number.
The proof of the theorem is completed in \cref{sec:conclusion}.

\subsection{What is proved on paper and what is checked finitely}

The argument has five stages.
\begin{enumerate}
\item Exhibit an exact algebraic packing at $T$.
\item Cover the possible normalized centers by sixteen closed cells, each
      too small to contain two square centers. Half-turn symmetry leaves
      2,184 possible occupied-cell patterns.
\item Exclude all but four patterns by exact certificates whose rules
      preserve every feasible square position and orientation.
\item Apply symmetries of the container to reach one specified pattern,
      numbered 438.
\item Divide that pattern into four exhaustive branches. Three are
      impossible; the fourth lies in a neighborhood where an analytic
      argument forces the exact attaining construction.
\end{enumerate}

A \emph{certificate} means finite data that satisfy explicit, checkable
premises of a mathematical implication. Examples are rational polygon vertices,
a list of closed angular intervals, or nonnegative weights combining linear
inequalities. A \emph{checker} verifies those premises. Its
\emph{soundness theorem} proves that acceptance implies the asserted
mathematical conclusion. Searching for data and checking data are different
tasks; the search need not be trusted once the data and soundness theorem
are available.

Statements headed ``Certified computation'' identify the finite instances
imported from the repositories. Their surrounding lemmas explain the
continuous geometry and analysis that give them meaning. We do not print
the enormous generated certificate corpus or claim to reproduce its full
Lean build in this manuscript project. Precise source references, the formal
trust model, and the smaller independently executable supplement are given
in \cref{sec:formal,app:reproduction}. This separation is essential: a
finite list of successful numerical trials would not establish
\cref{thm:main}.

\subsection{Two elementary geometric facts}\label{sec:basics}

\begin{lemma}[Inscribed disks and center separation]\label{lem:separation}
Every $S(p,a)$ contains the closed disk of radius $1/2$ about $p$, and
its interior contains the corresponding open disk. Distinct centers in a
packing satisfy $\norm{p_i-p_j}\geq1$. Every center in a side-$s$ packing
belongs to $[1/2,s-1/2]^2$.
\end{lemma}
\begin{proof}
The orthonormal basis $(a,a^\perp)$ gives
$\inner{x-p}{a}^2+\inner{x-p}{a^\perp}^2=\norm{x-p}^2$.
If the right side is at most $1/4$, both body coordinates have absolute
value at most $1/2$; the strict version follows in the same way. If two
centers were less than one apart, their midpoint would lie in both open
disks and hence in both square interiors. Finally the four points
$p\pm(1/2,0)$ and $p\pm(0,1/2)$ lie in the square, so containment gives
the asserted coordinate bounds.
\end{proof}

For a nonzero vector $v$, projection onto $v$ means the scalar
$\inner{x}{v}$. The projection of $S(p,a)$ is the interval centered at
$\inner{p}{v}$ with radius
\begin{equation}\label{eq:support}
 h_a(v)=\frac{|\inner{a}{v}|+|\inner{a^\perp}{v}|}{2}
\end{equation}
This follows by maximizing separately over $\xi$ and $\eta$ in
\cref{def:square}. In particular, if
\begin{equation}\label{eq:sep-axis}
 \inner{p_j-p_i}{v}\geq h_{a_i}(v)+h_{a_j}(v)
\end{equation}
then the interiors are disjoint. Equality permits contact.

A \emph{convex} set contains every line segment joining two of its
points; its \emph{convex hull} is the set of finite convex combinations
$\sum_k\lambda_kx_k$ with $\lambda_k\geq0$ and $\sum_k\lambda_k=1$.
A \emph{halfplane} is a set $\{x:\inner{n}{x}\leq b\}$ with $n\ne0$.
A bounded intersection of finitely many closed halfplanes is a convex polygon,
possibly a segment, a point, or the empty set. An edge of a
two-dimensional polygon is also called a facet. These degenerate cases
will matter in the certificate argument.

For a convex compact set $K$ and nonzero $n$, its supporting face in
direction $n$ is the set where $\inner{n}{x}$ attains its maximum on
$K$. The vector $n$ is a normal to the corresponding supporting line;
an outward facet normal points away from the polygon across that facet.

\begin{lemma}[Separating axes for squares]\label{lem:SAT}
Two unit squares have disjoint interiors if and only if their projection
intervals have disjoint interiors along at least one of
$a_i,a_i^\perp,a_j,a_j^\perp$.
\end{lemma}
\begin{proof}
Sufficiency follows from \cref{eq:sep-axis}, allowing either sign of $v$.
For necessity put $K_i=S(0,a_i)$ and $K_j=S(0,a_j)$. The set
$K_i-K_j=\{x-y:x\in K_i,y\in K_j\}$ is a convex polygon. Its edges
are parallel to edges of one of the two squares: a supporting face of a
sum of polygons is the sum of their supporting faces, so a one-dimensional
face has one of those directions. Its outward normal directions are
therefore among the four stated axes and their negatives.
The interiors overlap exactly when $p_j-p_i$ lies in
$\Int(K_i-K_j)$. Indeed, overlap supplies a difference of interior
points; conversely an interior point of this sum of two full-dimensional
convex polygons belongs to $\Int K_i+\Int(-K_j)$, as follows explicitly: for $0<\lambda<1$,
$\lambda(K_i-K_j)=\lambda K_i+\lambda(-K_j)\subset
\Int K_i+\Int(-K_j)$, and these contracted polygons exhaust
$\Int(K_i-K_j)$ because the origin is an interior point. A point outside the interior of a polygon violates, or attains
equality in, one of its defining facet inequalities. The corresponding
normal gives \cref{eq:sep-axis} with one of the two signs.
\end{proof}
\section{The exact attaining construction}\label{sec:construction}

\begin{lemma}\label{lem:root}
The polynomial $P$ has exactly one zero in $[9/25,37/100]$, and this zero
lies in its interior.
\end{lemma}
\begin{proof}
Exact substitution gives
\begin{equation*}
 P(9/25)=-\frac{772365104}{30517578125}<0,\qquad
 P(37/100)=\frac{37988917991321}{2000000000000000}>0
\end{equation*}
Continuity gives existence. For uniqueness write
\begin{equation*}
 P'(x)=40x^7-70x^6-12x^5+70x^4+48x^3-18x^2+4x+2
\end{equation*}
Throughout this positive interval, bound each positive monomial from below
by its value at $9/25$, and each negative monomial from below by its value
at $37/100$. Their sum is
$10398878171521/2500000000000>0$. Thus $P$ is strictly increasing there.
\end{proof}

Set
\begin{equation}\label{eq:cs}
 c=\frac{1-u^2}{1+u^2},\qquad d=\frac{2u}{1+u^2}
\end{equation}
Then $c,d>0$ and $c^2+d^2=1$. The letter $d$ denotes a sine value here,
not a side length. Define
\begin{align}
 \rho&=1-(T-3)c,&
 \eta&=\frac{(1+\rho)c-1}{d},& v&=c-d\label{eq:construct-constants}\\
 \zeta&=\frac{T-1}{d}-\rho-(3+\eta)\frac cd,&
 x_0&=1+\frac2c-(T-2)\frac dc\nonumber
\end{align}
All denominators are positive. For real $a,b$, let
$A(a,b)=[a,a+1]\times[b,b+1]$, and put
\begin{equation}\label{eq:F}
 F(x,y)=(1,1)+\begin{pmatrix}c&-d\\d&c\end{pmatrix}
                       \binom{x}{y-\rho}
\end{equation}

\begin{proposition}[Attaining configuration]\label{prop:construction}
The following eleven squares form a packing in $[0,T]^2$:
\begin{align*}
 &A(0,0),\ A(T-1,0),\ A(x_0,T-1),\ A(0,T-1),\ A(1,T-1),\ A(0,T-2)\\
 &F(A(0,0)),\ F(A(\eta,-1)),\ F(A(1,v)),\
 F(A(\eta+1,v-1)),\ F(A(\eta+2,-\zeta))
\end{align*}
Their horizontal and vertical spans are both $T$.
\end{proposition}
\begin{proof}[Proof and finite algebraic verification]
The matrix in \cref{eq:F} is orthogonal, so it preserves unit squares.
Each of the eleven squares is the convex hull of its four vertices. Hence
containment is equivalent to 88 two-sided bounds on the coordinates of the 44 vertices.
For each of the 55 pairs, \cref{lem:SAT} reduces disjointness of interiors
to finding one weak separating axis among the edge axes of the two squares.
These finite bounds are exact algebraic inequalities in $u$. They are
established by the construction data and proofs in
\formalref{ElevenSquare/Construction.lean}{\repo{Construction.lean}} and
\formalref{ElevenSquare/ConstructionData.lean}{\repo{ConstructionData.lean}}.
The supplemental checker in this project also checks the displayed
construction directly; its scope is described in \cref{app:reproduction}.

To explain how this finite step avoids numerical tolerances, reduce
polynomial expressions using $P(u)=0$, test zero expressions algebraically,
and isolate $u$ between increasingly tight rational endpoints. A nonzero
expression of known sign is certified when its rational interval enclosure
lies wholly on one side of zero. Inverses used in this calculation are
verified algebraically, so no unproved assertion about a denominator is
needed. The formal sources contain their own exact arithmetic realization.

Finally $A(0,0)$ meets both coordinate-zero walls,
$A(T-1,0)$ meets $x=T$, and $A(0,T-1)$ meets $y=T$.
Containment and these contacts prove both span assertions.
\end{proof}

\begin{figure}[!htbp]
\centering
\includegraphics[width=.63\textwidth]{figures/construction.pdf}
\caption{The attaining construction, with labels $0,\ldots,10$ in the order
of \cref{prop:construction}. Coordinates in the drawing are rounded only
for display. The algebraic formulas and weak separating inequalities certify
the actual packing.}
\label{fig:construction}
\end{figure}

The construction is attributed to Walter Trump; the bundled upstream
construction credits David Ellsworth's reconstruction diagram. The
formalization and verification have additional contributors, including
EvolvingPrograms and the incorporated upstream developments
\cite{credits}. This manuscript makes no new priority claim.
\section{From arbitrary packings to 2,184 Voronoi patterns}\label{sec:voronoi}

\subsection{Three coordinate systems}

The exact endpoint $T$ is algebraic. Much of the global exclusion uses the
slightly larger rational number
\begin{equation}\label{eq:ULB}
 U=\frac{387708359002281417731}{10^{20}},\qquad
 L=\frac{191}{50},\qquad B=\frac LU
\end{equation}
Exact arithmetic gives $T<U$. If a packing exists at side $s<T$, translate
every square by $((U-s)/2,(U-s)/2)$. Its container is now
$[(U-s)/2,(U+s)/2]^2\subset[0,U]^2$. This translation leaves all distances,
angles, and non-overlap conditions unchanged.

For a center $p$ in this positive $U$-container, distinguish
\begin{equation}\label{eq:frames}
 p\quad\text{(physical)},\qquad
 z=\frac{p-(1/2,1/2)}{U-1}\quad\text{(normalized)},\qquad
 p_f=Bp\quad\text{(field)}
\end{equation}
By \cref{lem:separation}, $z\in[0,1]^2$. The field transformation is a
scaling: its container has side $L$, and its small squares have side $B$.
In particular the field calculation is not a unit-square packing problem
at side $L$.

\subsection{Closed nearest-site cells}

Let $q_0,\ldots,q_{15}$ be the sixteen rational points in
\cref{tab:sites}. These are auxiliary points used to divide the space of
possible centers; they are not required to be the centers of a packing.

\begin{definition}
The closed Voronoi cell of $q_j$, restricted to the unit box, is
\begin{equation}\label{eq:cell}
 C_j=\{z\in[0,1]^2:\norm{z-q_j}^2\leq\norm{z-q_k}^2
                       \text{ for all }k=0,\ldots,15\}
\end{equation}
Its physical version is $\widehat C_j=(1/2,1/2)+(U-1)C_j$.
\end{definition}

For each $z$ one of the sixteen distances is minimal. Thus
$\bigcup_j C_j=[0,1]^2$. Equality of distances places $z$ in every tied
cell. We keep these shared boundaries throughout the argument. Expanding
squared distances shows that the cell inequalities are rational halfplanes:
\begin{equation}\label{eq:bisector}
 2\inner{q_k-q_j}{z}\leq\norm{q_k}^2-\norm{q_j}^2
\end{equation}

\begin{certified}[Covering-radius bound]\label{cert:radius}
With $r=173/1000$, every $z\in[0,1]^2$ is within distance $r$ of at
least one site $q_j$.
\end{certified}

The formal proof divides the unit box into finitely many dyadic boxes
(rectangles obtained by repeated bisection). For each final box it supplies
a site whose squared distance from all four corners is at most $r^2$.
The squared-distance function is convex, so the same bound holds on the
convex hull of those corners. The subdivision covers the original box,
including shared edges. The four files
\formalref{ElevenSquare/GeneratedCover0.lean}{\repo{GeneratedCover0.lean}}
through \repo{GeneratedCover3.lean}, composed in
\formalref{ElevenSquare/Cover.lean}{\repo{Cover.lean}}, certify this finite
claim. The supplement gives a different exact check by reconstructing
the rational vertices of every cell and checking their distances to its site.

\begin{lemma}[Capacity one]\label{lem:capacity}
A closed physical cell $\widehat C_j$ contains at most one center of any
packing of unit squares.
\end{lemma}
\begin{proof}
If $z\in C_j$, its nearest-site property and \cref{cert:radius} give
$\norm{z-q_j}\leq r$. Therefore any $z,z'\in C_j$ satisfy
$\norm{z-z'}\leq2r$. In physical coordinates the squared distance is at
most $4r^2(U-1)^2$, and exact rational comparison gives
\begin{equation}\label{eq:capacity-bound}
 4\left(\frac{173}{1000}\right)^2
 \left(\frac{287708359002281417731}{10^{20}}\right)^2<1
\end{equation}
This contradicts \cref{lem:separation} for two distinct centers.
\end{proof}

\begin{figure}[!htbp]
\centering
\includegraphics[width=.61\textwidth]{figures/voronoi-cover.pdf}
\caption{The sixteen closed Voronoi cells in normalized coordinates.
Dots are the sites; numbers are cell labels. Shared edges belong to both
adjacent cells. The cover has exact half-turn symmetry.}
\label{fig:cover}
\end{figure}

\subsection{Occupied masks and the half-turn quotient}

\begin{definition}
An \emph{assignment} of a packing is a choice of a label $j$ for each
square such that its center lies in $\widehat C_j$. Its \emph{occupied
mask} is the set of chosen labels.
\end{definition}

An assignment always exists, and \cref{lem:capacity} makes it injective.
Every eleven-square packing therefore has an eleven-element mask. More
than one assignment may be possible; no uniqueness is asserted.

The sites satisfy $q_{15-j}=(1,1)-q_j$. The half turn
$H(z)=(1-z_1,1-z_2)$ consequently takes $C_j$ exactly to $C_{15-j}$:
it preserves the box and every comparison of distances. For a mask $J$ put
$HJ=\{15-j:j\in J\}$.

\begin{definition}
Represent a mask by its increasing tuple. Compare two tuples
lexicographically, meaning at their first differing entry. Its
\emph{canonical mask} is the smaller of $J$ and $HJ$. List all canonical
masks in lexicographic order and number them starting at zero; denote the
mask at index $m$ by $J_m$.
\end{definition}

\begin{lemma}\label{lem:casecount}
There are exactly $2,184$ canonical masks. Every packing in the $U$-container,
possibly after a physical half turn about its center, admits one of them.
\end{lemma}
\begin{proof}
There are $\binom{16}{11}=4,368$ eleven-element masks. An $H$-invariant
mask is a union of pairs $\{j,15-j\}$, so has even cardinality. Thus no
eleven-element mask is fixed, and every orbit has two elements. Dividing
by two gives 2,184. Applying a half turn to the actual packing realizes
the replacement of a mask by its half-turn partner.
\end{proof}

Write $\mathcal M=\{0,\ldots,2183\}$. The four cases that survive the
global exclusions are
\begin{equation}\label{eq:candidates}
 \mathcal C=\{438,999,1462,1659\}
\end{equation}
Their exact masks are recorded here because subsequent statements depend on
the labeling convention, not just on a count.
\begin{center}
\begin{tabular}{rl}
\toprule Index & Increasing cell labels\\\midrule
438 & $0,1,2,3,4,8,9,10,11,13,15$\\
999 & $0,1,2,4,6,7,9,10,12,14,15$\\
1462 & $0,1,3,5,6,8,9,11,12,13,14$\\
1659 & $0,2,3,4,5,6,7,11,12,13,14$\\\bottomrule
\end{tabular}
\end{center}

The word ``case'' means the assertion that a packing admits the specified
closed-cell assignment. It never means an assumption that centers avoid
cell boundaries or that square orientations have been fixed.
\section{Exact certificates excluding the noncandidate cases}\label{sec:certificates}

This section explains both kinds of exclusion used by the Voronoi proof:
counting inequalities from weighted auxiliary points and geometric
propagation of possible poses. Their finite data are extensive, but the
soundness rules are geometric statements about all real configurations.

\subsection{Continuous angles represented by rational intervals}

In the field frame a square has side $B$ and can be written
\begin{equation}\label{eq:pose-square}
 S_B(x,t)=x+R(t)[-B/2,B/2]^2,\qquad
 R(t)=\frac1{1+t^2}
 \begin{pmatrix}1-t^2&-2t\\2t&1-t^2\end{pmatrix}
\end{equation}
Every orientation is represented by $t\in[0,1]$, since a square is
unchanged by a quarter turn and $t=\tan(\theta/2)$ for
$\theta\in[0,\pi/2]$. The endpoints $t=0,1$ represent the same
axis-aligned shape, and both are retained. Different squares have
independent parameters.

A \emph{pose} is a pair $(x,t)$ of center and orientation parameter.
A \emph{pose row} consists of a closed interval $I=[a,b]\subset[0,1]$
and a closed center region $D$, a finite union of rational convex polygons.
It represents $D\times I$. An \emph{outer pose cover} is a finite union
of such rows that contains every feasible pose under the current case and
branch assumptions. Containment, rather than equality, is sufficient:
retaining an impossible pose may reduce efficiency but cannot invalidate
an exclusion.

Initially the center region is the scaled physical cell, intersected with
necessary wall bounds. At parameter $t$ the horizontal and vertical
half-widths are equal to
\begin{equation*}
 h(t)=\frac B2\frac{1-t^2+2t}{1+t^2}
\end{equation*}
On a closed row the minimum of the fraction occurs at an endpoint: in
angular coordinates it is $\cos\theta+\sin\theta$, whose only interior
critical point in $[0,\pi/2]$ is a maximum. Thus
$\min(h(a),h(b))\leq x_1,x_2\leq L-\min(h(a),h(b))$ is a valid
outer envelope. The bounds remain weak, allowing wall contact.

\subsection{Strict cores and owned hulls}

Two inclusions must be kept distinct. Outer covers bound where a square
\emph{can be}; inner sets specify points the square \emph{must contain}.

\begin{definition}\label{def:owned}
A \emph{strict core} for an angle row $I$ is a nonempty two-dimensional compact convex polygon $Q$
such that $Q\subset\Int S_B(0,t)$ for every $t\in I$.
An \emph{owned hull} for square $i$ is a nonempty compact convex polygon $K_i$ (possibly a point or segment)
such that $K_i\subset\Int S_B(x_i,t_i)$ in every packing compatible
with the current assumptions. The word ``owner'' refers to this square,
usually indexed by its assigned cell.
\end{definition}

The core is attached to a variable center, whereas an owned hull is in fixed
field coordinates. A core proof is elementary. For a vertex $q=(q_1,q_2)$
one must check both signed inequalities for the body coordinates
\begin{equation*}
 \frac{(1-t^2)q_1+2tq_2}{1+t^2},\qquad
 \frac{-2tq_1+(1-t^2)q_2}{1+t^2}
\end{equation*}
to have absolute value strictly below $B/2$ on $I$. After multiplication
by $1+t^2>0$, these are positivity tests for rational quadratics. A
quadratic on a closed interval has its minimum at an endpoint or at its
interior stationary point when its leading coefficient is positive.
Checking these finitely many rational values proves the inequalities on
the whole interval. Convexity then proves them on the whole polygon.

The scaled site $y_j=B((1/2,1/2)+(U-1)q_j)$ is initially owned
by the square assigned to cell $j$: its distance to every possible
field center in that cell is at most $B(U-1)r<B/2$. This follows
from the covering-radius bound and \cref{eq:capacity-bound}. More
generally, a point $y$ is initially owned if every possible center $x$
satisfies $\norm{y-x}<B/2$, by the scaled version of
\cref{lem:separation}. On a convex center polygon it suffices to verify
this strict bound at each vertex. Sharper seed certificates use the
body-coordinate inequalities and wall envelopes directly. In either
case a finite convex hull of owned points is still strictly inside the
square. Strictness is needed in the next lemma.

\begin{lemma}[Forbidden Minkowski regions]\label{lem:minkowski}
Let $K_j$ be owned by a different square $j$, and let $Q_i$ be a strict
core for a row of square $i$. Every center in
\begin{equation}\label{eq:forbidden}
 K_j-Q_i=\{k-q:k\in K_j,\ q\in Q_i\}
\end{equation}
is impossible for square $i$ in that row.
\end{lemma}
\begin{proof}
If $x_i=k-q$, then $k=x_i+q$ lies strictly inside square $i$ by the
core property and strictly inside square $j$ by ownership. This violates
disjointness of interiors. Both conclusions remain strict when $k$ or
$q$ lies on the boundary of its auxiliary polygon. Consequently the
entire closed set in \cref{eq:forbidden} is forbidden.
\end{proof}

The operation $A+B=\{a+b:a\in A,b\in B\}$ is the \emph{Minkowski
sum}; \cref{eq:forbidden} is $K_j+(-Q_i)$. For convex polygons it is
the convex hull of all sums of vertices. This gives an exact rational
construction of the forbidden set.

\subsection{Propagation rules and their invariant}

The invariant at each step is: every compatible packing lies in each
owner's outer pose cover and contains each owner's hull strictly in that
square's interior. The following updates preserve it.

\paragraph{Removing forbidden poses.}
For one row, let $F_1,\ldots,F_k$ be verified forbidden polygons and
$D'_1,\ldots,D'_m$ proposed residual polygons. Check
\begin{equation}\label{eq:residual}
 D\subseteq\bigcup_{\ell=1}^kF_\ell\ \cup\
                   \bigcup_{\ell=1}^mD'_\ell
\end{equation}
An actual center cannot be in any $F_\ell$, hence is retained in the
residual cover. The residual may overlap a forbidden set; equality with a
set difference is unnecessary.

\paragraph{Using every pose of a partner.}
Suppose another owner has a complete pose cover. A region $F$ is forbidden
if, for every partner row with strict core $Q_j$ and domain $D_j$,
\begin{equation*}
 F\subseteq\bigcap_{y\in D_j}\bigl(y+Q_j-Q_i\bigr)
\end{equation*}
For any actual partner pose this guarantees intersection of the translated
strict cores. If $Q_j-Q_i$ has facets $\inner{n}{z}\leq h_n$, the
condition is checked by
\begin{equation*}
 \inner{n}{x}\leq h_n+\min_{y\in D_j}\inner{n}{y}
 \quad(x\in F)
\end{equation*}
Linear extrema occur at polygon vertices. All partner rows must be
included. An empty complete partner cover is already a contradiction.

\paragraph{Promoting new owned points.}
Let $Q=\{q:\inner{n}{q}\leq h_n\text{ for all its facets}\}$ be a
strict core in a residual row with domain $D'$. A fixed point $y$ lies
in $x+Q$ for every $x\in D'$ exactly when
\begin{equation}\label{eq:promotion}
 \inner{n}{y}\leq h_n+\min_{x\in D'}\inner{n}{x}
 \quad\text{for every facet}
\end{equation}
Check this for every nonempty residual row. Empty rows are skipped;
if all rows are empty the terminal contradiction already applies. Then $y$ is owned regardless of which
row contains the actual pose. Add it to the owned hull. Replacing an owned
vertex list by a shorter list is safe when every new point is an exact
convex combination of already justified points. Promotion before all
angles allowed by the branch assumptions are covered would be invalid.

\paragraph{Using a square's own hull.}
If the projection radius of the square in direction $n$ is at most $E$
throughout the current row and $K$ is owned, then necessarily
\begin{equation}\label{eq:selfcut}
 \max_{y\in K}\inner{n}{y}-E\leq\inner{n}{x}
 \leq\min_{y\in K}\inner{n}{y}+E
\end{equation}
Indeed every owned point is inside the square, so its projection differs
from the center's by at most $E$. These are consequences of proved
ownership, not imposed contacts or guesses about the optimum.

\begin{proposition}[Soundness of a propagation trace]\label{prop:trace}
A finite sequence of the preceding updates, starting from verified seed
data, excludes its case and branch assumptions if either some owner's
complete pose cover becomes empty or two different owners' hulls intersect.
\end{proposition}
\begin{proof}
Induction preserves the invariant. An empty cover would leave the actual
pose nowhere to lie. An intersection of owned hulls would supply a point
in two square interiors. Either contradicts a compatible packing.
\end{proof}

A trace is the finite record of these updates and their witnesses. A
branch adds stated inequalities to the assumptions; a contradiction within
one branch excludes only that branch. A family of branch traces excludes
the parent case only after its assumptions are shown to cover the parent.

\subsection{Why zero-area sets are not discarded}

All row intervals and polygon inequalities are closed. In particular a
point or a segment is a possible residual domain. It cannot be declared
empty merely because its area is zero. For a segment
$x(t)=a+t(b-a)$, $0\leq t\leq1$, intersecting a rational polygon with
the segment reduces each of its halfplanes to a linear inequality in $t$.
The checker can therefore verify \cref{eq:residual} by exact coverage of
$[0,1]$ by closed intervals. Taking $a=b$ includes the singleton case.

For a two-dimensional polygon an exact arrangement calculation can check
coverage on the open slabs between successive vertex abscissae and
halfplane intersection events. Endpoints of vertical slices are affine
functions on each such slab; the required interval-cover inequalities
reduce to linear inequalities. The finite union on the right of
\cref{eq:residual} is closed. Containing a dense subset of the old polygon
therefore implies containing its closure, including event lines and edges.
This is a proof of coverage, not an area comparison. The historical
checker rules and their treatment of degenerate sets are detailed in
\cite{continuum}; the formal development proves the corresponding
set-inclusion implications.

\subsection{Charge fields: finite budgets for a packing}\label{sec:charges}

Propagation is not the only source of exclusions. Other certificates assign
a nonnegative \emph{charge} $\Phi(S)$ to each square. They prove a
global budget $\sum_i\Phi(S_i)\leq W$ for any packing, and cellwise
lower bounds $\Phi(S_i)\geq\gamma_j$ for a square assigned to cell $j$.
If $\sum_{j\in J}\gamma_j>W$, the mask $J$ is impossible.

The auxiliary points in a charge field are distinct fixed points in the
field plane; they are separate data from the sixteen Voronoi sites.
Several elementary budget rules are used.

\begin{lemma}[Point and counting budgets]\label{lem:charge}
For a fixed finite set $G$ of $m$ auxiliary points put
$N_G(S)=|G\cap\Int S|$. Across an interior-disjoint packing,
\begin{equation*}
 \sum_i N_G(S_i)\leq m
\end{equation*}
For an integer $k\geq1$, both the threshold charge
$\mathbf1_{N_G(S)\geq k}$ and the charge
$\lfloor N_G(S)/k\rfloor$ have total budget $\lfloor m/k\rfloor$.
A weighted point charge $\sum_{v\in G}w_v\mathbf1_{v\in\Int S}$,
with $w_v\geq0$, has total budget $\sum_vw_v$.
\end{lemma}
\begin{proof}
Each auxiliary point belongs to at most one square interior. Hence the
first and weighted bounds hold by summing point contributions. Moreover
$k\mathbf1_{N\geq k}\leq N$ and $k\lfloor N/k\rfloor\leq N$.
Sum these inequalities and use integrality of the left-hand charge sums.
Here $\mathbf1_E$ is one if $E$ holds and zero otherwise, and
$\lfloor x\rfloor$ is the greatest integer at most $x$.
\end{proof}

One less familiar charge detects intersections with convex hulls of a
majority of auxiliary points.

\begin{definition}
For $|G|=2k-1$, a square has \emph{majority-hull charge} one if
$\Int S\cap\conv A\ne\varnothing$ for every $k$-element subset
$A\subset G$, and charge zero otherwise.
\end{definition}

\begin{lemma}[Majority-hull budget]\label{lem:majority}
At most one square of an interior-disjoint packing has majority-hull
charge one for a fixed group $G$.
\end{lemma}
\begin{proof}
If two squares had charge one, select for each $k$-subset one witnessing
intersection point in each square. The two convex hulls of these finite
witness sets are compact, convex, contained strictly inside their respective
squares, and disjoint. They are strictly separated by a line. For completeness,
choose a closest pair of points in these two compact sets; convexity implies
that the perpendicular bisector of their joining segment separates the
sets strictly, by the one-sided derivatives of squared distance at the
minimum. At least $k$ of the $2k-1$ points of $G$ lie in one of the two
closed halfplanes bounded by this line (assign any points on the line to
one side). Their convex hull cannot meet the witness hull on the opposite
side. This contradicts its chosen witness for that $k$-subset.
\end{proof}

This feature is also finitely certifiable on a pose row. For a strict core
$Q$, the condition that $x+Q$ meet every $\conv A$ is
\begin{equation}\label{eq:majority-core}
 x\in\bigcap_{|A|=k}(\conv A-Q)
\end{equation}
For a directed normal $n$, the support bound for $\conv A-Q$ is
$\max_{v\in A}\inner{n}{v}-\min_{q\in Q}\inner{n}{q}$.
Minimizing the first term over all $k$-subsets gives the $k$th smallest
of the $2k-1$ projections, their median. The needed normals are finite:
both directed normals perpendicular to every edge of $Q$ and to every
nonzero difference of auxiliary points contain every possible facet normal of these Minkowski polygons.
Thus exact median halfplanes prove \cref{eq:majority-core}; alternatively
one may check each of its finitely many polygon inclusions directly.

Nonnegative rational combinations of the preceding charges have the
corresponding combined budgets. For each possible pose, strict cores
certify that selected auxiliary points lie inside the square, or that
\cref{eq:majority-core} holds. Polygon covers and complete angular
intervals give uniform cellwise charge lower bounds. Linear programming
(optimization of a linear expression subject to linear inequalities) can
discover suitable weights, but the proof only uses the resulting exact
nonnegative coefficients and inequalities. No numerical optimizer verdict
is a premise.

Some field certificates also use points already owned by an occupied
square. Such a point cannot lie inside any other square, giving charge
budget zero for the other owners. This use retains the owner's occupancy
as an explicit assumption. A certificate for a smaller occupied set
therefore transfers to an eleven-cell mask only when that mask contains
every cell used in the certificate's assumptions, or after a justified
physical symmetry.

\subsection{The exhaustive exclusion theorem}

\begin{certified}[Noncandidate exclusion]\label{cert:exclusions}
For every $m\in\mathcal M\setminus\mathcal C$, no packing of unit
squares in $[0,U]^2$ admits the mask $J_m$.
\end{certified}

The original certificate inventory consists of 1,931 baseline exclusions,
76 extensions, and 173 further exclusions. The baseline uses 59 field
certificates and 34 generic geometric certificates; one certificate can
exclude several masks by containment of its occupied antecedent.
The current formal implementation further selects 44 field certificates
covering the same 1,904 field cases, as documented in
\formalref{Sqpack/S11Opt/Simplified/SelectedFields.lean}{\repo{SelectedFields.lean}}.
These are counts of certificate objects and their coverage, not a change
to the outer three-family partition. The required conclusion is the exact set equality
\begin{equation}\label{eq:union}
 E_{\rm base}\ \dot\cup\ E_{\rm ext}\ \dot\cup\ E_{\rm ret}
       =\mathcal M\setminus\mathcal C
\end{equation}
where $\dot\cup$ denotes disjoint union. The arithmetic
$1931+76+173=2180$ does not alone prove this equality. Exact case identities,
mask transfers, and discharged conditional premises are part of the
verification. The formal integration includes
\formalref{ElevenSquare/Interop/Wand125/Families.lean}{\repo{Interop/Wand125/Families.lean}}
and the exclusion interfaces listed in \cref{sec:formal}.

There is a potential circularity to avoid: some conditional exclusions
use earlier independently established support restrictions. Those
restrictions must be proved before the conditional results are used.
The final four-case symmetry bridge in the next section depends on
\cref{cert:exclusions}; it cannot in turn be used to justify that
same exclusion inventory. The imported theorem dependencies establish
the required order.
\section{The square-symmetry bridge to case 438}\label{sec:symmetry}

The four surviving masks do not form an ordinary orbit under a permutation
of the sixteen cells. Only the half turn has that simple effect on the
cover. A quarter turn may split one cell across several others. The
symmetry argument must therefore track how a point can be labeled in
several views at once.

\subsection{Four views and their common refinement}

Let $D_4$ denote the eight Euclidean symmetries of the unit square, with
composition as group operation. Choose four representatives modulo the
half turn $H$:
\begin{equation}\label{eq:views}
 \begin{aligned}
 g_0(x,y)&=(x,y),&g_1(x,y)&=(1-x,y)\\
 g_2(x,y)&=(1-y,x),&g_3(x,y)&=(y,x)
 \end{aligned}
\end{equation}
Together $g_0,\ldots,g_3,Hg_0,\ldots,Hg_3$ are all eight symmetries.
Their physical versions act about $(U/2,U/2)$, and normalization in
\cref{eq:frames} intertwines the two actions.

For a label quadruple $\ell=(\ell_0,\ell_1,\ell_2,\ell_3)$, define
its \emph{overlay region}
\begin{equation}\label{eq:overlay}
 R_\ell=\bigcap_{k=0}^3g_k^{-1}(C_{\ell_k})
\end{equation}
A center with these four chosen labels lies in $R_\ell$. The choices
in different views are independent; there is no symmetry-compatible
tie-breaking rule to prove.

\begin{certified}[Overlay inventory]\label{cert:overlay}
There is a fixed lexicographically ordered list of 220 label quadruples containing every quadruple
with nonempty overlay region.
\end{certified}

In the exact polygon reconstruction these are 212 two-dimensional polygons
and eight points. The current formal proof needs only exhaustiveness of
the list. Its finite tree tries all sixteen possible labels at each of
four levels. A rejected branch is supplied with a rational halfplane
contradiction. Specifically, for inequalities
$\inner{n_j}{x}\leq b_j$, nonnegative weights $\lambda_j$ with
$\sum_j\lambda_jn_j=0$ and $\sum_j\lambda_jb_j<0$ would imply
$0<0$. An accepted leaf matches an entry in the list. This proves
exhaustiveness while retaining every equality case. See
\formalref{ElevenSquare/Simplified/InventoryTree.lean}{\repo{InventoryTree.lean}}
and its data file.

Write $R_h$ for the region at index $h\in\{0,\ldots,219\}$ in that
fixed list, and $\ell_k(h)$ for its $k$th label. These indices refer to
overlay entries, not to case indices or square labels.

\subsection{Four elementary collision bounds}

The simplified formal proof uses four unordered pairs of overlay indices:
\begin{equation}\label{eq:fourpairs}
 \{13,26\},\quad\{92,172\},\quad\{193,206\},\quad\{47,127\}
\end{equation}
The following rational rectangles contain the corresponding regions:
\begin{center}
\begin{tabular}{rcc}
\toprule $h$ & $x$ interval & $y$ interval\\\midrule
13 &$[23/50,27/50]$ &$[0,11/100]$\\
26 &$[11/25,14/25]$ &$[23/100,7/25]$\\
92 &$[18/25,77/100]$ &$[11/25,14/25]$\\
172 &$[89/100,1]$ &$[23/50,27/50]$\\
193 &$[11/25,14/25]$ &$[18/25,77/100]$\\
206 &$[23/50,27/50]$ &$[89/100,1]$\\
47 &$[0,11/100]$ &$[23/50,27/50]$\\
127 &$[23/100,7/25]$ &$[11/25,14/25]$\\\bottomrule
\end{tabular}
\end{center}
Each rectangle bound is certified by nonnegative combinations of the
original halfplanes in \cref{eq:overlay}; these finite combinations are
given in
\formalref{ElevenSquare/Simplified/FourCollisionGeometry.lean}{\repo{FourCollisionGeometry.lean}}.
For the first pair, any two points in the two rectangles differ in
$x$ by at most $1/10$ and in $y$ by at most $7/25$. The other three
pairs give these same bounds, possibly exchanged. Consequently
\begin{equation}\label{eq:fourdistance}
 \norm{z-z'}^2\leq\frac1{100}+\frac{49}{625}
   =\frac{221}{2500},\qquad
 (U-1)^2\frac{221}{2500}<1
\end{equation}
Two distinct physical centers therefore cannot occupy both regions of
any pair in \cref{eq:fourpairs}.

\subsection{The finite incompatibility and its geometric consequence}

Let $\mathcal B$ be the set of six raw masks consisting of
$J_{999},J_{1462},J_{1659}$ and their half turns. A \emph{compatible
selection} is a choice of eleven overlay indices $h_i$ such that, for
each view $k$, the eleven labels $\ell_k(h_i)$ are distinct and their
set belongs to $\mathcal B$, and no two chosen indices form a pair in
\cref{eq:fourpairs}.

\begin{certified}[Finite incompatibility]\label{cert:finite-symmetry}
There is no compatible selection.
\end{certified}

This statement involves a finite set of integers only. One exhaustive
procedure chooses a mask from $\mathcal B$ in each of the four views
($6^4=1296$ choices). For each cell in the first-view mask, list all
overlay entries with that first label and other labels in the three
chosen masks. Choose an entry for each of the eleven cells, rejecting
repeated labels or a blocked pair. Empty domains close a branch; all
choices must be exhausted. The source
\formalref{ElevenSquare/Simplified/FourCollisionFinite.lean}{\repo{FourCollisionFinite.lean}}
proves the instance, using the sound finite-refutation machinery in
\formalref{ElevenSquare/Simplified/FiniteRefutation.lean}{\repo{FiniteRefutation.lean}}.
Failure to finish a search is not acceptance. The project supplement
also exhausts this small finite instance.

\begin{theorem}[Symmetry reduction]\label{thm:symmetry}
Every packing of eleven unit squares in $[0,U]^2$ has a $D_4$ image
admitting the raw mask $J_{438}$.
\end{theorem}
\begin{proof}
Suppose no image admits $J_{438}$. No image admits $HJ_{438}$ either,
since another half turn would give $J_{438}$. By
\cref{cert:exclusions}, every assignment of every image has canonical
mask in $\mathcal C$. It follows that every raw assignment of every
image has its mask in $\mathcal B$.

For each actual center choose a containing cell in each of the four
views. By \cref{lem:capacity}, the labels are distinct within each
view. Their quadruple belongs to the exhaustive overlay list. The
resulting eleven indices avoid every pair in \cref{eq:fourpairs} by
\cref{eq:fourdistance} and center separation. They are therefore a
compatible selection, contrary to \cref{cert:finite-symmetry}.
\end{proof}

The original Python bridge used 1,572 strict distance bans obtained from
all relevant overlay vertex pairs. Four are sufficient in the current
formal proof. Both arguments depend on the noncandidate exclusion theorem;
neither is an independent proof that four candidate masks suffice.
\section{Local isolation by a common cone and weighted duals}\label{sec:local}

We now prove the analytic mechanism that rules out a different packing
sufficiently close to the construction in the fixed container $[0,T]^2$.
Proximity is not assumed globally: \cref{sec:capture} establishes it for
the remaining case. This section uses physical unit-length coordinates.

\subsection{Perturbations, corners, and separation gaps}

Let $p_i^0,a_i^0$ be the centers and chosen axes of the construction,
with labels $0,\ldots,10$ as in \cref{prop:construction}. Let
$J(x,y)=(-y,x)$, and let $R_\theta$ be rotation through $\theta$
radians. A perturbation is a vector $h\in\R^{33}$, with
\begin{equation*}
 v_i=(h_{3i},h_{3i+1}),\qquad \omega_i=h_{3i+2},\qquad
 p_i(h)=p_i^0+v_i,\quad a_i(h)=R_{\omega_i}a_i^0
\end{equation*}
Its square corners are $p_i^0+v_i+R_{\omega_i}q_{i,m}$, where
$q_{i,m}=(\epsilon_1a_i^0+\epsilon_2Ja_i^0)/2$ and the four sign
pairs $(\epsilon_1,\epsilon_2)$ are, in the source's corner order
$m=0,1,2,3$, respectively $(-1,-1),(1,-1),(1,1),(-1,1)$.

A \emph{separation feature} for two squares chooses an owner $o$ of
the separating axis, the other square $p$, one of the two unit axes
$n\in\{a_o^0,Ja_o^0\}$, and a sign $\epsilon\in\{-1,1\}$.
Define its four corner gaps by
\begin{equation}\label{eq:gap}
 g_m(h)=\epsilon\inner{R_{\omega_o}n}
 {p_p^0-p_o^0+v_p-v_o+R_{\omega_p}q_{p,m}}-\frac12
\end{equation}
This feature gives weak separation exactly when all four gaps are
nonnegative. Each unordered pair has eight features. By
\cref{lem:SAT}, a feasible pair has at least one such feature; it is
not required to satisfy all eight.

For a corner $(x,y)$ the four wall gaps are $x$, $T-x$, $y$, and
$T-y$. A local packing is feasible if its perturbed squares satisfy
all wall conditions and every pair has a separating feature.
All these elementary gaps are differentiable functions of all orders,
because they are built from affine functions, sine, and cosine.

The local calculation uses the following fourteen pairs that touch in
the reference configuration:
\begin{equation*}
\begin{split}
 &(0,6),(1,9),(2,8),(2,10),(3,4),(3,5),(4,5)\\
 &(4,8),(5,6),(6,7),(6,8),(7,9),(8,9),(9,10)
\end{split}
\end{equation*}
Other pair conditions can be omitted when deriving necessary conditions.
The listed pairs need not remain in contact after perturbation; they
still must be separated.

\subsection{A quantified Taylor estimate}

Fix positive radii $r_0,\ldots,r_{32}$ and the closed rectangle
\begin{equation}\label{eq:rectangle}
 \mathcal R=\{h\in\R^{33}:|h_j|\leq r_j\text{ for }0\leq j\leq32\}
\end{equation}
The actual rational radii are given in \cref{tab:radii}. Angles here are
in radians, not half-angle parameters.

For a gap $g$, its \emph{gradient} at zero is the row vector
$a=(\partial_0g(0),\ldots,\partial_{32}g(0))$, so that $a h$
means $\sum_j a_jh_j$. A \emph{curvature bound} $K_g$ will mean a
nonnegative number for which
\begin{equation}\label{eq:taylor}
 |g(\tau v)-g(0)-\tau av|\leq\frac{K_g\tau^2}{2}
 \quad(v\in\mathcal R,\ 0\leq\tau\leq1)
\end{equation}
This is a bound along every radial line, not a claim that the intervening
configurations are feasible.

The formal proof derives such bounds using an elementary trigonometric
profile. To avoid confusing its parameter with the half-angle parameter,
write the line parameter as $\tau$.

\begin{lemma}[Trigonometric Taylor bound]\label{lem:trig}
For constants $a,b,c,d,w\in\R$, put
\begin{equation*}
 f(\tau)=(a+b\tau)\cos(w\tau)+(c+d\tau)\sin(w\tau)
\end{equation*}
Then $f(0)=a$, $f'(0)=b+wc$, and on $0\leq\tau\leq1$,
\begin{equation*}
 |f''(\tau)|\leq
 |2wd-w^2a|+w^2|b|+|-2wb-w^2c|+w^2|d|
\end{equation*}
If $|a|+|c|\leq A$, $|b|+|d|\leq V$, and $|w|\leq W$,
the right side is at most $(A+V)W^2+2VW$.
\end{lemma}
\begin{proof}
Differentiate twice to obtain
\begin{align*}
 f''(\tau)={}&(2wd-w^2a-w^2b\tau)\cos(w\tau)\\
 &+(-2wb-w^2c-w^2d\tau)\sin(w\tau)
\end{align*}
Use $|\sin|,|\cos|\leq1$, $0\leq\tau\leq1$, and the triangle
inequality. Grouping the $w^2$ and $2|w|$ terms gives the last bound.
Taylor's theorem with the integral remainder then gives
$|f(\tau)-f(0)-\tau f'(0)|\leq K\tau^2/2$ for either stated
second-derivative bound $K$.
\end{proof}

For a direction $v\in\mathcal R$, write its translations as $v_i$
and angular entries as $w_i$ within this paragraph. In a pair gap let
$D=p_p^0-p_o^0$ and $V_0=v_p-v_o$. The expression before its sign
and constant in \cref{eq:gap} is a sum of two profiles of the form in
\cref{lem:trig}, with coefficient lists
\begin{align*}
 &(\inner{D}{n},\inner{V_0}{n},\inner{D}{Jn},\inner{V_0}{Jn},w_o)\\
 &(\inner{q_{p,m}}{n},0,\inner{Jq_{p,m}}{n},0,w_p-w_o)
\end{align*}
This follows by expanding the two rotations and using
$R_{w_o\tau}n\cdot R_{w_p\tau}q=n\cdot R_{(w_p-w_o)\tau}q$.
For example, valid uniform constants are
\begin{align*}
 W_i&=r_{3i+2}\\
 A&=|\inner{D}{n}|+|\inner{D}{Jn}|\\
 V&=(|n_1|+|n_2|)(r_{3p}+r_{3o}+r_{3p+1}+r_{3o+1})\\
 C&=|\inner{q_{p,m}}{n}|+|\inner{Jq_{p,m}}{n}|\\
 K_g&=(A+V)W_o^2+2VW_o+C(W_p+W_o)^2
\end{align*}
For a wall gap of square $i$, a valid bound is
$(|q_{i,m,1}|+|q_{i,m,2}|)W_i^2$; its translation term is affine
and has zero second derivative. These are the coefficient-based bounds
proved in
\formalref{ElevenSquare/Tasks/T06/AnalyticPairs.lean}{\repo{AnalyticPairs.lean}}
and \formalref{ElevenSquare/Tasks/T06/AnalyticWalls.lean}{\repo{AnalyticWalls.lean}}.
Their rational majorants are checked against the exact algebraic
construction. Historical curvature estimates in \cite{focused} use a
different formula; the present argument follows the formal dependency path.

\subsection{Complete feature coverage near the construction}

\begin{certified}[Unavailable features and branch coverage]\label{cert:local-cover}
Among the $14\cdot8=112$ contact features, 88 have a chosen corner gap
for which
\begin{equation}\label{eq:negative}
 g(0)+\sum_j|\partial_jg(0)|r_j+K_g/2<0
\end{equation}
The remaining 24 features yield 512 possible selections, reduced to
128 derivative branches. Each branch consists of 42 rows drawn from a
fixed list of 56 gradient rows. Every feasible $h\in\mathcal R$
has a branch such that each of its rows is the gradient of an elementary
gap $g$ with $g(0)=0$ and $g(h)\geq0$.
\end{certified}

Indeed \cref{eq:taylor,eq:negative} keep the selected negative gap
negative on the entire closed rectangle, so none of those 88 features
can separate a feasible pair. Of the fourteen pairs, six have one
remaining feature, seven have two, and one has four; hence
$1^6 2^7 4=512$ selections before equal derivative descriptions are
identified. The finite enumeration is proved by
\formalref{ElevenSquare/Simplified/LocalAliasCover.lean}{\repo{LocalAliasCover.lean}}
and \formalref{ElevenSquare/Simplified/LocalBranchCover.lean}{\repo{LocalBranchCover.lean}}.

Different nonlinear gaps can have the same zero value and gradient at
the reference packing. Such gaps are called \emph{aliases} of a row.
Equal gradients do not make the functions equal. The branch theorem
supplies a nonnegative alias for each selected row, and its curvature
bound must cover \emph{every} alias that may be selected. With this
convention, if $h=\tau v$ and $v\in\mathcal R$, the selected row
$a$ satisfies
\begin{equation}\label{eq:quadratic-row}
 ah\geq-\tau^2 K/2
\end{equation}
by \cref{eq:taylor}. This step uses feasibility at $h$ only.

\subsection{Replacing 128 branches by forty common inequalities}

The current proof extracts the same forty necessary inequalities from
every branch. Thirty are branch-independent rows. The other ten arise
in pairs from five parallel contacts. At such a contact either square
may own the separating axis and supply the branch's two rows. For either choice, each
target common row is a convex combination
\begin{equation}\label{eq:combo}
 a_{\rm target}=\alpha a_{\rm first}+(1-\alpha)a_{\rm second},
 \qquad0\leq\alpha\leq1
\end{equation}
Twenty exact identities suffice: two targets for each of five contacts,
for each of two choices. The coefficients are explicit rational
polynomials in $u$ and their bounds are certified using an isolating
interval. Nonnegative combinations preserve \cref{eq:quadratic-row};
using a curvature majorant for both source rows supplies a valid bound
for the common row. The two rows for one corner contact are simply
dropped, which weakens the necessary system and is therefore safe.

\begin{certified}[Common-row system]\label{cert:common}
The pinned data specify a matrix $A\in\R^{40\times33}$ and
nonnegative rational bounds $K_0,\ldots,K_{39}$ such that every feasible
$h\in\mathcal R$ satisfies
\begin{equation}\label{eq:common}
 A_i h\geq-\tau^2K_i/2\quad(0\leq i<40)
\end{equation}
whenever $0<\tau\leq1$ and $|h_j|\leq\tau r_j$ for all $j$.
Here $A_i$ is row $i$ of $A$.
\end{certified}

The rows are gradients of the gaps just defined; their indices and
convex-combination choices are given in \cref{app:common}. The exact
identities and curvature transport are proved in
\formalref{ElevenSquare/Simplified/LocalCommonCone.lean}{\repo{LocalCommonCone.lean}}
and \formalref{ElevenSquare/Simplified/LocalCommonBranchCone.lean}{\repo{LocalCommonBranchCone.lean}}.
The term \emph{cone} refers here to the nonnegative combinations of
linear rows. The actual necessary estimates \cref{eq:common} retain
their quadratic remainder; a first-order rigidity assertion alone would
not establish the result.

\subsection{The weighted dual criterion and its proof}

Let $e_j$ be the $j$th standard coordinate row in $\R^{33}$. A
\emph{dual certificate} for $(j,\sigma)$, with $\sigma\in\{-1,1\}$,
is a vector of nonnegative rational weights $w_i$, $0\leq i<40$,
that nearly expresses $\sigma e_j$ as a combination of the common
rows. Define its weighted residual and curvature total by
\begin{equation}\label{eq:dual}
 E_{j,\sigma}=\sum_{k=0}^{32}r_k
       \left|\sum_{i=0}^{39}w_i A_{ik}-\sigma\delta_{jk}\right|,
 \qquad M_{j,\sigma}=\sum_{i=0}^{39}w_iK_i
\end{equation}
Here $\delta_{jk}$ is one when $j=k$ and zero otherwise. Weighting the
error by the actual coordinate radii is part of the certificate.

\begin{certified}[Sixty-six strict margins]\label{cert:duals}
For every $j=0,\ldots,32$ and both signs there are such weights and a
verified rational upper bound $\overline E_{j,\sigma}$ on
$E_{j,\sigma}$ satisfying
\begin{equation}\label{eq:dual-margin}
 \overline E_{j,\sigma}+\frac12M_{j,\sigma}<r_j
\end{equation}
\end{certified}

The finite arithmetic is made explicit in \cref{app:common}. In
particular the supplement independently checks all 66 integer margin
inequalities. The formal proofs also establish that the interval matrix
and curvature data bound the actual gradients and remainders.

\begin{theorem}[Local isolation]\label{thm:isolation}
The only feasible perturbation in $\mathcal R$ in the fixed
$T$-container is $h=0$.
\end{theorem}
\begin{proof}
Suppose $h\ne0$, and set
\begin{equation*}
 \tau=\max_{0\leq k<33}\frac{|h_k|}{r_k}
\end{equation*}
Positivity of the radii and $h\in\mathcal R$ give $0<\tau\leq1$.
Choose $j$ attaining the maximum and $\sigma$ opposite to the sign
of $h_j$. Then $-\sigma h_j=|h_j|=\tau r_j$.
Use the certificate for $(j,\sigma)$ and put
$b=\sum_iw_iA_i-\sigma e_j$. Since $|h_k|\leq\tau r_k$,
\begin{equation*}
 |bh|\leq\tau E_{j,\sigma}\leq\tau\overline E_{j,\sigma}
\end{equation*}
Nonnegative combination of \cref{eq:common} gives
$(\sum_iw_iA_i)h\geq-\tau^2M_{j,\sigma}/2$. Therefore
\begin{align*}
 \tau r_j=-\sigma h_j
 &=bh-\left(\sum_iw_iA_i\right)h\\
 &\leq\tau\overline E_{j,\sigma}+\tau^2M_{j,\sigma}/2\\
 &\leq\tau(\overline E_{j,\sigma}+M_{j,\sigma}/2)
 <\tau r_j
\end{align*}
The second-to-last step uses $M_{j,\sigma}\geq0$ and $\tau\leq1$;
the last uses \cref{eq:dual-margin}. This contradiction proves $h=0$.
\end{proof}

This proof includes points on the rectangle's boundary. It neither
assumes an unchanged contact graph nor confuses infinitesimal rigidity
with finite local isolation. The formal endpoint is
\formalref{ElevenSquare/Simplified/LocalCommonIsolation.lean}{\repo{construction_locally_isolated}}.
\section{Capturing case 438 and completing the lower bound}\label{sec:capture}

Local isolation only concerns the rectangle $\mathcal R$. To use it
globally, every remaining packing must be brought into that same
rectangle, with the same square labels and the same fixed $T$-container.
This section supplies that missing link.

\subsection{Retaining the original container size}

Say a packing in $[0,U]^2$ is \emph{centered in side $s$} if every
point $(x,y)$ of every square satisfies
\begin{equation}\label{eq:centered}
 |x-U/2|\leq s/2,\qquad |y-U/2|\leq s/2
\end{equation}
The embedding in \cref{sec:voronoi} has this property. Every symmetry
about the center of the $U$-container preserves it. Thus after applying
\cref{thm:symmetry}, a hypothetical smaller packing still occupies a
centered square of its original side $s$.

The owner labels in a case-438 trace are cell labels. In contrast, the
local theorem uses the eleven construction labels from
\cref{prop:construction}. Relabel the owners so that the square of
construction role $i$ has cell
\begin{equation}\label{eq:rolecells}
 (j_0,\ldots,j_{10})=(3,15,8,0,4,1,2,11,9,10,13)
\end{equation}
This is a permutation of $J_{438}$, so an injective assignment provides
the required relabeling. It does not change any physical square. The
formal correspondence is
\formalref{ElevenSquare/Tasks/T07/RoleAssignmentFinite.lean}{\repo{roleCell}}.

\begin{figure}[!htbp]
\centering
\includegraphics[width=.53\textwidth]{figures/candidate-438.pdf}
\caption{The eleven occupied cells in $J_{438}$. Occupancy specifies
regions for centers, not fixed center locations or fixed orientations.}
\end{figure}

\subsection{Four closed branches}

Let $y_{15}$ be the \emph{centered physical} vertical coordinate of the
square assigned to cell 15: if its field ordinate is $y_f$, then
$y_{15}=y_f/B-U/2$. Let $t_{13}$ and $t_2$ be the half-angle
parameters of the owners assigned to cells 13 and 2. The subscripts
here are cell labels, not construction roles. The following branches
cover all possibilities:
\begin{align}
 \mathsf F_{15}:&\quad y_{15}\leq5/4\label{eq:branches}\\
 \mathsf F_{13}:&\quad y_{15}\geq5/4,\quad t_{13}\leq147/512\nonumber\\
 \mathsf F_2:&\quad y_{15}\geq5/4,\quad t_{13}\geq147/512,
                           \quad t_2\leq183/512\nonumber\\
 \mathsf N:&\quad y_{15}\geq5/4,\quad t_{13}\geq147/512,
                           \quad t_2\geq183/512\nonumber
\end{align}
The proof of coverage is successive application of $x\leq c$ or
$x\geq c$. Neighboring branches overlap at equality. In field
coordinates the first threshold is exactly
\begin{equation*}
 B(U/2+5/4)=\frac{121802296569435750786621}
                         {38770835900228141773100}
\end{equation*}
Using $5/4$ as a normalized or field ordinate would describe a different
and incorrect subdivision.

\begin{certified}[Complete case-438 capture]\label{cert:capture}
Starting from genuine closed-cell occupancy of $J_{438}$, the verified
geometric traces exclude $\mathsf F_{15},\mathsf F_{13},\mathsf F_2$.
The trace in $\mathsf N$ retains every feasible pose and ends in the
near-state outer cover used by the local-coordinate verification. After
the role permutation \cref{eq:rolecells} and the rigid transformation
below, every packing centered in side $s\leq T$ has a perturbation
$h\in\mathcal R$.
\end{certified}

These are instances of the invariant and trace soundness in
\cref{prop:trace}. They start from the cell seeds, rather than from an
assumption of proximity to the construction. The formal chain is
\formalref{ElevenSquare/Tasks/T07/Ext/Case438.lean}{\repo{role_near_box_state}},
followed by
\formalref{ElevenSquare/Tasks/T07/ConditionalGlobal.lean}{\repo{role_near_box_to_case438_certificate}}.
The historical endpoint data contain 136 live closed angular rows and
1,542 center vertices. Their mathematical role is an outer pose
inclusion; their number by itself has no force.

\subsection{The exact change to local coordinates}

Write $Q(x,y)=(-y,x)$. For a field center $p_f$, its corresponding
positive $T$-frame center is
\begin{equation}\label{eq:transport}
 p_T=Q^{-1}\left(\frac{p_f}{B}-(U/2,U/2)\right)+(T/2,T/2)
\end{equation}
Dividing by $B$ undoes the field scaling. What remains is a rigid
rotation and translation of physical unit squares. The term involving
$U$ and $T$ keeps the container centers aligned exactly; it cannot be
dropped because the two sides happen to be numerically close.
Property \cref{eq:centered} becomes
\begin{equation}\label{eq:smallT}
 |(p_T)_1-T/2|\leq s/2,\qquad |(p_T)_2-T/2|\leq s/2
\end{equation}
for every transformed square point (the same affine formula applies
to all points). Since $s\leq T$, the transformed packing is in
$[0,T]^2$, while retaining the stronger side-$s$ restriction.

To check the center entries of $h\in\mathcal R$, it suffices to
bound \cref{eq:transport} at every vertex of every nonempty residual
polygon: each coordinate is affine. Angles require their own argument.
The inverse quarter turn changes an axis angle by $-\pi/2$, but does
not change a square's orientation modulo $\pi/2$. We choose equivalent
axis representatives before comparing the row parameter with the
construction's orientation.
If an axis-aligned construction square has a row $[a,b]$ near $t=0$,
then $|\Delta\theta|\leq2b$. For a row near $t=1$, choose the
equivalent axis obtained by a quarter turn. Its half-angle parameter is
$(t-1)/(t+1)$, giving
\begin{equation*}
 |\Delta\theta|\leq\frac{2(1-a)}{1+a}
\end{equation*}
For a tilted construction square with parameter $u\in[u_-,u_+]$
and a nonnegative row $[a,b]$, the mean value theorem gives
\begin{equation}\label{eq:anglebound}
 |\Delta\theta|\leq
 \frac{2\max(|a-u_+|,|b-u_-|)}{1+\min(a,u_-)^2}
\end{equation}
Indeed $\theta(t)=2\arctan t$ has derivative $2/(1+t^2)$, and the
displayed minimum bounds the entire interval joining $t$ to $u$.
These estimates cover full closed intervals, including both chart seams.
They never identify a half-angle parameter with an angle in radians.

\subsection{The final contradiction}\label{sec:conclusion}

\begin{proof}[Proof of \cref{thm:main}]
The construction in \cref{prop:construction} proves $T\in\mathcal A_{11}$.
Suppose that some $s<T$ belongs to $\mathcal A_{11}$. Embed its packing
in the centered $U$-container. The cover reduction and
\cref{cert:exclusions} leave only the four candidate masks.
By \cref{thm:symmetry}, some symmetry of the packing admits $J_{438}$;
it is still centered in side $s$.

Apply \cref{cert:capture}. The three far branches are impossible, and
the near branch, with \cref{eq:transport}, gives a feasible perturbation
$h\in\mathcal R$ in $[0,T]^2$, retaining \cref{eq:smallT}.
By \cref{thm:isolation}, $h=0$. The transformed packing is therefore
the exact construction. That construction contains $(T,0)$, so the
first inequality in \cref{eq:smallT} gives $T/2\leq s/2$.
This contradicts $s<T$.

No smaller side is admissible, and $T$ itself is admissible. Hence the
minimum side is exactly $T$.
\end{proof}

No compactness argument or passage to a limit is used. The proof excludes
each putative smaller packing directly. It does not assert that case
438 is infeasible at the larger cap $U$, nor does the public optimality
statement classify all optimal packings up to symmetry.
\section{Formal statements, provenance, and verification scope}\label{sec:formal}

\subsection{The public theorem and its mathematical meaning}

The Lean object \repo{UnitSquare} consists of a center and an arbitrary
real unit axis. The predicate \repo{Packing n S} assumes precisely
closed-square containment and disjoint open interiors, together with
$S\geq0$. Center separation, the cell cover, and finite case reduction
are conclusions, not extra input assumptions. The public theorem is
\begin{quote}\ttfamily\small
optimal\_side\_lower\_bound \{S : R\} (h : Packable 11 S) : T <= S
\end{quote}
with \repo{R} in this display denoting Lean's real-number type. Its
companion \repo{optimality} combines this bound with
\repo{construction_packable}. Both occur in
\formalref{ElevenSquare/Optimality.lean}{\repo{ElevenSquare/Optimality.lean}}.
They are unconditional theorem statements in the published development;
the finite certificate checks are dependencies of their proofs.

The following table gives entry points for the main implications. Paths
are relative to \repo{11SquaresFormalized}; links are pinned to the
snapshot cited in the bibliography.
\begin{longtable}{@{}p{.31\textwidth}p{.65\textwidth}@{}}
\toprule Mathematical role & Source entry point\\\midrule
\endhead
Packing model and elementary geometry &
\formalref{ElevenSquare/Geometry.lean}{\repo{ElevenSquare/Geometry.lean}};
\formalref{ElevenSquare/BasicGeometry.lean}{\repo{BasicGeometry.lean}}\\[4pt]
Endpoint and attaining construction &
\formalref{ElevenSquare/Endpoint.lean}{\repo{ElevenSquare/Endpoint.lean}};
\formalref{ElevenSquare/Construction.lean}{\repo{Construction.lean}}\\[4pt]
Closed cover and canonical masks &
\formalref{ElevenSquare/Cover.lean}{\repo{ElevenSquare/Cover.lean}};
\formalref{ElevenSquare/Combinatorics.lean}{\repo{Combinatorics.lean}}\\[4pt]
Exact exclusion partition &
\formalref{ElevenSquare/Pending/S06_ExclusionPartition.lean}{\repo{Pending/S06_ExclusionPartition.lean}}\\[4pt]
All noncandidate exclusions &
\formalref{ElevenSquare/Pending/S06_Inventory.lean}{\repo{Pending/S06_Inventory.lean}}\\[4pt]
Selected field certificates &
\formalref{Sqpack/S11Opt/Simplified/SelectedFields.lean}{\repo{Sqpack/S11Opt/Simplified/SelectedFields.lean}}\\[4pt]
Four-collision symmetry bridge &
\formalref{ElevenSquare/Simplified/FourCollisionBridge.lean}{\repo{Simplified/FourCollisionBridge.lean}}\\[4pt]
Local common-cone isolation &
\formalref{ElevenSquare/Simplified/LocalCommonIsolation.lean}{\repo{Simplified/LocalCommonIsolation.lean}}\\[4pt]
Complete case-438 ancestry &
\formalref{ElevenSquare/Tasks/T07/Ext/Case438.lean}{\repo{Tasks/T07/Ext/Case438.lean}}\\[4pt]
Centered capture interface &
\formalref{ElevenSquare/Tasks/T07/GlobalComposition.lean}{\repo{Tasks/T07/GlobalComposition.lean}};
\formalref{ElevenSquare/Tasks/T07/ConditionalGlobal.lean}{\repo{ConditionalGlobal.lean}}\\[4pt]
Final lower bound &
\formalref{ElevenSquare/Pending/S09_GlobalLowerBound.lean}{\repo{Pending/S09_GlobalLowerBound.lean}};
\formalref{ElevenSquare/Optimality.lean}{\repo{Optimality.lean}}\\\bottomrule
\end{longtable}

The directory name \repo{Pending} and some comments saying
``UNPROVED'' survive from earlier development stages. Current status
must be read from the completed verification report and proof
dependencies, rather than inferred from those historical comments.
Likewise the original \repo{PROOF.md} in \cite{optimal} describes
formalization as future work; it predates the completed formalization.

\subsection{What the verification report establishes}

The repository's October 6 report \cite{verification} records an
accepted run of 7,920 local Lean modules, with zero inventoried
admissions. An \emph{admission} is an asserted proof step left without
its proof, such as Lean's \repo{sorry}; absence of admissions is distinct
from the choice of computational trust model.
The report identifies an upstream verified source commit and the
repository states that its exact proof sources and pinned build
configuration were imported. The pins are Lean 4.34.1 and Mathlib
revision \texttt{d13f23b723b8a846827a245b89c10fc7d3f11612}.

Lean's \emph{kernel} checks ordinary proof terms. Some large, exact
numerical decisions instead use \repo{native_decide}, which evaluates
specified decidable propositions through native compilation. Thus the
reported proof trusts both the kernel and the native compiler, in
addition to the usual logical axioms and computing environment. Geometry,
checker soundness, and proof assembly retain ordinary Lean proofs.
Calling this particular run ``kernel-only'' would be incorrect.

This manuscript was prepared by reading the pinned source and performing
the explicitly listed supplemental computations. We did not carry out
a fresh build of all 7,920 modules. The successful full run is a
repository-reported result, identified by its source and report, rather
than a new run certified by this writing task. The project includes
build instructions for readers who wish to reproduce the full audit.

\subsection{Why the pieces fit together}

The same physical packing passes through all stages. It is first
translated into the rational cap, labeled using closed cells, transformed
by a genuine symmetry, then moved by an exact rigid map to the
algebraic endpoint frame. The remembered centered side bound is never
discarded. The local rectangle applies to that transformed packing,
not to an unrelated numerical approximation.

Similarly, finite certificates are not accepted merely because their
counts add up. Their inputs must match the cells, cap, scales, owner
labels, and antecedents used by their soundness theorems. The global
union uses actual sets of canonical case indices. This is why a local
rigidity theorem, a successful packing search, or a numerical infeasibility
message alone would leave the optimality argument incomplete.
\appendix
\section{Exact sites and local numerical data}

\subsection{The sixteen sites}

In \cref{tab:sites}, the displayed integers $(X_j,Y_j)$ mean
$q_j=(X_j/2000000,Y_j/2000000)$. This common denominator makes the
half-turn identity $q_{15-j}=(1,1)-q_j$ visible. The source is
\formalref{ElevenSquare/CoverData.lean}{\repo{CoverData.lean}}.
\begin{table}[htbp]
\centering
\begin{tabular}{rrr@{\qquad}rrr}
\toprule $j$&$X_j$&$Y_j$&$j$&$X_j$&$Y_j$\\\midrule
0&209982&265837&8&218244&1328948\\
1&746404&91006&9&729486&1167955\\
2&1267243&277512&10&1257689&1374134\\
3&1731123&205608&11&1793819&1199242\\
4&206181&800758&12&268877&1794392\\
5&742311&625866&13&732757&1722488\\
6&1270514&832045&14&1253596&1908994\\
7&1781756&671052&15&1790018&1734163\\\bottomrule
\end{tabular}
\caption{Exact normalized Voronoi sites.}\label{tab:sites}
\end{table}

\subsection{The focused rectangle}

The entries in \cref{tab:radii} are the integer numerators of
$(r_{3i},r_{3i+1},r_{3i+2})$, all with denominator $10^{10}$.
The first two are physical translation radii and the last is an angular
radius in radians. They use construction-role labels.
\begin{table}[htbp]
\centering
\begin{tabular}{rrrr}
\toprule Role $i$ & $10^{10}r_{3i}$ & $10^{10}r_{3i+1}$ & $10^{10}r_{3i+2}$\\\midrule
0&18767167&22176635&22681452\\
1&16360330&13760362&17641130\\
2&8962451&10424794&22681452\\
3&16350530&10683139&15120968\\
4&16348076&13962901&20161291\\
5&12900283&10683060&15120968\\
6&13565580&8248658&35312013\\
7&11182451&6465674&35297932\\
8&9356857&8671199&15099566\\
9&7338775&10335557&40352153\\
10&7680628&32891612&67647473\\\bottomrule
\end{tabular}
\caption{Positive radii of the local isolation rectangle.}\label{tab:radii}
\end{table}
The largest is $0.0067647473<1/64$. It exceeds the older uniform
isolation radius $1/248$. The focused rectangle must therefore be
checked with its own coordinatewise bounds; it does not follow merely
by containment in that older ball.

\subsection{Common rows and entirely integer dual checks}\label{app:common}

Let $a_0,\ldots,a_{55}$ denote the 56 exact derivative-row types in
the local source inventory. Their values are gradients of the specified
gap aliases in \cref{eq:gap} and the wall gaps. The common matrix takes
the rows with indices
\begin{equation*}
 0,1,\ldots,27,30,31,33,53,35,54,37,50,39,49,40,47
\end{equation*}
The first thirty are retained directly. The last ten use the following
alternative source-row pairs and common targets:
\begin{center}
\begin{tabular}{cccc}
\toprule Contact group & Option A & Option B & Common target rows\\\midrule
0&$(32,33)$&$(52,53)$&$(33,53)$\\
1&$(34,35)$&$(54,55)$&$(35,54)$\\
2&$(36,37)$&$(50,51)$&$(37,50)$\\
3&$(38,39)$&$(48,49)$&$(39,49)$\\
4&$(40,41)$&$(46,47)$&$(40,47)$\\\bottomrule
\end{tabular}
\end{center}
For each target and each option, \cref{eq:combo} is a separately
checked identity. The table specifies which identities are needed;
the polynomial coefficients and their interval proofs are in
\formalref{ElevenSquare/Simplified/LocalCommonCone.lean}{\repo{LocalCommonCone.lean}}.

For the numerical dual step, write
\begin{equation*}
 r_k=\frac{R_k}{10^{10}},\quad K_i=\frac{C_i}{10^{12}},\quad
 w_i=\frac{b_i}{1000},\quad \widetilde A_{ik}=\frac{M_{ik}}{10^{12}}
\end{equation*}
Here $R_k,C_i,b_i$ are nonnegative integers, $R_k>0$,
$M_{ik}$ are signed integers, and the source proves
$|A_{ik}-\widetilde A_{ik}|\leq10^{-12}$. The integers $b_i$
depend on the chosen pair $(j,\sigma)$. Therefore
\begin{equation*}
 \overline E_{j,\sigma}=
 \sum_k r_k\left(\left|\sum_iw_i\widetilde A_{ik}
                       -\sigma\delta_{jk}\right|
                         +10^{-12}\sum_iw_i\right)
\end{equation*}
is a valid residual upper bound. Clearing positive denominators in
\cref{eq:dual-margin} yields the integer inequality
\begin{equation}\label{eq:integer-margin}
\begin{split}
 &2\sum_k R_k\left(\left|\sum_i b_iM_{ik}
                   -\sigma\delta_{jk}10^{15}\right|+\sum_i b_i\right)
       +10^{10}\sum_i b_iC_i\\
 &\hspace{35mm}<2\cdot10^{15}R_j
\end{split}
\end{equation}
All 66 inequalities are thus integer comparisons. The data file
\repo{data/common_dual_data.json} contains the matrix, radii,
curvature majorants, dual coefficients, and pinned provenance. The
supplement checks the gradient rounding intervals as well as these
margins. The largest ratio of the left side to the right side in
\cref{eq:integer-margin} is
\begin{equation*}
 \frac{1732516775872644050197}{1792490200000000000000}<1
\end{equation*}
at $j=6$, $\sigma=-1$. The strict rational comparison is the proof;
its approximate value $0.96654$ is only a measure of the margin.

\section{Reproducing the manuscript and the supplementary checks}\label{app:reproduction}

\subsection{Build the paper}

The project is a standard multi-file LaTeX document. From its directory run
\begin{verbatim}
latexmk -pdf -interaction=nonstopmode -halt-on-error main.tex
\end{verbatim}
No shell escape is required. The included vector PDF figures can be
used directly; \repo{scripts/draw_figures.py} regenerates them with
Python and ReportLab. The main file is also suitable for an Overleaf
project with pdfLaTeX selected.

\subsection{Run the smaller exact checks}

The following checkers use Python's standard library, including exact
integer and rational arithmetic. Run them from the project directory:
\begin{verbatim}
python3 scripts/check_supplement.py
python3 scripts/check_four_collisions.py
python3 scripts/check_common_duals.py
python3 scripts/check_d4.py
\end{verbatim}
The first checks root isolation, the displayed construction's 44 vertices
and 55 pair separations, $T<U$, the exact cover bounds, half-turn
symmetry, and the case enumeration. The second checks the current
finite four-collision selection problem. The third checks the common
matrix's polynomial interval bounds and all 66 numerical dual margins.
The fourth independently reconstructs the full overlay geometry and
checks the older conditional bridge using 1,572 distance bans.

These are useful cross-checks, not a standalone replacement for the
entire formal proof. In particular they do not replay the 2,180-case
geometric inventory, the complete capture traces, or all analytic
soundness proofs. The four-collision finite checker uses the supplied
overlay list and blocked-pair semantics as geometric premises. The
dual checker uses the specified curvature majorants; the Lean
development connects them to the actual nonlinear gaps.

\subsection{Reproduce the full formal verification}

Clone \cite{formal}, check out the pinned commit, keep its
\repo{lake-manifest.json} unchanged, and follow the repository's
platform instructions. Its documented Linux entry point is
\begin{verbatim}
bash scripts/run_verification.sh --bootstrap --jobs 2
\end{verbatim}
The final audit must report
\repo{OPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES}, zero admissions,
and the trust model \repo{lean_kernel_and_native_compiler}.
The repository also offers \repo{--fresh} for a full replay.
Compilation progress reaching 100\% is not a substitute for the final
source, dependency, receipt, and axiom audit. The source-only command
\repo{python3 scripts/check_sources.py} is a different, weaker check.

The full repositories and generated proof corpus are external pinned
dependencies rather than bundled copies in this manuscript archive.
The project remains compilable offline; only a full proof replay
requires obtaining those dependencies.
\clearpage
\begingroup\raggedright
\begin{thebibliography}{9}
\bibitem{formal} Queuingtheorydotcom and contributors,
\emph{11SquaresFormalized}, source snapshot
\texttt{cdc746ed907d258057c283aeb6d077cb2c27e349}.
\url{https://github.com/Queuingtheorydotcom/11SquaresFormalized/tree/cdc746ed907d258057c283aeb6d077cb2c27e349}.
\bibitem{optimal} Queuingtheorydotcom and contributors,
\emph{11SquaresOptimal}, source snapshot
\texttt{4262f07c7723428c1725bb757ed06d0c4d28be1a}, especially
\optimalref{PROOF.md}{\emph{PROOF.md}} and its linked evidence sources.
\url{https://github.com/Queuingtheorydotcom/11SquaresOptimal/tree/4262f07c7723428c1725bb757ed06d0c4d28be1a}.
\bibitem{continuum} \emph{Source review: why an unconditional v9 PASS is a continuum case exclusion},
\optimalref{src/evidence/docs/V9_CONTINUUM_SCOPE_REVIEW.md}{source note in \emph{11SquaresOptimal}}.
\bibitem{focused} \emph{A focused rectangle around the eleven-square candidate},
\optimalref{src/evidence/research/global-math/FOCUSED-LOCAL-RECTANGLE.md}{source note in \emph{11SquaresOptimal}}.
\bibitem{verification} \emph{Verification report, October 6, 2026},
\formalref{docs/VERIFICATION_20261006.md}{report in \emph{11SquaresFormalized}}.
\bibitem{credits} \emph{Acknowledgements and provenance},
\formalref{ACKNOWLEDGEMENTS.md}{acknowledgements} and
\formalref{PROVENANCE.md}{provenance} in \emph{11SquaresFormalized};
\optimalref{THIRD_PARTY_NOTICES.md}{third-party notices} in \emph{11SquaresOptimal}.
\end{thebibliography}
\endgroup
\end{document}