\documentclass[11pt]{article} \usepackage[a4paper,margin=25mm]{geometry} \usepackage{amsmath,amssymb,amsthm,booktabs,tikz} \usepackage[colorlinks=true,urlcolor=blue,citecolor=blue]{hyperref} \hypersetup{pdftitle={Sharp thresholds for five-colour cube assemblies},pdfauthor={Jason Davies}} \newtheorem{theorem}{Theorem} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{remark} \newtheorem*{remark}{Remark} \newcommand{\col}{\{0,1,2,3,4\}} \newcommand{\mass}[2]{#1(#2)} \title{Sharp thresholds for five-colour cube assemblies} \author{Jason Davies\thanks{\href{mailto:jason@jasondavies.com}{\nolinkurl{jason@jasondavies.com}}}} \date{November 9, 2026} \begin{document} \maketitle \begin{abstract} We determine the least pool sizes guaranteeing a frame or a complete $a\times b\times c$ box from unit cubes whose faces use all five colours of a fixed palette, for every $a,b,c\ge2$. Proper rotations are allowed; the target has monochromatic exterior faces using all five colours. The frame threshold is $\max\{15,4(a+b+c)-16,2(a+b+c)+1\}$, and the complete-box threshold is $\max\{abc,15,2(a+b+c)+1\}$. The proof combines a certified fifteen-cube corner theorem with elementary Hall arguments and a uniform three-variety obstruction. It completes the five-colour frame column left open by Berkove, Eickemeyer and Schulman (2018). All threshold statements are formalised in Lean. A fixed-size flow formulation decides feasibility and constructs assemblies in time linear in the explicit source list. We also determine the corner thresholds when the number of source varieties is bounded, and classify all fourteen-cube obstructions into 56 classes under common colour relabelling and simultaneous reflection, described by three structural forms. The minimum size of a collection capable of reproducing every $2\times2\times2$ target is also fifteen. \end{abstract} \noindent\small\textit{AI transparency.} The closing disclosure describes the AI contributions; Section~\ref{sec:formal} states the formal verification scope. \normalsize \section{Introduction} MacMahon's coloured-cube puzzles~\cite{MacMahon} ask when a collection of face-coloured cubes can form a larger cube with monochromatic exterior faces. Here every source and target uses all five colours of a fixed palette. Proper rotations identify varieties; reflections are not allowed as moves. Collections may contain repeated varieties, and touching interior faces need not have equal colours. For $a,b,c\ge2$, a \emph{frame} consists of the eight corners and the noncorner positions on the twelve edges of an $a\times b\times c$ box. It has $L=4(a+b+c)-16$ positions. Write $F_5(a,b,c)$ for the least pool size guaranteeing a frame and $G_5(a,b,c)$ for the least pool size guaranteeing a complete box. An assembly may use a subset of the pool; its target colouring may depend on the collection. \begin{theorem}[All cuboid thresholds]\label{thm:all-boxes} For every integer $a,b,c\ge2$, \[ \begin{aligned} F_5(a,b,c)&=\max\{15,4(a+b+c)-16,2(a+b+c)+1\},\\ G_5(a,b,c)&=\max\{abc,15,2(a+b+c)+1\}. \end{aligned} \] \end{theorem} The three frame terms have separate explanations: $15$ comes from the fourteen-cube corner obstruction, $4(a+b+c)-16$ counts frame positions, and $2(a+b+c)+1$ comes from a uniform failing collection of size $2(a+b+c)$. Completion gives the conceptual relation \[ G_5(a,b,c)=\max\{abc,F_5(a,b,c)\}: \] once a frame is built, arbitrary unused sources fill the remaining positions, each of which exposes at most one face. The frame threshold depends only on the sum $s=a+b+c$: it is $15$ for $s=6,7$, $17$ for $s=8$, and the frame's own cardinality $4s-16$ for $s\ge9$. Up to permuting sides, only three complete boxes can require spare sources: $2\times2\times2$, $2\times2\times3$, and $2\times2\times4$, whose thresholds are $15,15,17$. The distinction between the two thresholds matters: a $2\times3\times3$ frame has sixteen positions and needs seventeen available sources, whereas its complete box uses any eighteen sources without spares. Table~\ref{tab:small-boxes} lists the smallest shapes. For $s\ge9$, $F_5=L$ and $G_5=abc$. \begin{table}[ht] \centering \small \begin{tabular}{c c c c c c} \toprule Box & $s$ & Frame positions & $F_5$ & Volume & $G_5$\\ \midrule $2\times2\times2$ & 6 & 8 & \textbf{15} & 8 & \textbf{15}\\ $2\times2\times3$ & 7 & 12 & \textbf{15} & 12 & \textbf{15}\\ $2\times2\times4$ & 8 & 16 & \textbf{17} & 16 & \textbf{17}\\ $2\times3\times3$ & 8 & 16 & \textbf{17} & 18 & 18\\ $2\times2\times5$ & 9 & 20 & 20 & 20 & 20\\ $2\times3\times4$ & 9 & 20 & 20 & 24 & 24\\ $3\times3\times3$ & 9 & 20 & 20 & 27 & 27\\ \bottomrule \end{tabular} \caption{Thresholds for the smallest boxes. A bold entry exceeds the number of positions: some collections with no spare sources fail.} \label{tab:small-boxes} \end{table} For ordinary cubes, abbreviate $F_5(n)=F_5(n,n,n)$ and $G_5(n)=G_5(n,n,n)$. The classification immediately gives the following. \begin{corollary}[Ordinary cubes]\label{thm:frames}\label{thm:complete} \[ F_5(n)=\begin{cases}15,&n=2,\\12n-16,&n\ge3,\end{cases} \qquad G_5(n)=\max\{n^3,15\}\quad(n\ge2). \] In particular, any twenty sources form the frame of a $3\times3\times3$ cube, and any 27 form a complete $3\times3\times3$ cube. \end{corollary} Berkove, Eickemeyer and Schulman~\cite[Section 8, Table 7]{BES} record frame thresholds for palettes of two to six colours, leaving the five-colour column open. Table~\ref{tab:palette-thresholds} inserts the values proved here; the cuboid classification goes beyond that table. \begin{table}[ht] \centering \small \begin{tabular}{c c c c c c} \toprule Side length & 2 colours & 3 colours & 4 colours & \textbf{5 colours} & 6 colours\\ \midrule $n=2$ & 11 & 23 & 11 & \textbf{15} & 24\\ $n=3$ & 20 & 35 & 20 & \textbf{20} & 24\\ $n\ge4$ & $12n-16$ & $16n-17$ & $12n-16$ & $\boldsymbol{12n-16}$ & $12n-16$\\ \bottomrule \end{tabular} \caption{Cube-frame thresholds. The five-colour column is proved here; other columns are as recorded in~\cite[Table 7]{BES}.} \label{tab:palette-thresholds} \end{table} We first prove the corner threshold independently of the extensions. Write $N_5=F_5(2)=G_5(2)$. \begin{theorem}[Corner threshold]\label{thm:main} $N_5=15$. \end{theorem} An elementary fourteen-cube obstruction proves the lower bound. For the upper bound, Hall deficiencies and symmetry reduce hypothetical counterexamples to finite problems, excluded by interval certificates (Sections~\ref{sec:cases}--\ref{sec:certificates}). For cuboids, Lemma~\ref{lem:eight-common-missing} builds corners from eight sources lacking a common pair and any three others. This lets the proof choose targets avoiding scarce edge requirements; compatibility bounds then complete the Hall argument (Sections~\ref{sec:frames}--\ref{sec:boxes}). These cuboid deductions need no further interval certificates. Sections~\ref{sec:construction}--\ref{sec:universal} give the construction algorithm, support thresholds, extremal obstructions and minimum universal corner collections. The complete extremal classification in Section~\ref{sec:classification14} has its own certificate computation and yields a short deletion proof of the corner threshold. The universal minimum has an independent elementary proof. Section~\ref{sec:formal} describes the verification scope. The side-length restriction is substantive. With a side of length one, a source can meet two opposite exterior faces and expose four or more faces at once. The corner-and-edge model and the completion by arbitrary unused cubes then need replacement. The accompanying repository contains the certificates, programs, geometric audits and Lean sources.\footnote{The proof artifact is pinned to \href{https://github.com/jasondavies/five-colour-cubes/tree/c4bd4efc20472049b7492589d8c86b573b32e0a0}{Git commit \texttt{c4bd4efc2047}}. Appendix~\ref{app:reproduction} gives the full identifier, certificate checksum and reproduction commands.} The companion paper~\cite{FourToThree} considers four-colour sources and targets using exactly three colours. It gives the sharp frame threshold $16n-3$ for every side length $n\ge2$, with a classification of the largest failing collections. The two developments share the palette-independent geometry in the \texttt{colour-\allowbreak cubes-\allowbreak core} library~\cite{ColourCubes}; neither threshold theorem is used to prove the other. \section{Geometry and Hall deficiencies}\label{sec:model} Represent a cube by its colours on the faces $(+x,-x,+y,-y,+z,-z)$ in a right-handed coordinate frame. A five-colour cube has one repeated colour. There are 75 varieties: for each repeated colour, three have its two faces opposite and twelve have them adjacent. In the opposite case, the other four colours form two opposite pairs, giving three possibilities. In the adjacent case, fix the two equal faces; the 24 orders of the other colours are identified in pairs by the rotation exchanging those equal faces. Thus there are 15 opposite-repeat varieties and 60 adjacent-repeat varieties. Each class is one orbit under colour permutations. A corner type is the ordered triple of its incident face colours, modulo cyclic permutation. Order the outward face normals positively, equivalently read the triple counterclockwise from outside along the body diagonal. This reverses the clockwise convention in~\cite{BES}, consistently on every cube, and therefore preserves all matching and containment relations. Repeated occurrences of a corner type are retained as distinct target positions. \begin{lemma}[Corner--rotation correspondence]\label{lem:corner} A source cube fits a target corner by a proper rotation if and only if it has the same cyclic corner type at some corner. \end{lemma} \begin{proof} A proper rotation preserves the orientation of a corner frame, so it induces a cyclic permutation of its three outward faces. Conversely, any two positively oriented corner frames, with a prescribed cyclic alignment, are related by a determinant-positive signed permutation of the coordinate axes. This is a proper rotation of the cube. \end{proof} The palette-independent Lean version of this lemma is reused from the shared \texttt{colour-\allowbreak cubes-\allowbreak core} library~\cite{ColourCubes}. Fix a target $T$. Form a bipartite graph whose left vertices are its eight corner positions and whose right vertices are the individual source copies. A copy is adjacent to a position when it fits there. A matching covering the eight positions is exactly a solution: each chosen copy can be rotated independently, since interior faces are unrestricted. By Hall's theorem~\cite{Hall}, failure is equivalent to a nonempty set $D$ of target positions having fewer than $|D|$ neighbouring copies. Index the varieties by $i=1,\ldots,75$, and let $x_i$ be their multiplicities. For a set $S$ of varieties, write $x(S)=\sum_{i\in S}x_i$. Let $N_T(D)$ be the varieties fitting at least one position of $D$. The 255 nonempty choices of $D$ give 19,125 cuts across the 75 targets. Failure of $T$ is equivalent to the existence of a cut \begin{equation}\label{eq:hall} x(N_T(D))\le |D|-1,\qquad \varnothing\ne D\subseteq\{1,\ldots,8\}. \end{equation} \section{An elementary fourteen-cube obstruction}\label{sec:lower} Consider four copies of $A$, five of $B$, and five of $C$, where \[ A=(0,0,1,2,3,4),\quad B=(0,1,2,3,2,4),\quad C=(0,3,1,2,4,1). \] Their corner types are shown below. Triples denote cyclic classes; the last column counts positions whose type occurs in neither of the other varieties. \begin{center} \begin{tabular}{clc} \toprule Variety & Corner types & Private positions\\ \midrule $A$ & $013,014,023,024,031,032,041,042$ & 5\\ $B$ & $022,023,034,042,122,124,132,143$ & 6\\ $C$ & $011,014,021,042,113,123,134,243$ & 6\\ \bottomrule \end{tabular} \end{center} \begin{lemma}\label{lem:lower} The collection $4A+5B+5C$ has no five-colour solution. \end{lemma} \begin{proof} A solvable target must have every corner type in the displayed union. Its only two-colour types are $022,122,011,113$. An adjacent-repeat target therefore repeats either colour 2, with types $022,122$, or colour 1, with types $011,113$. In either case these two corners determine the colours on the faces at the ends of the repeated-colour edge. The two orders of the remaining colours give a mirror pair: $B$ and its mirror, or $C$ and its mirror. The mirror of $B$ requires $043$, and the mirror of $C$ requires $012$; both types are absent. Only $B,C$ remain. An opposite-repeat target requires both cyclic orientations of each corner triple. The unordered triples with both orientations in the union are \[ 013,014,023,024,123,134. \] If its repeated colour is $r$, delete $r$ from the four triples containing it. The remaining pairs must form a $K_{2,2}$ on the other four colours: choose one face from each of their two opposite pairs. Colours 2 and 4 occur in fewer than four listed triples. For $r=1$ or $r=3$, the four pairs have degree sequence $(3,2,2,1)$, so do not form $K_{2,2}$. For $r=0$, the pairs are $13,14,23,24$, forcing opposite pairs $\{1,2\}$ and $\{3,4\}$. This is $A$. Thus only $A,B,C$ can be targets. Their private positions require respectively at least five, six and six copies of the corresponding variety, exceeding the available four, five and five copies (Figure~\ref{fig:obstruction}). None is solvable. \end{proof} \begin{figure}[ht] \centering \input{obstruction-figure} \caption{The fourteen-cube obstruction $4A+5B+5C$. Each net has $+x$ at its centre. Corner types are read counterclockwise from outside; the highlighted corner types occur on neither of the other two displayed varieties. A target of variety $X$ has these private positions, and only copies of $X$ fit them.} \label{fig:obstruction} \end{figure} \section{Reduction to finite problems}\label{sec:cases} Eight copies of any variety solve that variety, so a solution-free collection has every multiplicity at most seven. Suppose such a collection has size 15. \begin{lemma}[Anchored Hall cover]\label{lem:anchor} Suppose a collection contains $m$ copies of a variety $A$ and does not solve $A$. There is a set $K$ of its target positions such that \begin{equation}\label{eq:anchor} |K|\le 7-m,\qquad \#\{\text{other copies fitting some position outside }K\} \le 7-m-|K|. \end{equation} Conversely, such a set certifies failure of target $A$. \end{lemma} \begin{proof} Apply~\eqref{eq:hall} to $A$ and put $K=D^c$. Every copy of $A$ is a neighbour of the nonempty set $D$. Subtract these $m$ copies from the bound $|D|-1=7-|K|$. The converse is the same Hall inequality read backwards. \end{proof} First suppose the maximum multiplicity $m$ is at least two. Choose an adjacent-repeat anchor attaining $m$ if possible; otherwise choose an opposite-repeat anchor attaining $m$. In the latter case all adjacent-repeat multiplicities are at most $m-1$. Relabel the colours to send the anchor to a fixed representative of its orbit. For each cover $K$ in Lemma~\ref{lem:anchor}, put \[ S(K)=N_A(K^c)\setminus\{A\},\qquad b(K)=7-m-|K|. \] Write $S=S(K)$ and $b=b(K)$. The case has $x_A=m$, $x(S)\le b$, and the multiplicity bounds just described. Additional upper bounds use two-variety solutions, for each variety $V\ne A$. If $j$ copies of $A$ and $8-j$ copies of $V$ build a target, with $j\le m$, then $x_V\le 7-j$ in a solution-free collection. These tests are finite: the two varieties must cover all eight target positions, $A$ must fit at least $j$, and $V$ at least $8-j$. They are also sufficient: at most $j$ positions are unavailable to $V$, and all of them are available to $A$. Assign these to $A$, extend the assignment to $j$ positions that $A$ fits, and assign the remaining $8-j$ positions to $V$. Colour permutations and simultaneous reflection of the entire collection preserve solvability. This action has $2\cdot5!=240$ elements; its anchor stabilisers have orders $240/15=16$ and $240/60=4$ for opposite-repeat and adjacent-repeat varieties, respectively. First identify equal pairs $(S(K),b(K))$, even when they arise from inequivalent position subsets $K$; then retain one representative per orbit of these pairs under the anchor stabiliser. The counts below refer to these constraint pairs. Transporting a cover also transports its constrained varieties, budget and multiplicities, so no counterexample is lost. Global reflection transports the whole collection; individual cubes still move only by proper rotations. The repeated-variety cases give 244 constraint orbits; the breakdown is in Appendix~\ref{app:verification}. For distinct collections a different choice of anchor reduces the count. \begin{lemma}[Shared two-colour corner]\label{lem:shared} Among eleven adjacent-repeat cubes, two share a two-colour corner type. If a distinct collection contains such a pair and one member is chosen as anchor, the set consisting of its two two-colour positions is not Hall-deficient. \end{lemma} \begin{proof} Each adjacent-repeat cube with repeated colour $r$ has exactly two such types, $rrx$ and $rry$, with $x\ne y$. There are only $5\cdot4=20$ types $rrx$. Eleven cubes contribute 22 incidences, so two cubes share a type. For the two characteristic positions of the chosen anchor, the anchor itself and the other cube are two distinct neighbours. Their neighbourhood therefore has size at least two. \end{proof} If an opposite-repeat variety is present, choose it as anchor; this gives 31 constraint orbits with every multiplicity at most one. Otherwise use Lemma~\ref{lem:shared} to choose an adjacent-repeat anchor. Omit the cover complementary to its two characteristic positions and set all opposite-repeat capacities to zero. Its stabiliser preserves these positions, so the omission is compatible with the orbit reduction. It removes one of the 83 adjacent-repeat constraint orbits, leaving 82 further cases. A \emph{root case} is an integer feasibility problem specified by an anchor multiplicity, coordinate bounds and an anchored Hall budget. \begin{proposition}\label{prop:cover} Every solution-free fifteen-cube collection is carried by colour relabelling and, if needed, global reflection into one of the 357 exported root cases. \end{proposition} \begin{proof} The preceding arguments cover repeated and distinct collections. The finite catalogue, two-variety bounds and coverage of all anchor-cover orbits are checked from physical rotations by the accompanying audit. It regenerates rotations from quarter turns, separately from the signed-axis permutations used by the case generator, and checks every exported bound and every cover orbit. The resulting counts are \[ 244+31+82=357. \] The cases need not be disjoint; completeness of the cover is what is required. \end{proof} Each root specifies an anchor $A$ of multiplicity $m$, coordinate bounds $\ell,u$, a set $S$ of non-anchor varieties and a budget $b$. The bounds fix $\ell_A=u_A=m$, with $\ell_i=0$ for $i\ne A$. A vector $x\in\mathbb Z_{\ge0}^{75}$ is \emph{admissible} for this root if \begin{equation}\label{eq:admissible} \begin{gathered} \ell\le x\le u,\qquad \sum_{i=1}^{75}x_i=15,\qquad x(S)\le b,\\ \text{for every target }T\text{, there is }\varnothing\ne D\subseteq\{1,\ldots,8\} \text{ with }x(N_T(D))\le |D|-1. \end{gathered} \end{equation} Thus admissibility includes failure of every target, in addition to the anchor constraints. The cuts are alternatives within each target, but at least one cut must hold for every target. The cover can be reduced without further search. If $S'\subseteq S$ and $b'\ge b$, then $x(S)\le b$ implies $x(S')\le b'$ for nonnegative $x$. Together with coordinatewise inclusion of the root boxes, this identifies 49 cases contained in other cases, leaving 308. Write $u$ for the root upper bounds. In 29 retained cases, $b+u(S^c)<15$ already contradicts the prescribed total, so only 279 cases need further exclusion proofs. The exact map and retained case numbers are in \path{data/q5-root-reduction.json}; Lean checks all containments and arithmetic exclusions. All 357 original root definitions remain available. \begin{lemma}[Hall-budget projection]\label{lem:projection} Suppose a root has anchor multiplicity $m$, budget $x(S)\le b$, and total $N$, with the anchor outside $S$. For an integer $\lambda$ with $0\le \lambda\le b$, put $G=N-b+\lambda$ and suppose $G\ge m$. Every admissible vector $x$ has a vector $y\le x$ with the same anchor multiplicity, total $G$, budget $y(S)\le \lambda$, and a Hall deficiency for every target. It obeys the original upper bounds, tightened to $\min(u_i,\lambda)$ on $S$. \end{lemma} \begin{proof} First retain only $\min(x(S),\lambda)$ copies in $S$. This removes at most $b-\lambda$ copies and leaves the anchor untouched, so the remaining total is at least $G$. Delete further non-anchor copies until the total is $G$; this is possible because $G\ge m$. Every coordinate decreases, so all upper bounds and Hall deficiency inequalities are preserved. Nonnegativity and $y(S)\le \lambda$ give $y_i\le \lambda$ for $i\in S$. \end{proof} For our anchored covers, $b=7-m-|K|$, so \[ G=m+(N-7)+|K|+\lambda. \] At $N=15$, the reduced collection consists of the $m$ fixed anchor copies and $8+|K|+\lambda$ other copies; in particular, $G\ge m$ is automatic. Apply the lemma after selecting and normalising the original root, retaining its bounds. No new anchor selection is required for the smaller collection. The resulting 279 projected problems have totals between 9 and 15. Their parameters and exceptional cases are recorded in Appendix~\ref{app:verification}. \section{Interval certificates}\label{sec:certificates} For a projected problem, admissibility is defined by~\eqref{eq:admissible} with tightened upper bounds and total $G$. In this section denote its projected budget by $b$. We certify that no admissible vector exists. Write a box as $\ell\le x\le u$. For a cut $x(S)\le r$, two necessary conditions for feasibility in the box are \begin{equation}\label{eq:possible} \ell(S)\le r,\qquad G\le r+u(S^c). \end{equation} The first follows from the lower bounds; the second follows from $G=x(S)+x(S^c)$. When they hold, put $\sigma=r-\ell(S)$ and $\gamma=r+u(S^c)-G$. Every satisfying vector obeys \begin{equation}\label{eq:refine} x_i\le\min(u_i,\ell_i+\sigma)\quad(i\in S),\qquad x_i\ge\max(\ell_i,u_i-\gamma)\quad(i\notin S). \end{equation} For example, the upper bound follows by giving all other coordinates of $S$ their lower bounds; the lower bound follows by giving all other coordinates of $S^c$ their upper bounds. For a target, retain its cuts satisfying~\eqref{eq:possible}. If none remain, no vector in the box can fail that target. Otherwise let $I$ and $U$ be the intersection and union of their neighbourhoods, and let $\sigma_*,\gamma_*$ be the largest corresponding $\sigma,\gamma$. Then all vectors in the box that fail this target remain in the refined box \begin{equation}\label{eq:summary} u'_i=\begin{cases}\min(u_i,\ell_i+\sigma_*)&i\in I,\\u_i&i\notin I,\end{cases} \qquad \ell'_i=\begin{cases}\max(\ell_i,u_i-\gamma_*)&i\notin U,\\\ell_i&i\in U.\end{cases} \end{equation} Indeed, a failing vector satisfies one of the retained cuts, and its bounds in~\eqref{eq:refine} imply~\eqref{eq:summary}. For a concrete example, use the archive's zero-based numbering for both certificates and varieties. Projected certificate 28 starts with two copies of adjacent variety 3, total $G=14$ and budget zero. All other lower bounds are zero, and the upper bounds sum to 40. At this root, consider a refinement using target 4. Of that target's 255 cuts, 17 satisfy~\eqref{eq:possible}; their neighbourhood intersection is $\{4,10,30\}$ and their maximum slack is $\sigma_*=1$. The three corresponding upper bounds therefore decrease from 2 to 1. Here varieties 3 and 4 have face tuples $(0,1,0,2,3,4)$ and $(0,1,0,2,4,3)$; all indices refer to \texttt{data/five-colour-geometry.txt}. The root budget is treated as a family containing a single cut. The total $\sum_i x_i=G$ gives \[ \ell'_i=\max\!\left(\ell_i,G-\sum_{j\ne i}u_j\right),\qquad u'_i=\min\!\left(u_i,G-\sum_{j\ne i}\ell_j\right). \] A total-bound leaf closes exactly when $\sum_i\ell_i>G$ or $\sum_i u_ib$ or $b+u(S^c)d$, every source neighbours $D$, since none can miss all its positions. In each case Hall's inequality holds. \end{proof} \emph{Universal-copy consequence.} In a pool of $N\ge L$ sources, if each source misses at most $d$ of the $L$ positions and at least $d$ source copies each fit all $L$ target positions, a complete matching exists. This is the case $P_0=\varnothing$ of Lemma~\ref{lem:partial-matching}. \begin{lemma}[Missing pairs and shared corners]\label{lem:cube-incidence} Every five-colour variety has eight distinct cyclic corner types. An adjacent-repeat variety lacks exactly one bichromatic edge type; an opposite-repeat variety lacks exactly two, which are disjoint. Two disjoint missing pairs determine a unique opposite-repeat variety. If either of two varieties is opposite-repeat, they share at least two corner types. A target has at most one monochromatic edge; each bichromatic type occurs on at most two edges, and a doubled type contains the repeated colour. Thus two disjoint bichromatic types account for at most three geometric target edges. \end{lemma} \begin{proof} A missing bichromatic pair occupies opposite singleton faces: if a colour is repeated, a face of the other colour cannot be opposite both copies. An adjacent-repeat variety has one opposite pair of singleton faces, and an opposite-repeat variety has two. Two disjoint missing pairs specify two opposite face pairs, leaving the fifth colour on the remaining pair, which determines a unique variety. For the shared-corner assertion, let the opposite-repeat variety repeat $r$, with singleton opposite pairs $\{\alpha,\beta\}$ and $\{\gamma,\delta\}$. It contains both cyclic orientations of each $rxy$ with $x\in\{\alpha,\beta\}$ and $y\in\{\gamma,\delta\}$. In the other variety, an $r$-face with no adjacent $r$-face has at least three distinct colours around it. Their cyclic order crosses between the two pairs at least twice, giving two shared corners. If its $r$-faces are adjacent, the other neighbours of each form a path of three distinct colours. Each path crosses between the pairs and gives a shared corner, and these have different types. Corner counts are symmetric: a five-colour variety has eight distinct cyclic corner types, since the only repeated colour multisets occur at the two ends of an edge, in opposite cyclic orders. Only the repeated colour can form a monochromatic edge. Two singleton faces meet along at most one edge; hence a doubled bichromatic type contains the repeated colour and occurs at most twice. Two disjoint types cannot both contain that colour, proving the final bound. \end{proof} \begin{lemma}[A transverse edge forces a common corner]\label{lem:transverse-corner} Let source and target both be adjacent-repeat varieties. If the source lacks the type of a target edge not parallel to the target's monochromatic edge, then it shares a corner type with the target. \end{lemma} \begin{proof} Relabel the colours and rotate the target to $T=(0,1,0,2,3,4)$. Its monochromatic edge is parallel to $z$. The types occurring on edges transverse to the monochromatic edge are $03,04,13,14,23,24$. The proper half-turn interchanging the $x$- and $y$-directions and reversing $z$, followed by the colour relabelling $1\leftrightarrow2$, $3\leftrightarrow4$, fixes $T$ and pairs these types as $(03,04)$, $(13,24)$, and $(14,23)$. Thus three cases suffice. For each missing type the source has its two colours on opposite faces. The other three colours occur around that axis in one of two cyclic orientations. The three adjacent-repeat choices in each orientation share six tricoloured corners. Reading those common corners gives: \[ \begin{array}{c|c|c} \text{Missing type}&\text{Shared corners in one orientation} &\text{Shared corners in the other orientation}\\\hline 03&024,041&123\\ 13&032&041,142\\ 14&013,123&024 \end{array} \] Every entry is nonempty, so the source and target share a corner. \end{proof} For a bichromatic pair $\alpha\beta$, let $\mathcal H_{\alpha\beta}$ be the family of varieties lacking that edge type. In every such cube, $\alpha$ and $\beta$ are opposite singleton faces. The four faces around this axis use the other three colours, one of them twice. There are nine varieties in $\mathcal H_{\alpha\beta}$: three opposite-repeat varieties $O_r$, and six adjacent-repeat varieties $A_r^+$ and $A_r^-$, where $r$ is the repeated colour. The signs distinguish the two cyclic orientations of the three distinct ring colours. All three $A_r^+$ varieties share the same six tricoloured corner types; all three $A_r^-$ varieties share the reverse six types. \begin{lemma}[The missing-pair corner array]\label{lem:fixed-missing-pair} The eight corners of an opposite-repeat target $O_r\in\mathcal H_{\alpha\beta}$ form a $2\times2$ array with two positions per cell. Rows correspond to the two unordered ring-colour pairs involving $r$, and columns to their cyclic orientations. A source $O_r$ fits every cell; the other two opposite-repeat varieties each fit one row; and the positive and negative adjacent-repeat varieties fit the corresponding columns. Consequently, every variety in $\mathcal H_{\alpha\beta}$ shares at least four corner types with every opposite-repeat variety in that family. \end{lemma} \begin{proof} Each cell contains one corner at each end of the $\alpha\beta$ axis. Reading the ring colours gives the stated incidences. Figure~\ref{fig:ring-array} shows the example $O_2=(0,1,2,2,3,4)$ in $\mathcal H_{01}$, with $+$ chosen to include $023$. Relabelling the three ring colours gives the other two targets, and relabelling the palette gives every missing-pair family. Cyclic rotations identify corner labels. In particular, the two positions in each cell have identical neighbourhoods among sources in $\mathcal H_{\alpha\beta}$. \end{proof} \begin{figure}[ht] \centering \begin{tikzpicture}[x=3cm,y=1.1cm] \fill[blue!8] (0,0) rectangle (1,2); \fill[orange!12] (1,0) rectangle (2,2); \draw (0,0) rectangle (2,2); \draw (1,0)--(1,2); \draw (0,1)--(2,1); \node at (.5,1.5) {$023,132$}; \node at (1.5,1.5) {$032,123$}; \node at (.5,.5) {$042,124$}; \node at (1.5,.5) {$024,142$}; \node[align=center] at (.5,2.45) {$A_r^+$ sources\\positive column}; \node[align=center] at (1.5,2.45) {$A_r^-$ sources\\negative column}; \node[anchor=east,align=right] at (-.1,1.5) {pair $23$\\$O_3$ fits this row}; \node[anchor=east,align=right] at (-.1,.5) {pair $24$\\$O_4$ fits this row}; \node at (1,-.45) {$O_2$ fits all four cells}; \end{tikzpicture} \caption{Corner array of $O_2$ in the family lacking $01$. Each cell contains two target positions. Here $r\in\{2,3,4\}$; all three adjacent-repeat sources of a given sign fit the same column.} \label{fig:ring-array} \end{figure} \input{boxes} \input{construction} \input{extremal} \input{universal} \section{Formal verification}\label{sec:formal} The development uses Lean~4 and mathlib~\cite{Lean4,mathlib}, both at \texttt{v4.35.0}, with the physical model and palette-independent geometry of \texttt{colour-cubes-core}~\cite{ColourCubes}. It connects arbitrary physical cubes to the catalogue, Hall deficiencies, the complete root cover and the certified exclusions. The cuboid deductions apply the verified corner theorem. The following table distinguishes the proof scopes; ``comparison'' means the separate Mathlib-only statement interface, accepted by both NanoDa and Lean's standalone kernel. The certificate column includes dependencies: the cuboid deductions use the certified corner theorem, and the symbolic classification uses the certified exhaustion by concrete representatives. \begin{center} \small \begin{tabular}{p{.52\linewidth}ccc} \toprule Result & Lean & \shortstack{Uses interval\\certificates} & Comparison\\ \midrule Corner, cuboid and support thresholds & Yes & Yes & Yes\\ Multiplicity bound, three-variety classification and obstruction family & Yes & No & Yes\\ Fourteen-cube classification: 56 concrete classes & Yes & Yes & Yes\\ Symbolic $51+4+1$ forms and labelled counts & No & Yes & No\\ Universal minimum and cyclic construction & Yes & No & Yes\\ Minimum-universal tree structure (Corollary~\ref{cor:universal-structure}) & Yes & No & No\\ Construction complexity and Domino observation & No & No & No\\ \bottomrule \end{tabular} \end{center} In namespace \path{FiveColour.Puzzle}, the unconditional endpoints \path{box_frame_threshold} and \path{complete_box_threshold} are exported by \path{Solution.lean}. They use the physical box definitions and proper-rotation bridges. The sixteen-claim comparison interface describes physical copies, proper rotations and exposed faces without catalogue indices. The symbolic forms and labelled counts are proved here and checked by the separate normal-form audit. The deletion deduction is a manuscript argument; the exported threshold retains its separate certificate proof. Appendix~\ref{app:verification} gives the soundness and audit details. Appendix~\ref{app:reproduction} pins the proof artifact and gives separate commands for full verification and external comparison, together with the scope of the retained execution records. \section{Remaining questions} Does $N_5=15$ admit a short elementary proof, replacing the finite certificates used here? Boxes with a side of length one also fall outside the model, since a source there exposes opposite faces; their thresholds remain open. The \emph{Domino condition}, requiring touching interior faces to agree \cite[Section~8]{BES}, changes the guarantee fundamentally. For any fixed $a,b,c\ge2$, arbitrarily many copies of one adjacent-repeat variety cannot assemble a Domino frame or box. To see this, write that variety as $D=(r,p,r,q,s,t)$, with the five colours distinct. The corner encoding in Section~\ref{sec:support} determines a variety from its eight distinct corner types. An identical-source pool can therefore reproduce only $D$, up to a common proper rotation: containment of its eight corner types forces equality. Along the edge common to the $p$- and $q$-faces, every source must align its unique $p$ and $q$ faces with the same two perpendicular directions. This fixes its proper orientation. Consecutive copies then meet with colour $s$ against colour $t$, which differ. The edge contains at least two cubes and is present in both a frame and a complete box. Thus there is no finite threshold for arbitrary multisets under the Domino condition. This observation concerns a different model and is not included in the Lean interface; its universal-collection questions are left for separate investigation. \section*{AI disclosure} GPT-6-Astra (OpenAI), used through Codex, developed the arguments, computational search, verification programs, Lean formalisation and manuscript under the author's direction. Claude Opus 5.5 (Anthropic), used through Claude Code, contributed illustrations, the migration to the shared \path{colour-cubes-core} library, and review and editing of the manuscript. The author initiated and directed the research and takes responsibility for the content. The inherited geometry has its own provenance in the pinned dependency. Automated checks and AI review are not independent human peer review. \appendix \input{verification} \begin{thebibliography}{9} \raggedright \bibitem{MacMahon} P.~A.~MacMahon, \emph{New Mathematical Pastimes}, Cambridge University Press (1921). \href{https://archive.org/details/newmathematicalp00macmuoft}{Digitised edition}. \bibitem{BES} E.~Berkove, A.~Eickemeyer and M.~Schulman, \emph{The 4-Color Cubes Puzzle}, Integers \textbf{18} (2018), A68. \href{https://doi.org/10.5281/zenodo.10680216}{doi:\nolinkurl{10.5281/zenodo.10680216}}. \href{https://math.colgate.edu/~integers/s68/s68.pdf}{Journal PDF}. \bibitem{Hall} P.~Hall, \emph{On Representatives of Subsets}, Journal of the London Mathematical Society \textbf{s1-10}(1) (1935), 26--30. \href{https://doi.org/10.1112/jlms/s1-10.37.26}{doi:\nolinkurl{10.1112/jlms/s1-10.37.26}}. \bibitem{EdmondsKarp} J.~Edmonds and R.~M.~Karp, \emph{Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems}, Journal of the ACM \textbf{19}(2) (1972), 248--264. \href{https://doi.org/10.1145/321694.321699}{doi:\nolinkurl{10.1145/321694.321699}}. \bibitem{FourToThree} J.~Davies, \emph{Three-colour solutions from four-colour cubes}, \href{https://hexagonmath.org/2611.00070v1}{hexagon:\nolinkurl{2611.00070v1}} (2026). \href{https://github.com/jasondavies/four-to-three-colour-cubes}{Accompanying repository}. \bibitem{ColourCubes} J.~Davies, \texttt{colour-\allowbreak cubes-\allowbreak 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}. \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 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}. \end{thebibliography} \end{document}