\documentclass[11pt]{article}
\usepackage[a4paper,margin=25mm]{geometry}
\usepackage{amsmath,amssymb,amsthm,booktabs,tikz,needspace}
\usepackage[colorlinks=true,urlcolor=blue,citecolor=blue]{hyperref}
\hypersetup{pdftitle={Three-colour cuboids from four-colour cubes},
  pdfauthor={Jason Davies}}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{corollary}{Corollary}
\theoremstyle{remark}
\newtheorem*{remark}{Remark}
\title{Three-colour cuboids from four-colour cubes}
\author{Jason Davies}
\date{November 8, 2026}
\begin{document}
\maketitle

\begin{abstract}
We determine the least number of four-colour cubes that guarantees a cuboid
with monochromatic faces using exactly three colours. Each source uses all
four colours of a fixed palette; only proper rotations are allowed, and
interior faces need not match. For integer side lengths $2\le a\le b\le c$,
the sharp threshold for the corner-and-edge frame is
$\max\{16a-3,4(a+b+c)-16,\lfloor(24c-1)/5\rfloor\}$, and the complete-cuboid
threshold is $\max\{abc,16a-3,\lfloor(24c-1)/5\rfloor\}$.
The three frame bounds arise from colour-bucket capacity, the number of
positions and balanced checkerboards. The upper bound combines corner
containment, a weighted graph selecting edge directions, and Hall's theorem.
For cubic frames the threshold is $16n-3$, with exactly two failing
collections of size $16n-4$. For $n\ge3$ we classify every failure of size
at least $14n$ and count these collections and the inclusion-maximal ones.
The case $n=2$ answers the threshold question in Problem 2 of Berkove,
Eickemeyer and Schulman (2018).
All threshold, stability and counting results are formalised in Lean.
\end{abstract}

\section{Introduction}
Berkove, Eickemeyer and Schulman (BES)~\cite[Problem 2]{BES} ask for the
least number of four-colour cubes that guarantees a choice of eight cubes
forming a three-colour corner solution: a $2\times2\times2$ cube whose
exterior faces are monochromatic and use exactly three colours. Touching
interior faces need not match.
As in BES~\cite[Section 1]{BES}, every source is a unit cube with one colour
on each face and all four colours of one fixed palette present; every
target uses exactly three of them. A
\emph{variety} is a face colouring up to proper rotation.
Collections are multisets of varieties, so repeated copies
are allowed.

We determine the thresholds for every cuboid with sides at least two.
A frame consists of the corner and edge pieces, including each corner once.
For ordered sides $2\le a\le b\le c$, its cardinality is $4(a+b+c)-16$.
Writing $F$ and $G$ for the least inventory sizes guaranteeing a frame and
a complete box, respectively, our general result is
\begin{align*}
 F(a,b,c)&=\max\{16a-3,\;4(a+b+c)-16,\;\lfloor(24c-1)/5\rfloor\},\\
 G(a,b,c)&=\max\{abc,\;16a-3,\;\lfloor(24c-1)/5\rfloor\}
 \qquad\text{(Theorem~\ref{thm:cuboids}).}
\end{align*}
The target may depend on the inventory. Three obstructions explain the
frame formula: the shortest side controls a repeated-colour demand,
the sum of the sides counts positions, and the longest side controls a
checkerboard shortage. A frame needs no spare sources precisely when
$b+c\ge3a+4$ and $c\le5(a+b)-19$.

Cubic targets admit a stronger structural description. Their frame
threshold is $F(n,n,n)=16n-3$ (Theorem~\ref{thm:frames}). Exactly two collections of
$16n-4$ cubes fail: $4n-1$ copies of each of four varieties, one with a
monochromatic corner of each colour, all in the same orientation class.
Reflection or any odd colour permutation exchanges these collections.
Figure~\ref{fig:obstruction} shows the first case, $n=2$.
More generally, every failure of size at least $14n$, for $n\ge3$, is
confined to one ordinary class with bounded buckets
(Theorem~\ref{thm:stability}). Counting pair multiplicities and bucket
slacks gives explicit binomial formulas for a band of failures
(Theorem~\ref{thm:stability-count}). This includes the 32 failures of size
$16n-5$, twenty-four of which cannot be enlarged; the same counts hold
separately at $n=2$ (Theorem~\ref{thm:near}).

Filling the remaining positions gives the complete-cube threshold
$\max\{n^3,16n-3\}$ (Corollary~\ref{cor:full-cubes}). Thus any $n^3$
sources suffice for a complete cube exactly when $n\ge4$: in particular,
any 64 sources build a $4\times4\times4$ cube without spares.

For general complete boxes, the only shapes that can require spare cubes
are rods $2\times2\times c$ and the four boxes
$2\times3\times3$, $2\times3\times4$, $3\times3\times3$ and
$3\times3\times4$ (Corollary~\ref{cor:cuboid-volume}). Rods and strips
$2\times3\times c$ have the same frame threshold, despite their different
cardinalities (Corollary~\ref{thm:thin}). Every complete $2\times4\times c$
box can be assembled from exactly its volume.

