We determine two finite models motivated by open problems in discrete geometry. Let $T_4=\{-1,0,1\}^4$. We prove that the maximum Borsuk number of a subset of $T_4$ is exactly 4: every nondegenerate subset can be partitioned into four sets of strictly smaller diameter, and a four-point equidistant set shows sharpness. Let $U_5=\{v/\lVert v\rVert:v\in\{-1,0,1\}^5\setminus\{0\}\}$. We also prove that a spherical code in $U_5$ with pairwise inner products at most $1/2$ has at most 40 points, with equality only for the $D_5$ root system inside this fixed library. The first result is certified by exact distance-layer colorings and an exhaustive symmetry-reduced enumeration of 15,056 maximal feasible sets; the second by two exact maximum-clique computations using integer predicates. These are finite-library theorems: they do not settle Borsuk's conjecture in $R^4$ or the unrestricted kissing numbers in dimensions 5 and 6.