The 28 convex uniform honeycombs: a completeness theorem

We prove that every vertex-transitive face-to-face honeycomb of Euclidean 3-space by unit-edge convex uniform polyhedra (Platonic, Archimedean, prisms and antiprisms) is one of the 28 convex uniform honeycombs. The list dates to Andreini (1905, with errors) and was settled at 28 by Johnson and Grünbaum (1994), but no completeness proof has appeared. The proof closes four finite gates: an Alphabet Theorem — only 13 cells can occur in any face-to-face unit-edge honeycomb, vertex-transitive or not, by a two-tier angle arithmetic in 15°ℤ + arctan(√2)ℤ and interval-certified corona fixpoints whose few exact coincidences are refuted over ℚ(√5) and by an interleaving argument; a species table — exactly 34 vertex stars, enumerated as edge-to-edge sphere tilings by rigid cell corners, with the Barlow dichotomy as a corollary; a transitive pattern enumeration over the 26 surviving species — exactly 28 congruence classes, with a forcing theorem and a counterexample showing local consistency does not imply developability; and a periodization audit upgrading each finite development to a certified periodic honeycomb and closing every enumeration cap. All certificates are finite and machine-verified, and every positive certificate on the critical path of the main theorem is exact over ℚ(√2,√3), and the completeness direction is carried independently by an exact Delaney–Dress census, so that no tolerance test on doubles sits on the critical path of either direction.Keywords: convex uniform honeycomb; uniform partition of 3-space; vertex-transitive tiling; Barlow packing; Delaney–Dress symbol; computer-assisted proof. MSC 2020: 52C22 (primary); 52B10, 05B45, 68V05.