For comparison, BES~\cite[Theorem 5]{BES} show that any $12n-16$
four-colour cubes build a four-colour $n$-frame when $n\ge3$. Requiring
exactly three exterior colours raises the sharp threshold to
$16n-3$.\footnote{BES's Table~7 also records the frame number $16n-17$, for
$n\ge4$, for three-colour source cubes building three-colour frames: a
different problem with the same leading coefficient.} Their completion
argument~\cite[Section 1]{BES} gives a four-colour complete cube from any
$n^3$ sources when $n\ge3$; our result guarantees exactly three exterior
colours when $n\ge4$.

Sections~\ref{sec:corners}--\ref{sec:frames} prove the corner threshold,
cube stability and counting results. Section~\ref{sec:cuboids} proves the
general cuboid thresholds from the common geometry and edge facts.

\section{Model and geometric facts}\label{sec:geometry}
Only proper rotations are allowed. Exterior faces must match the target;
interior faces are unrestricted.

A corner type is a cyclically ordered triple of face colours, read
counterclockwise when viewed from outside along the corner's body diagonal.
Equivalently, order the three outward face normals to form a positively
oriented basis. A trichromatic corner has three distinct colours and two
orientations, $abc$ and $acb$. BES~\cite[Section 2]{BES} use clockwise order; our convention
reverses every triple, preserving containment and matching. A source cube
fits a target corner by a proper rotation if and
only if it has the same cyclic corner type: the cyclic alignments of two
corner frames are exactly those realised by proper rotations of the cube.
Only the presence of a corner type on a source matters: a physical copy
occupies one position. Target occurrences remain separate requirements.
For the corner problem ($n=2$), a target is represented by its multiset of
eight corner types. A collection builds a corner solution modelled on that
target exactly when these eight occurrences can be matched to distinct
cubes having the required types.

For distinct colours $a,b,c$, write $Q(a;b,c)$ for a target whose $b$ and $c$
faces are opposite and whose other four faces have colour $a$. Its corner multiset is
$4aab+4aac$. Write $R(a;b,c)$ for the analogous target with $b$ and $c$
adjacent; its corners are
\[
  2aaa+2aab+2aac+abc+acb.
\]
Finally, write $D(a,b,c)$ for the target with opposite pairs $aa,bb,cc$;
it has four corners of each orientation on $\{a,b,c\}$. These three families suffice for the corner argument. Section~\ref{sec:frames}
introduces $U$ for cube stability; Section~\ref{sec:cuboids} uses a different
target $H$ for directional cuboid demands.

\begin{lemma}\label{lem:balance}
In a cube using exactly three colours, the two orientations of a
trichromatic corner occur equally often. If no trichromatic corner occurs,
the cube is $Q(a;b,c)$ for some distinct $a,b,c$.
\end{lemma}
\begin{proof}
For any cube coloured from a palette $\{a,b,c,d\}$, let $\nu(xyz)$ count
corners of cyclic type $xyz$. Read the three directed transitions around
each corner in the chosen cyclic order. Each edge between an $a$ face
and a $b$ face contributes $ab$ at one endpoint and $ba$ at the other,
so the total counts of these transitions agree. Corners with repeated
colours contribute equally to both counts. The remaining contributions give
\begin{equation}\label{eq:edge-balance}
 \nu(abc)-\nu(acb)+\nu(abd)-\nu(adb)=0.
\end{equation}
If only $a,b,c$ occur, the last two terms vanish, proving the balance.

For the second assertion, if a colour $c$ occurs on only one face, its
four neighbours must all have the same colour $a$: a change from $a$ to
$b$ around this face would produce a trichromatic corner. The opposite
face is then the sole $b$ face. Otherwise each colour occurs twice.
If the two $c$ faces are opposite, the four neighbours of either contain
both $a$ and $b$, forcing a change. If they are adjacent, the other three
neighbours form a path containing both $a$ and $b$, since each occurs only
twice. Again a change is forced. Both cases produce a trichromatic corner.
\end{proof}

The target families test complementary constraints:
\begin{center}
\begin{tabular}{ll}
\toprule
Target & Role\\
\midrule
$D$ & Detects the availability of both orientations\\
$Q$ & Bounds the capacity of a colour bucket\\
$R$ & Eliminates minority cubes in the corner case\\
$U$ & Eliminates minority cubes in the cube stability proof\\
$H$ & Supplies directional demands in cuboids\\
\bottomrule
\end{tabular}
\end{center}
The two ordinary classes below supply opposite cyclic orientations. The
balance lemma explains why confining a collection to one class obstructs
all targets with trichromatic corners.

If every corner type of a variety $v$ occurs on a variety $w$, replacing a
copy of $w$ by $v$ cannot create a solution to any target. In particular, it
preserves unsolvability. Table~\ref{tab:reduction} records the reduction.
Face tuples use the order
$+x,-x,+y,-y,+z,-z$. The rows represent the seven orbits under colour
permutations, with rotations already identified. They cover all 68 varieties;
four orbits are retained.

