\section{Verification details}\label{app:verification}
Fifty-eight results and their required definitions are restated in a
standalone verification file (the comparator challenge) importing only
mathlib. They include both cuboid thresholds, the no-spare criteria,
the cube, rod and strip corollaries, position counts and frame completion,
the stability and near-extremal classifications, their counts and the
forty-target theorem. Failures are counted as vectors of rotation-class
multiplicities, and a vector fails when some physical family with those
multiplicities has no frame. The tables of ordinary classes and buckets
are identified with their corner-type definitions in
Lemma~\ref{lem:geometry}. The comparator checks statements and their
underlying definitions against the proof library, then replays proofs
through the Lean, NanoDa and con-ron kernels.

The library's axiom guards permit only \texttt{propext},
\texttt{Classical.choice} and \texttt{Quot.sound}. No proof uses holes or
\texttt{native\_decide}; the challenge contains statement placeholders,
which the proof library does not import. The repository\footnote{\url{https://github.com/jasondavies/four-to-three-colour-cubes}.}
provides sources, reproduction commands and the comparator configuration.
The physical model and palette-independent geometry come from
\texttt{colour-cubes-core}~\cite{ColourCubes}. The challenge restates its
definitions locally; this checks agreement, not independent conception
of the model.

\texttt{BoxDefs} gives one exposed-face position model for every cuboid.
\texttt{BoxModel} proves its cardinalities and completion theorem.
Cubes are equal-sided instances of that model.
\texttt{CuboidResults} proves Theorem~\ref{thm:cuboids} and the no-spare
criteria in Corollary~\ref{cor:cuboid-volume}. The upper proof follows the
weighted-triangle and $Q,H$ constructions in Section~\ref{sec:cuboids}.
A cuboid frame can be restricted and reassembled as an $a\times a\times a$
frame or a $2\times2\times c$ rod. These restrictions transfer the bucket
and balanced-checkerboard lower bounds. The cube, rod and strip thresholds
are specialisations of this general theorem.
The cube stability and obstruction classifications have their own
counting arguments, since they describe failures below the threshold.

Independent rotation-based audits check the local geometry, coordinate
positions, lower witnesses and constructive controls. Sampled inventories
supplement the written and formal proofs; they are not an exhaustive
upper-bound computation.