\section{Verification and reproduction details}\label{app:verification}
\subsection{Finite certificates}
The repeated-variety cases have the following counts,
totalling 244.
\begin{center}
\begin{tabular}{lrrrrrr}
\toprule
Anchor / maximum multiplicity & 2 & 3 & 4 & 5 & 6 & 7\\
\midrule
Adjacent-repeat & 72 & 55 & 31 & 14 & 4 & 1\\
Opposite-repeat & 26 & 21 & 11 & 6 & 2 & 1\\
Total & 98 & 76 & 42 & 20 & 6 & 2\\
\bottomrule
\end{tabular}
\end{center}

Of the 279 remaining roots, 277 admit an exclusion certificate with $\lambda=0$. The other two, original
cases 68 and 69, use $\lambda=1$ and $G=12$. Their $\lambda=0$, $G=11$ problems actually
have solution-free collections, supplied and checked by physical matching in
the projected manifest. The projected totals range from 9 to 15. The 101 roots
whose original budget was zero retain their original problem statements.

The projected archive contains 298,167 instructions. Every certificate header
is checked against its exported root case. Eighty
negative controls are rejected, including all 77 possible direct closing
claims against a separate $G=11$ fixture, not a $G=15$ root problem.
This fixture is a known solution-free eleven-cube collection: it satisfies
its total, fixed anchor count, coordinate bounds and zero root budget, and
fails all 75 targets by physical matching. It is \path{data/q5-distinct-known-control.txt}; its regeneration and witness
checks are in \path{scripts/check_five_colour_distinct.py}.

\subsection{Lean implementation}
Lean proves completeness and uniqueness of the 75 varieties and checks all
45,000 corner-compatibility bits using the shared corner--rotation theorem.
The lower bound uses 75 deficient corner sets: 72 singletons and three
sets of sizes 5, 6 and 6. Its theorem is
\path{FiveColour.Physical.lower_bound} in \path{FiveColour/LowerBound.lean}. In the formal proof, this replaces the elementary
target classification in Lemma~\ref{lem:lower}; catalogue completeness and
rotation transport extend the result to every physical target.

The upper-bound formalisation follows the Hall reduction, symmetry
transport, anchor selection and shared-corner argument. Finite checks
verify capacities, cover representatives and the reduction from 357 roots
to 279. The deletion step is \path{FiveColour.Physical.root_projection}
in \path{FiveColour/RootProjection.lean}. The shared
\texttt{ProjectionBridge.lean} module identifies the full admissibility
predicate: coordinate bounds, total, budget and all Hall-cut families.

For efficient replay, Lean proves soundness of a packed implementation of
the interval checker. For multiplicities $0\le x_i\le7$, index the varieties
by $0,\ldots,74$ and put
\[
 P(x)=\sum_{i=0}^{74}x_i B^i,\qquad
 W(S)=\sum_{i\in S}B^{74-i},\qquad B=1024.
\]
Then
\[
 x(S)=\left\lfloor\frac{P(x)W(S)}{B^{74}}\right\rfloor\bmod B.
\]
Every coefficient in the product is at most $75\cdot7<1024$, so no carry
can affect this coefficient extraction. Lean proves the identity, decoding,
coordinate updates and equivalence with the integer inequalities, and
checks all 19,125 neighbourhood weights. The evaluator in
\path{FiveColour/PackedFast.lean} computes digit places directly as powers;
Lean proves it equal to the original evaluator on every certificate.
The helpers in \path{FiveColour/PackedComputations.lean} prove that
containment in the packed all-seven digit mask establishes bounded digits
and exact reconstruction. A second helper converts a neighbourhood mask
to its reversed base-1024 weight by consuming successive low bits. These
helpers discharge the original validity and calibration propositions.