\begin{table}[ht]
\centering
\begin{tabular}{cccc}
\toprule
Representative & Orbit size & Retained type & Replacement\\
\midrule
$001123$ & 6  & checkerboard $C$ & ---\\
$010203$ & 8  & monochromatic-corner $T$ & ---\\
$010213$ & 12 & pair type $P$ & ---\\
$010223$ & 12 & pair type $P$ & ---\\
\midrule
$000123$ & 12 & --- & $001123$\\
$001213$ & 12 & --- & $001123$\\
$010123$ & 6  & --- & $001123$\\
\bottomrule
\end{tabular}
\caption{The 68 varieties reduce to 38.}
\label{tab:reduction}
\end{table}

A reduced variety belongs to bucket $a$ if it has
at least two of the three corner types $aab$ with $b\ne a$.
The reduction, 38 minimal varieties, orientation classes, checkerboards
and buckets below are from BES~\cite[Section 2, Table 8 and Definition 3]{BES};
we count each bucket's seven mirror pairs as fourteen individual varieties.

\begin{lemma}[Finite geometry]\label{lem:geometry}
Every non-retained variety in Table~\ref{tab:reduction} contains the corner
types of a checkerboard, so every variety reduces to one of the 38 retained
varieties. Their bucket incidences are:
\begin{itemize}
\item There are eight $T$ varieties. Each has a repeated colour $a$, corners
  $aaa$ and $aab$ for every $b\ne a$, and belongs only to bucket $a$.
\item The 24 $P$ varieties belong to two buckets, one for each repeated
  colour.
\item The six checkerboards belong to no bucket. Their repeated colours
  occupy opposite face pairs; with repeated colours $a,b$, a checkerboard
  has both orientations on $\{a,b,c\}$ and $\{a,b,d\}$.
\end{itemize}
The 32 ordinary varieties ($T$ and $P$) split into two classes of 16,
corresponding to BES's $K_o$ and $K_m$ (up to interchanging the names).
Every member of a class has exactly the same four trichromatic corner
types, one for each three-element colour set. The two classes have opposite
orientations. In our convention one class has the trichromatic corner set
\[
\Omega=\{012,031,023,132\},
\]
one set of BES's \emph{universal corners}.
Each class contains exactly one $T$ variety for each repeated colour.
Even colour permutations preserve the classes; odd colour permutations and
reflection exchange them.
\end{lemma}
\begin{proof}
The face-colour multiplicities are $3+1+1+1$ or $2+2+1+1$.
In the first case, the three equal faces either meet at a vertex or contain
an opposite pair, giving two orbits. In the second case, both repeated
pairs can be opposite, exactly one can be opposite, or both can be adjacent.
In the last case, the two monochromatic edges either have perpendicular
directions, giving two mirror configurations represented by $010213$ and
$010223$, or are parallel, represented by $010123$. These cases cover all
varieties. The orbit sizes in Table~\ref{tab:reduction} sum to 68, the total
number of varieties~\cite{BES}, so the seven orbits are distinct.
The three non-retained representatives contain the corner types of $001123$;
colour permutations transport these containments to their whole orbits.
Table~\ref{tab:corners} gives the corner sets of the retained representatives.
All three ordinary representatives in Table~\ref{tab:corners} belong
to the class of $\Omega$. Even colour permutations preserve $\Omega$
and odd ones reverse it, with triples read cyclically. Applying colour
permutations to Table~\ref{tab:corners} gives the stated incidences and
orientation classes. The eight $T$ varieties split evenly between the
classes, and even permutations act transitively on the four colours, so
each class contains exactly one $T$ variety for each repeated colour.
Reflection reverses every trichromatic corner.
\end{proof}

\begin{table}[ht]
\centering
\begin{tabular}{cc}
\toprule
Representative & Corner-type set\\
\midrule
$001123$ & $\{012,013,021,031\}$\\
$010203$ & $\{000,001,002,003,012,023,031,132\}$\\
$010213$ & $\{001,003,011,012,023,031,112,132\}$\\
$010223$ & $\{002,003,012,022,023,031,122,132\}$\\
\bottomrule
\end{tabular}
\caption{Corner-type sets of the retained representatives, with cyclic
triples written in lexicographically least form.}
\label{tab:corners}
\end{table}

\Needspace{11\baselineskip}
\begin{lemma}[Bucket bound]\label{lem:bucket}
Eight reduced cubes in bucket $a$ can build a target $Q(a;b,c)$ for some
$b,c$. Consequently, a reduced collection with no $Q$ target has at most
seven cubes in each bucket.
\end{lemma}
\begin{proof}
Each of the eight cubes misses at most one of the three types $aab$.
Thus at most one type is missed by five or more cubes. Choose two types,
$aab$ and $aac$, each missed by at most four cubes. Assign cubes missing
$aac$ to $aab$ positions, and cubes missing $aab$ to $aac$ positions.
These groups are disjoint and each has size at most four. Every remaining
cube has both types, so they fill the remaining positions of
$Q(a;b,c)$.
\end{proof}

