The minimum number of vertices of a triangulation of $\mathbb{RP}^5$
Xinrui Chang
math.CO
Oct 18, 2026 · v1
math.AT math.GT
TL;DR
Several intermediate statements of the computer-assisted lower-bound proof have Lean 4 proofs; the full theorem is not formalized end-to-end.
Abstract
We give a computer-assisted proof that every finite simplicial triangulation of real projective five-space has at least twenty-four vertices. Together with the construction of Guyer, Steinerberger, and Yang, this determines the minimum. A cup-product argument produces an induced subcomplex on sixteen or seventeen vertices. Transfer to the spherical double cover then imposes a covering condition on its lifted faces. In the sixteen-vertex case, a direct capacity bound excludes twenty-two vertices. For twenty-three vertices, a cochain extension argument reduces every relevant completion to one of 115 critical signed complexes; integer weights and exact covering certificates exclude all of them. The argument requires no assumption that the triangulation is combinatorial.
Problem
Determine the minimum number of vertices of a simplicial triangulation of real projective five-space. Prior work gave a lower bound of 22 vertices and a construction with 24 vertices.
Approach
A cup-product argument yields an induced subcomplex on 16 or 17 vertices. Transfer to the spherical double cover then imposes a covering condition on lifted faces. The 22-vertex case is excluded by a capacity bound. For 23 vertices, a cochain extension argument reduces every relevant completion to 115 critical signed complexes, each excluded by integer weights and exact covering certificates; several intermediate statements are proved in Lean 4.
Results
Every triangulation of RP^5 has at least 24 vertices, so the minimum is exactly 24. The proof does not assume the triangulation is combinatorial.