For larger certificate cases, the generated checker specialises the cut
families to the initial root. It discards alternatives that fail
\eqref{eq:possible}, removes fixed coordinates (subtracting their mass from
the right-hand side), and merges equal remaining neighbourhoods by keeping
the largest right-hand side. An alternative is also discarded if it implies
a weaker retained alternative. Each original feasible cut has a checked witness
pointing to a weaker replacement. Concretely, a cut $x(C)\le b_C$ may
be replaced by $x(D)\le b_D$ when
\[
 D\subseteq C,\qquad b_C+\ell(D)\le b_D+\ell(C).
\]
Indeed $x(C\setminus D)\ge\ell(C\setminus D)$ for vectors in the root.
Replacement weights are calibrated in the kernel. The theorem \path{FiveColour.Packed.excludes_of_covered} in
\path{FiveColour/PackedPruning.lean} transfers the resulting exclusion back
to the original families at the root; it does not assume that intermediate
split boxes are contained in that root. Small cases retain the original
families to avoid the additional validation cost.

The 279 certificates are split into 2,926 chunks of at most 128
instructions. Composition requires exact boundary-vector agreement and a
proof for every referenced box; the exporter is untrusted. All chunks and
their final assembly have passed kernel checking. The case mapping and
certificate hashes are in \path{data/q5-projected-root-manifest.json}.
The generated module \path{FiveColour/ProjectedChunks/Threshold.lean}
proves the unconditional theorems \path{threshold15} and
\path{sharpThreshold15}. Both lie in namespace
\path{FiveColour.Packed.ProjectedChunks}.

The cuboid proof in Lean follows Lemma~\ref{lem:eight-common-missing}.
The cube exports, such as \path{frame20}, specialise the cuboid theorems.
The equivalences in \path{FiveColour/CubeBoxBridge.lean} identify the cube
and equal-side cuboid position models, preserving exposed faces and physical
placements. Cube completion likewise reuses rectangular completion, whose
generic construction is adapted from~\cite{FourToThree}; no theorem of that
paper is used. The auxiliary eleven-cube missing-pair lemma remains in
\path{FiveColour/RingEleven.lean}, with its multiplicity argument proved
without enumerating collections.

The small-support proofs in \path{FiveColour/SmallSupport.lean} check pair
witnesses directly, without reducing them to five colour orbits.

The full cuboid classification is formalised in
\path{FiveColour/BoxThresholds.lean}. In namespace
\path{FiveColour.Physical}, \path{box_frame_threshold_iff} and
\path{box_threshold_iff} give necessary and sufficient pool sizes for
arbitrary side lengths at least two, assuming
\texttt{Threshold15}. \path{Solution.lean} discharges this assumption and
exports the unconditional \path{FiveColour.Puzzle} theorems
\path{box_frame_threshold} and \path{complete_box_threshold}.

The rectangular model and completion are in
\path{FiveColour/BoxModel.lean}; compatibility is connected to proper
rotations, and axis assignments are realised by proper rotations.
\path{FiveColour/EightPlusThree.lean} proves the physical prescribed-family
lemma. Its proof uses a failed Hall set to obtain the small cover directly,
as in Lemma~\ref{lem:eight-common-missing}; signed projection and small matching
patterns are checked in the kernel. The weighted bounds and upper deductions
are in \path{FiveColour/WideFrames.lean}, \path{FiveColour/RodFrames.lean}
and \path{FiveColour/StripFrames.lean}. The thin-box proofs formalise both
concentration and switching targets, including the equality cases of the
affine geometric bounds. Directional profiles are checked for the two
canonical target varieties; proved colour and rotation transport covers
all targets, including their corner, edge and axis labels. The small
half-mask matching step uses greedy selection after single-mask checks.
\path{FiveColour/BoxLowerBound.lean} proves the
uniform three-variety obstruction for every shape and orientation.
A separate C++ audit reconstructs the geometry and checks these profiles.

\subsection{Extremal obstructions}\label{app:extremal}
The multiplicity bound, three-variety classification and generalized
obstruction family have separate physical Lean proofs, independent of
\path{Threshold15} and the interval replay.