\section{The extremal corner collections}\label{sec:corners}
\begin{theorem}\label{thm:classification}
A collection of 28 four-colour cubes that builds no target of type $Q$,
$R$ or $D$ consists of seven copies of each of the four $T$ varieties
in one ordinary orientation class.
\end{theorem}
\begin{proof}
Replace each non-retained cube by a checkerboard using
Lemma~\ref{lem:geometry}, leaving retained cubes unchanged. This preserves
avoidance of all three target families.
Let $A\ge B$ count the cubes belonging to the two ordinary orientation
classes, and let $C$ count checkerboards, so $A+B+C=28$. Call the class with
$A$ cubes the majority class (either one if equal). Call the remaining $M=B+C$ cubes \emph{minority cubes}.
A minority cube \emph{supports} a three-element colour set $E$ if it has
the orientation on $E$ opposite to the majority class. Smaller-class
cubes support every $E$; a checkerboard supports two.

\smallskip\noindent\emph{(i) At most six minority cubes: $M\le6$.}
For $E=\{a,b,c\}$, let $z_E$ count checkerboards supporting $E$.
If $z_E\ge8$, those eight checkerboards build the
target $D(a,b,c)$. Thus $z_E\le7$ for each
$E$, and, since each checkerboard supports two triples, $2C\le28$.
It follows that $A+B\ge14$, so $A\ge7$. There are $m_E=B+z_E$
minority cubes supporting $E$. If $m_E\ge4$, four such cubes and four majority cubes
build $D(a,b,c)$. Hence
$m_E\le3$ for every $E$. Summing gives
\begin{equation}\label{eq:minority}
 4B+2C\le12,\qquad M\le6,\qquad A=28-M\ge22.
\end{equation}

\smallskip\noindent\emph{(ii) No minority cubes: $M=0$.}
Let $t_a$ and $p_a$ count only majority-class $T$ and $P$
cubes in bucket $a$, and let $n_T,n_P$ be their respective totals, so
$A=n_T+n_P$. By Lemma~\ref{lem:bucket}, $t_a+p_a\le7$.
Each $T$ cube belongs to one bucket and each $P$ cube to two. This is BES's
double-count~\cite[equation (1)]{BES}; summing the bucket bounds and using
$n_T+n_P=28-M$ gives
\begin{equation}\label{eq:buckets}
 n_T+2n_P\le28,\qquad n_P\le M.
\end{equation}

We use the following construction. If six majority cubes
supply $2aaa+2aab+2aac$ and a minority cube supports $\{a,b,c\}$, then
the minority cube supplies the opposite trichromatic orientation and an
unused majority cube supplies the other. Such a cube is available since
$A\ge22$. This builds $R(a;b,c)$.

Suppose $M>0$. We claim that $t_a\ge4$ forces $t_a+p_a\le5$. Otherwise
choose six majority cubes in bucket $a$, including at least four $T$ cubes.
Any minority cube supports some triple containing $a$, say $\{a,b,c\}$,
since a checkerboard's two supported triples together contain every colour.
Each of the at most two $P$ cubes has two of the three types $aax$, so it
has $aab$ or $aac$; since $R(a;b,c)$ needs two of each, each $P$ cube can
take a position of a type it has. The $T$ cubes have $aaa$ and every type
$aax$, so they fill the remaining positions of $2aaa+2aab+2aac$, and the
construction above gives a solution, a contradiction. In particular,
$t_a\le5$ for every $a$.

If $t_a\le3$, the bucket bound gives $2t_a+p_a\le t_a+7\le10$.
If $4\le t_a\le5$, the claim gives $2t_a+p_a\le t_a+5\le10$.
Thus $2t_a+p_a\le10$ in all cases. Each majority $T$ cube contributes two
through its single bucket, and each majority $P$ cube contributes one
through each of its two buckets. Summing gives
\[
 2A=2n_T+2n_P=\sum_a(2t_a+p_a)\le40,
\]
contradicting $A\ge22$ from \eqref{eq:minority}. Therefore $M=0$.

\smallskip\noindent\emph{(iii) Equal multiplicities: $t_a=7$.}
With $M=0$, \eqref{eq:buckets} forces $n_P=0$. All 28 cubes are majority-class
$T$ cubes, and the four bucket bounds force each $t_a=7$.

Since the reduced collection contains no checkerboards, no replacement
occurred: the original collection was already reduced.
\end{proof}

\Needspace{5\baselineskip}
\begin{theorem}\label{thm:upper}
Every collection of 29 four-colour cubes contains a three-colour corner
solution.
\end{theorem}
\begin{proof}
Otherwise every 28-cube subcollection would have the form in
Theorem~\ref{thm:classification}. Take one such subcollection $S$ and let
$v$ be the remaining cube. Remove from $S$ a cube of a variety different
from $v$, and insert $v$. The multiplicity of $v$'s variety is now 1 or 8,
whereas every variety in a collection described by
Theorem~\ref{thm:classification} has multiplicity 0 or 7, a contradiction.
\end{proof}

