totalHingesSimp
plain-language theorem explainer
The definition totalHingesSimp computes the total hinge count in the Freudenthal simplicial refinement of the unit cube by adding the twelve original edges to the thirteen new hinges. Researchers certifying zero-deficit angles around those hinges in three-dimensional Recognition Science constructions would cite this quantity. It arises as a direct arithmetic sum of two prior constants.
Claim. Let $H$ be the total number of hinges in the simplicial refinement of the unit cube. Then $H := 12 + 13$, where $12$ counts the edges of the unit cube and $13$ counts the new hinges consisting of twelve face diagonals together with one body diagonal.
background
The Freudenthal triangulation decomposes the unit cube $[0,1]^3$ into six congruent tetrahedra that share the body diagonal. The original cube supplies twelve edges. The refinement adds thirteen new hinges (twelve face diagonals plus the body diagonal), each asserted to carry zero deficit angle because the surrounding dihedral angles sum to $2π$ (six tetrahedra at the body diagonal, four at each face diagonal). The module records only the combinatorial counts needed for this certificate.
proof idea
The definition is a one-line wrapper that adds the value of cubeEdges to the value of newHinges.
why it matters
This count is invoked by the downstream theorem totalHinges_eq to obtain the equality 25. It supplies the numerical input required to certify that all new hinges have zero deficit angle, a key combinatorial step in the Freudenthal certificate for the three-dimensional case (D=3) inside the Recognition Science framework. The zero-deficit property guarantees local flatness of the simplicial complex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.