\path{ExtremalMultiplicity.lean} uses the anchor lemma and explicit corner
allocations for small grouped inventories. The allocation theorem reserves
distinct physical copies, and kernel checks validate both the assignments
and the filtered weak-composition lists. Four disjoint sources are handled
first by a separate lemma, leaving 2,702 six-copy inventories and 35
four-disjoint inventories. Their geometry uses 300 shared disjoint-group
masks and 24 optional singleton references; other masks reuse the incidence
data. The main-text proof instead uses the directed-cut intersection
calculation and a uniform reservation argument.

For the three-variety classification, the multiplicity bound forces
$(4,5,5)$. Normalizing the four-copy variety to one of the two anchor types
leaves $2\binom{74}{2}=5,402$ candidates. The coverage/private-position
criterion solves 5,143 at one of their own source targets, and the existing
four-plus-four lemma solves another 199 with a disjoint pair. Kernel checks
prove that the residual list covers both anchor kinds: it has 60 records,
comprising four positive target witnesses and 56 symmetry witnesses. A shared uniform Hall
argument proves that all five representatives fail. Completeness of the
sixteen-element stabilizer of the opposite anchor is checked on physical
faces; this establishes pairwise inequivalence under every allowed global
symmetry. \path{ExtremalClassification.lean} joins these results for arbitrary
physical collections.

\path{ExtremalFamilyTheorems.lean} proves the generalized
family as an equivalence: failure holds exactly when the two blocks have
disjoint repeated-colour supports. Four enlarged support patterns require
only 300 Hall witnesses; two uniform allocations prove the converse. The
21-member family and the five representatives reuse this proof.
The face tuples and orbit sizes are in
\path{data/five-colour-extremal.json}; a separate Python audit checks all
202,575 labelled $(4,5,5)$ collections, recovering 840 failures in five
orbits of sizes $120,120,120,240,240$. It also checks all 441 normalized
family distributions (91 failures and 350 solutions).
These finite formal proofs supplement the elementary main-text arguments;
no interval certificates are added or changed.

\paragraph{Complete classification.}
The separate 349-root proof in Section~\ref{sec:classification14} uses
713,099 interval instructions: 228,264 for 133 strictly projected exclusions,
446,427 for 196 identity projections, 14,012 for thirteen core covers and
extension exclusions, and 24,396 for seven terminal enumerations.
\path{CoreExtension.lean} retains the coordinatewise inequality from budget
projection and composes complete core coverage with exclusions under all
original upper bounds. The 710 smaller cores cannot extend to failures;
they are distinct from the 81 classification terminals.
\path{EnumerationCoverage.lean} assembles all 349 roots.
\path{Classification56.lean} connects coverage, representative failures,
symmetry transport and inequivalence to physical copies;
\path{ClassificationSubmission.lean} transfers the result to the independent
comparison model. The endpoint and its shared bridges are audited in
\path{ClassificationAudit.lean}. A separate physical audit checks the three
normal forms and the union of their 11,430 labelled inventories.

\paragraph{Universal collections.} The universal lower bound counts three sources for each repeated colour.
Small kernel-checked geometry relates the bicoloured types to physical sources;
the upper bound checks 75 explicit matchings and transports them to arbitrary
target orientations. The minimum-collection structure in Corollary~\ref{cor:universal-structure}
is proved in \path{UniversalStructure.lean}: the physical supplier argument
reduces to a kernel-checked lemma about three pairs on four vertices, followed
by the graph-theoretic tree criterion. These proofs do not use the interval
certificates.