\Needspace{0.8\textheight}
\section{Sharpness}
\begin{figure}[ht]
\centering
\input{obstruction-figure}
\caption{Why one exceptional 28-cube collection fails for three-colour targets. (A) Seven copies of each
variety, with monochromatic corners marked. (B) Targets with a trichromatic
corner need both orientations; the example's bottom face is hidden. (C) Targets without
trichromatic corners require eight cubes with the same repeated colour,
but only seven are available; $a,b,c$ are distinct. Reflection gives the
other obstruction.}
\label{fig:obstruction}
\end{figure}
\Needspace{16\baselineskip}
\begin{theorem}\label{thm:sharp}
The threshold 29 in Theorem~\ref{thm:upper} is best possible. For a fixed
palette, exactly two 28-cube collections fail, and they are mirror images.
Up to colour permutation, there is a single obstruction.
\end{theorem}
\begin{proof}
Take seven copies of each of the following four face tuples
(Figure~\ref{fig:obstruction}):
\[
 010203,\qquad 011213,\qquad 021223,\qquad 031323.
\]
These are $T$ cubes with repeated colours $0,1,2,3$, respectively, all in
the same ordinary orientation class. A target with any trichromatic corner
requires both orientations by Lemma~\ref{lem:balance}, whereas the
collection supplies only one. A target without one is $Q(a;b,c)$;
every one of its eight corners has colour $a$ twice, so only the seven
$T$ cubes of repeated colour $a$ are usable. No three-colour target is
possible. Reflection gives the analogous example in the other orientation
class. Theorem~\ref{thm:classification} excludes all other collections.
Every odd colour permutation exchanges the two orientation classes and
hence these two collections.
\end{proof}

\begin{remark}[Allowing fewer colours]
If targets may use at most three colours, 28 cubes suffice. In either
exceptional collection, four $T$ cubes of repeated colour $a$ and four of
repeated colour $b$ supply $aaa+3aab+bbb+3bba$. These are the corners of a
two-colour cube whose three $a$ faces meet at one vertex and whose three $b$
faces meet at the opposite vertex. Every other 28-cube collection builds
a three-colour target by Theorem~\ref{thm:sharp}. This gives an upper bound,
not an exact threshold, for that variant.
\end{remark}

\Needspace{12\baselineskip}
\begin{corollary}[Restricted targets]\label{cor:restricted}
Every collection of 29 four-colour cubes, and every solvable collection of
28, builds a target of type $Q$, $R$ or $D$. These families contain just
28 of the 120 target varieties.\footnote{For any fixed three colours, a
rotation with $k$ face cycles fixes $3^k-3\cdot2^k+3$ colourings using all
three. The 24 rotations have $6,4,3,2$ face cycles with multiplicities
$1,3,12,8$, so Burnside's lemma gives
$(540+3\cdot36+12\cdot6)/24=30$ varieties. Four choices of omitted colour
give 120.}
\end{corollary}
\begin{proof}
By Theorems~\ref{thm:classification} and~\ref{thm:sharp}, a 28-cube collection
avoiding these families is unsolvable. The swap in the proof of
Theorem~\ref{thm:upper} rules out a 29-cube collection avoiding them.
There are $4\binom{3}{2}=12$ varieties each of $Q$ and $R$: choose $a$ and
the unordered pair $\{b,c\}$. There are $\binom{4}{3}=4$ varieties of $D$,
one for each three-colour set.
\end{proof}

\Needspace{12\baselineskip}
\begin{remark}
For the palette $\{0,1,2,3\}$, write
$\delta(xyz)=\nu(xyz)-\nu(xzy)$. Applying \eqref{eq:edge-balance} to the
different colour pairs gives
\[
 \delta(012)=\delta(031)=\delta(023)=\delta(132).
\]
This common integer is the cube's \emph{degree}, relative to $\Omega$.
Reflection negates the degree, as does each transposition of colour labels;
thus even colour permutations preserve it and odd ones negate it.
Each ordinary representative in Table~\ref{tab:corners} has eight distinct
corner types, so each occurs once; the two ordinary classes therefore
have degrees $+1$ and $-1$. The checkerboard representative has neither
$023$ nor $032$, so its degree, and that of every checkerboard, is zero.
\end{remark}

\section{Cubic frames: threshold and stability}\label{sec:frames}
An $n$-frame consists of the eight corner cubes and the $n-2$ further cubes
on each of the twelve edges of an $n\times n\times n$ cube. Thus it contains
$L=12n-16$ cubes. Its six exterior faces are monochromatic and use exactly
three colours; face interiors are not part of the frame. This is the frame
model of BES~\cite[Section 1]{BES}, with three target colours instead of four.

\begin{theorem}[Frame threshold and classification]\label{thm:frames}
For every $n\ge2$, every collection of $16n-3$ four-colour cubes contains
a three-colour $n$-frame. For a fixed palette, exactly two collections of $16n-4$ cubes
fail: $4n-1$ copies of each of the four $T$ varieties in one orientation
class, or their reflections. Consequently the sharp frame threshold is
$F(n)=16n-3$.
\end{theorem}

