cubeVertices_eq
plain-language theorem explainer
The equality asserts that the combinatorial count of vertices in the unit cube is eight. Workers on the Freudenthal triangulation certificate cite this fact when enumerating the elements of the decomposition into six tetrahedra. The proof is immediate from the definition of the vertex count via reflexivity.
Claim. The vertex count of the unit cube satisfies $|V| = 8$.
background
The module formalizes the combinatorial skeleton of the Freudenthal triangulation of the unit cube $[0,1]^3$ into six tetrahedra sharing the body diagonal. The definition cubeVertices supplies the vertex count of this cube as eight. This count is the first of the basic facts listed in the module documentation: eight vertices, twelve edges, and six faces.
proof idea
The proof is a one-line wrapper applying reflexivity to the definition of cubeVertices.
why it matters
This equality supplies the vertex count required by the Freudenthal Triangulation Certificate, which establishes that all thirteen new hinges have zero deficit angle. It anchors the combinatorial facts needed to verify the dihedral angle sums around the body diagonal and face diagonals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.