\subsection{Reproduction}\label{app:reproduction}
The proof artifact is the repository at Git commit
\begin{center}\small\texttt{c4bd4efc20472049b7492589d8c86b573b32e0a0}.\end{center}
The \href{https://github.com/jasondavies/five-colour-cubes/tree/c4bd4efc20472049b7492589d8c86b573b32e0a0}{pinned source tree}
contains the mathematical sources and certificate inputs used here.
The verification extracts accompanying this manuscript identify the frozen
working-tree snapshot checked before that commit. The threshold archive,
\href{https://github.com/jasondavies/five-colour-cubes/blob/c4bd4efc20472049b7492589d8c86b573b32e0a0/data/q5-projected-certificates.tar.gz}{\texttt{q5-projected-certificates.tar.gz}},
has SHA-256
\begin{center}\small\texttt{7df56cc4b252e460c9e3a762b068010b1a894405ae105218f6cea545e9b80467}.\end{center}
The classification also uses three archives, whose exact hashes are retained
in the verification manifests:
\begin{center}\small
\begin{tabular}{l}
\path{data/five-colour-classification-certificates.tar.gz}\\
\path{data/five-colour-classification-projections.tar.gz}\\
\path{data/five-colour-classification-cores.tar.gz}
\end{tabular}
\end{center} The Lean proof sources and certificate
inputs in this manuscript's repository are byte-identical to those in the
pinned commit.

With the pinned toolchain installed, check out that revision and run:
\begin{verbatim}
git clone https://github.com/jasondavies/five-colour-cubes
cd five-colour-cubes
git checkout c4bd4efc20472049b7492589d8c86b573b32e0a0
lake exe cache get
make check-classification-data WORKERS=2
make classification-replay WORKERS=2
make verify-full WORKERS=2
make comparator
\end{verbatim}
The classification commands check the native data and generated sources,
then build all 349 root proofs and audit the physical endpoint.
\texttt{verify-full} checks the threshold audits, all 279 threshold certificate
proofs, unconditional extensions and their axiom reports; building
\path{Solution.lean} also includes the complete classification.
\texttt{comparator} separately compares all sixteen statements and rechecks
the exported dependency closure with both external kernels. The latter requires
\texttt{bwrap} and the pinned toolchain's \texttt{leanexport},
\texttt{leanchecker} and \texttt{nanoda\_bin} executables.
The pinned README and \path{FiveColour/README.md} give prerequisites and tuning.
The shorter \texttt{make check} omits the complete certificate replay.
For verification without Lean, run \texttt{make check-code WORKERS=2}
and \texttt{make check-classification-data WORKERS=2}. These check the
native certificates, independent audits and generated sources; they do not
replace kernel checking.

A fresh checkout must build the proof after obtaining the dependency cache.
Cached reruns validate Lake dependency traces; the external comparison checks
the complete export afresh. Audit declarations are listed in \path{Audit.lean},
\path{ExtensionsAudit.lean}, \path{ClassificationAudit.lean} and the final
threshold replay audit.
Only \texttt{propext}, \texttt{Classical.choice} and \texttt{Quot.sound} occur;
no \texttt{native\_decide} is used.

The verification record checks every installed dependency's revision and
tracked bytes against its pinned Git tree before and after the run. It also
records source hashes, tool versions, compiler flags and concurrency settings.
Ignored build caches are permitted; modified dependency sources are rejected.

All sixteen statements, shared definitions and permitted axioms passed local
comparison on 9 November 2026, and both NanoDa and Lean's standalone kernel
accepted the complete solution export. The run took 10 hours 32 minutes
48 seconds, using validated Lake artifacts and excluding a fresh project build.
The preceding classification and full-project runs used validated caches;
the external kernels checked the export afresh. These are observed execution
times, not a controlled performance comparison.
No complete cold-build time, aggregate peak memory or disk requirement has
been measured. The retained resource report covers the outer comparison
driver, not all sandboxed subprocesses.
The public provenance extract \path{verification/optimized-comparator.json}
identifies the measured source snapshot by the SHA-256 digest of its manifest of file hashes
and modes, rather than a Git commit:
\begin{center}\small\texttt{940980304874bf067ea978c4a2251381be6cb0fea2cf6ffa0fca7b97303c3f2c}.\end{center}
It also records dependencies, tool identities and settings. Public extracts
omit local paths and process metadata while preserving the original records'
checksums. The same directory retains comparison output, resource measurements
and the preceding successful verification extracts, including
\path{verification/classification.json} and its eight axiom reports.
The source manifest matches the Lean proof sources and certificate inputs
in this manuscript's repository.