The corner-containment reduction also preserves edge availability: an edge
occurs in a corner, so containment of corner types implies containment of
edge types~\cite[Section 2, after Definition 2]{BES}. An edge type is an
unordered pair of colours, allowing repetition. Every ordinary variety has all six bichromatic edge
types. A checkerboard has five, missing precisely the pair of its singleton
colours; different checkerboards miss different pairs. These facts follow
from the representatives in Table~\ref{tab:corners}, and also appear in
BES's frame arguments~\cite[proofs of Lemmas 7--8 and Table 5]{BES}.
A reduced cube has an $aa$ edge if and only if it belongs to bucket $a$.

\begin{lemma}\label{lem:D-extension}
Let $n\ge2$. A reduced collection with a $D$ corner solution has an $n$-frame
whenever its size $N$ satisfies
\[
 N\ge\max\{12n-16,\,8n-1\}.
\]
\end{lemma}
\begin{proof}
If a checkerboard variety occurs at least $4n$ times, use eight copies for
a supported $D$ corner solution. Its remaining copies supply at least
$4(n-2)$ neighbours for each required edge type. Otherwise every
checkerboard variety occurs at most $4n-1$ times. Remove any $D$ corner
solution. Each of its three bichromatic edge types then has at least
\[
 N-8-(4n-1)\ge4(n-2)
\]
available suppliers. In either case, the union of the supplier sets for
two edge types is the entire residual collection, since no reduced cube
misses two bichromatic types. There are at least $12(n-2)$ remaining
cubes, so Hall's inequalities hold for all edge positions.
\end{proof}

One more target supplies the growing repeated-colour demands. For distinct
$a,b,c$, let $U(a,b;c)$ have face tuple $(a,b,a,b,a,c)$. Its corner and edge
multisets are respectively
\[
 aaa+2aab+aac+abb+bbc+abc+acb,
 \qquad 3aa+bb+4ab+2ac+2bc.
\]
Write $T_a$ for the $T$ variety with repeated colour $a$ in a given ordinary
class. Thus an ordinary class supplies a $U$-frame using $3n-2$ of its $T_a$ cubes,
$n$ of its $T_b$ cubes, and $1+8(n-2)$ other cubes, together with one
minority cube supporting $\{a,b,c\}$. The $T_a$ cubes fill four corners and
the $3(n-2)$ monochromatic $aa$ edge positions; the $T_b$ cubes fill two
corners and the $n-2$ monochromatic $bb$ positions. The minority cube and
one further cube from the same ordinary class fill the two trichromatic corners. Every remaining
edge is bichromatic and can use any ordinary cube.

\begin{theorem}[Stability]\label{thm:stability}
Let $n\ge3$ and $N\ge14n$. A collection of $N$ four-colour cubes fails to
build a three-colour $n$-frame if and only if all its cubes are ordinary
varieties in one orientation class and each colour bucket contains at
most $h=4n-1$ cubes.
\end{theorem}
\begin{proof}
Reduce a failing collection as before. Let $A\ge B$ count the two ordinary
classes, let $C$ count checkerboards, and put $M=B+C$. Write $t_a,p_a,n_T,n_P$
for the majority-class counts. Lemma~\ref{lem:D-extension} excludes a $D$
corner solution. The orientation count from Theorem~\ref{thm:classification}
therefore gives
\[
 4B+2C\le12,\qquad M\le6,\qquad A=N-M\ge14n-6.
\]
A majority bucket of size $4n$ would build a $Q$-frame: eight of its cubes
supply the corners, $4(n-2)$ supply the monochromatic edge positions, and
$8(n-2)$ other majority cubes supply the bichromatic positions. There are
enough since $A\ge12n-16$. Thus
\[
 t_a+p_a\le h,\qquad n_T+2n_P\le4h,\qquad
 n_T\ge2N-4h-12\ge12n-8.
\]
Some $t_a\ge3n-2$. At most one colour has fewer than $n$ majority $T$ cubes,
since two such colours would give
\[
 n_T\le2(n-1)+2h=10n-4<12n-8.
\]
If $M>0$, a minority cube supports a triple containing $a$ and another
colour $b$ with $t_b\ge n$. The $U(a,b;c)$ construction then applies.
After its $4n-1$ majority corner and monochromatic-edge cubes have been
selected, at least $A-(4n-1)\ge10n-5\ge8(n-2)$ ordinary cubes remain.
This contradiction gives $M=0$. No checkerboards remain, so the reduction
made no replacements in the original collection.

Conversely, one ordinary class cannot supply both orientations of a
trichromatic corner. Lemma~\ref{lem:balance} leaves only $Q$ targets.
Their corners and monochromatic edges require $4n$ cubes from one bucket,
exceeding its capacity $h$.
\end{proof}

