cubeVertices
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.
claimThe 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 in Recognition Science
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π.
scope and limits
- Does not prove any geometric embedding or dihedral angles.
- Does not compute tetrahedron or hinge counts.
- Does not address deficit angles or the zero-deficit certificate.
formal statement (Lean)
24def cubeVertices : ℕ := 8
proof body
Definition body.
25/-- Unit cube edge count. -/