cubeEdges_eq
The equality fixes the edge count of the unit cube at twelve. Researchers counting hinges or verifying zero-deficit angles in the Freudenthal decomposition of [0,1]^3 into six tetrahedra would cite this fact when enumerating the twelve face diagonals plus body diagonal. The proof is a direct reflexivity step on the explicit definition of the edge count.
claimThe number of edges of the unit cube $[0,1]^3$ equals 12.
background
The module records the combinatorial skeleton of the Freudenthal triangulation of the unit cube into six tetrahedra sharing the body diagonal. Upstream definitions in Foundation.FreudenthalTriangulationCert, Physics.ParticlePhysicsGenerationsFromRS, and RecogSpec.RSBridge each set cubeEdges to the constant 12, supplying the base integer for subsequent edge-dual counts and hinge tallies. The local setting is the zero-deficit verification for the thirteen new hinges (twelve face diagonals plus one body diagonal).
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition cubeEdges := 12.
why it matters in Recognition Science
This equality supplies the edge count required by the combinatorial certificate that all new hinges carry zero deficit angle. It anchors the enumeration of the twelve face diagonals and the body diagonal in the module's zero-deficit claim. The result supports the broader statement that the Freudenthal decomposition introduces no curvature defects.
scope and limits
- Does not prove the geometric decomposition into tetrahedra.
- Does not compute any deficit angles.
- Does not address higher-dimensional or non-cubic lattices.
formal statement (Lean)
31theorem cubeEdges_eq : cubeEdges = 12 := rfl