\begin{proof}[Proof of Theorem~\ref{thm:frames}]
For $n=2$, use Theorem~\ref{thm:sharp}. For $n\ge3$, apply
Theorem~\ref{thm:stability}. At size $4h$, purity and
$n_T+2n_P\le4h=n_T+n_P$ force $n_P=0$, and all four $T$ multiplicities
equal $h$. Both collections fail by the converse. At size $4h+1$ the
bucket inequalities are impossible, proving the upper bound.
\end{proof}

\begin{theorem}[Counting stable failures]\label{thm:stability-count}
For $n\ge3$ and $0\le d\le2n-4$, exactly
\[
 2\binom{d+15}{15}
\]
fixed-palette collections of $16n-4-d$ cubes fail to build a three-colour
$n$-frame. Exactly $2\binom{d+11}{11}$ of them are inclusion-maximal.
\end{theorem}
\begin{proof}
The size is at least $14n$, so Theorem~\ref{thm:stability} applies. Fix an
orientation class. Write $x_1,\ldots,x_{12}$ for its $P$ multiplicities,
$p_a$ for their incidences in bucket $a$, and
$s_a=h-t_a-p_a$ for the four bucket slacks. Double counting gives
\[
 \sum_{j=1}^{12}x_j+\sum_a s_a=d.
\]
Conversely, any nonnegative solution determines a failing collection by
$t_a=h-p_a-s_a$. These values satisfy $t_a\ge h-d>0$, so there are no
additional feasibility constraints and the two orientation classes give
disjoint collections. Stars and bars, followed by the two choices of
orientation, gives the first count.

A positive slack permits adding the corresponding $T_a$. If all slacks
vanish, adding any ordinary cube in the same class overfills a bucket;
adding any other cube violates purity. The stability theorem applies to
the enlarged collection, so these and only these failures are
inclusion-maximal. Setting the four slacks to zero leaves twelve
nonnegative variables summing to $d$, giving the second count.
\end{proof}

\begin{theorem}[One cube below the extremal size]\label{thm:near}
For every $n\ge2$, exactly 32 fixed-palette collections of $16n-5$ cubes
fail to contain a three-colour $n$-frame. Put $h=4n-1$. They are:
\begin{enumerate}
\item the eight collections
\[
 (h-1)T_a+hT_b+hT_c+hT_d,
\]
one for each choice of ordinary orientation class and colour $a$;
\item the twenty-four collections
\[
 P+(h-1)T_a+(h-1)T_b+hT_c+hT_d,
\]
one for each ordinary $P$ variety, where $a,b$ are its bucket colours
and the four $T$ varieties belong to its orientation class.
\end{enumerate}
Each collection in the second family is inclusion-maximal among failures:
adding any cube makes it solvable.
\end{theorem}
\begin{proof}
Let $N=16n-5$ and retain the majority notation from the stability proof.
For $n\ge3$, Theorem~\ref{thm:stability} gives $M=0$ immediately.

For $n=2$, the orientation count at $N=27$ gives $M\le6$ and $A\ge21$.
If $M>0$, the $R$ argument in Theorem~\ref{thm:classification} still
implies $2t_a+p_a\le10$ for every colour. Summing yields $2A\le40$,
a contradiction. Thus $M=0$ here too.

Now $n_P\le1$. If $n_P=0$, four bucket capacities of $h$ and total
$4h-1$ leave exactly one $T$ multiplicity at $h-1$, giving the eight
deletion cases. If $n_P=1$, every bucket must have size $h$, since
$n_T+2n_P=4h$. The unique $P$ cube fills two buckets, giving the stated
multiplicities and twenty-four cases. No checkerboards remain, so the
reduction made no replacements in the original collection.

Conversely, each listed collection lies in one ordinary orientation
class. Orientation balance excludes every target with a trichromatic
corner. A remaining target $Q(a;b,c)$ requires $4n$ distinct cubes with
an $aa$ edge for its corners and monochromatic edges, while bucket $a$
has at most $h=4n-1$ cubes. Every listed collection therefore fails.
Finally, adding any cube to a pair case produces a collection of size
$16n-4$ still containing a $P$ cube; Theorem~\ref{thm:frames} excludes it
from the failing collections of that size.
\end{proof}

\begin{corollary}\label{cor:frame-targets}
For $n\ge3$, every collection of at least $16n-3$ source cubes has an
$n$-frame modelled on one of the 40 targets of types $Q,D,U$.
\end{corollary}
\begin{proof}
The frame counting argument uses only these three types: avoiding them
forces purity and four bucket capacities of $4n-1$, hence at most
$16n-4$ cubes. There are twelve $Q$ targets and four $D$ targets.
The ordered choice of three distinct colours in $U(a,b;c)$ gives
$4\cdot3\cdot2=24$ varieties: their face multiplicities $3,2,1$
recover $a,b,c$, respectively. These families are disjoint.
\end{proof}

