cubeVertices
plain-language theorem explainer
The declaration fixes the vertex count of the unit cube at the integer 8. Workers on Freudenthal decompositions of the cube into tetrahedra cite this count when assembling the combinatorial certificate. The definition is a direct constant assignment with no lemmas or computation.
Claim. The unit cube possesses eight vertices.
background
The module records the combinatorial skeleton of the unit cube [0,1]^3 under the Freudenthal triangulation into six tetrahedra. The documentation states that this decomposition produces thirteen new hinges (twelve face diagonals plus one body diagonal) whose deficit angles are zero. The vertex count supplied here is one of the three basic cube data items required by the certificate structure.
proof idea
Direct definition that assigns the constant 8 to the natural-number identifier for cube vertices.
why it matters
The value feeds the cube_data field of FreudenthalCert, which in turn certifies the zero-deficit property for the full set of new hinges. It supplies the first conjunct in the conjunction cubeVertices = 8 ∧ cubeEdges = 12 ∧ cubeFaces = 6 that anchors the triangulation count. Within the Recognition framework this datum supports the claim that six tetrahedra meet along the body diagonal with dihedral angles summing to 2π.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.