\begin{corollary}[Complete cubes]\label{cor:full-cubes}
For every integer $n\ge2$, the sharp threshold for a complete
$n\times n\times n$ cube with exactly three exterior colours is
\[
 G(n)=\max\{n^3,16n-3\}.
\]
In particular, $G(2)=29$, $G(3)=45$, and $G(n)=n^3$ for $n\ge4$.
\end{corollary}
\begin{proof}
Both terms are necessary: an assembly uses $n^3$ pieces, and contains an
$n$-frame. Conversely, construct a frame using Theorem~\ref{thm:frames}.
Each face-interior position prescribes just one colour, which every unused
source cube has; interior positions prescribe none. Thus arbitrary unused
cubes complete the assembly whenever at least $n^3$ pieces are available.
\end{proof}

\input{cuboids}

\section{Formal verification and computation}
All threshold, stability, counting and restricted-target results are
formalised in Lean~4 and mathlib~\cite{Lean4,mathlib}, both at
\texttt{v4.35.0}. The threshold statements quantify over arbitrary indexed
families of physical four-colour cubes. A solution selects distinct copies
and proper rotations matching every exposed face. The classifications and
counts concern multisets of rotation classes over a fixed palette. The
forty-target result uses a checked canonical target index; the threshold
and sharpness statements use no catalogue indices.

The kernel checks the finite geometry, including the equivalence between
corner matching and proper-rotation placement. The allocation and counting
proofs are symbolic in the dimensions. The cuboid lower bounds reuse the
cube and rod obstructions through proved restriction maps, and the counting
proof gives an explicit bijection with weak compositions. Separate geometric
and inventory audits supplement these proofs; their outputs are not assumed
by the formalisation. Appendix~\ref{app:verification} distinguishes the
library proofs from the narrower comparator challenge.

To find an assembly, use capacitated bipartite matching. Source varieties
have capacities equal to their multiplicities; corner and edge types have
capacities equal to their demands. Adjacency records whether a source has
the required type. There are at most eight corner and twelve edge
requirement nodes, regardless of the dimensions. An integral flow meeting
all demands selects the copies; compatible proper rotations then place
them. Unused sources fill the remaining positions when at least the volume
is available.

For cubic frames in the guaranteed range, it suffices to test 28 targets
of types $Q,R,D$ when $n=2$ (Corollary~\ref{cor:restricted}), or 40 of types
$Q,D,U$ when $n\ge3$ (Corollary~\ref{cor:frame-targets}). Testing all 120
target varieties decides feasibility for arbitrary cube inventories.
For a general cuboid, also test the at most six assignments of target axes
to box directions. Proper rotations with the same axis assignment give
the same corner multiset and directional edge demands, so these tests
decide frame feasibility.

\section*{Further questions}
The cuboid thresholds are determined, but their extremal inventories
remain to be classified. In particular, the interaction between the
bucket and checkerboard obstructions may give a cuboid counterpart of
Theorem~\ref{thm:stability}. For cubes, classifying failures below the
stability range remains open.
\Needspace{12\baselineskip}
\section*{Declaration of AI-generated research and review}
GPT-6-Astra (OpenAI), used through Codex, developed the original research
argument, computational search, Lean formalisation and manuscript under
the author's direction. Claude Opus 5.5 (Anthropic), used through Claude
Code, contributed the minority-cube argument, balance proof, further
mathematical simplifications, illustrations and review. Subsequent Codex
revisions incorporated and extended these contributions. Detailed attribution
and review scope are recorded in the repository's \texttt{formalization.yaml}.
The human author initiated and directed the research and accepts responsibility
for the paper's content and the accuracy of this disclosure.

\appendix
\input{verification}

\begin{thebibliography}{9}
\raggedright
\bibitem{BES}
E. Berkove, A. Eickemeyer and M. Schulman,
\emph{The 4-Color Cubes Puzzle}, Integers \textbf{18} (2018), A68.
\href{https://math.colgate.edu/~integers/s68/s68.pdf}{Journal PDF}.
\bibitem{Lean4} L.~de Moura and S.~Ullrich,
\emph{The Lean 4 Theorem Prover and Programming Language},
in Automated Deduction---CADE~28, LNCS \textbf{12699}, Springer (2021),
625--635.
\href{https://doi.org/10.1007/978-3-030-79876-5_37}{doi:\nolinkurl{10.1007/978-3-030-79876-5_37}}.
\bibitem{mathlib} The mathlib Community,
\emph{The Lean Mathematical Library},
in Proceedings of the 9th ACM SIGPLAN International Conference on
Certified Programs and Proofs (CPP~2020), ACM (2020), 367--381.
\href{https://doi.org/10.1145/3372885.3373824}{doi:\nolinkurl{10.1145/3372885.3373824}}.
\href{https://arxiv.org/abs/1910.09336}{arXiv:1910.09336}.
\bibitem{ColourCubes} J.~Davies,
\texttt{colour-cubes-core}: palette-independent Lean definitions and proofs
for face-coloured cubes, Lean library (2026).
Release \href{https://github.com/jasondavies/colour-cubes-core/tree/v1.0.0}{\texttt{v1.0.0}},
\url{https://github.com/jasondavies/colour-cubes-core}.
\end{thebibliography}
\end{document}