totalHinges_eq
plain-language theorem explainer
The equality fixes the total hinge count in the simplicial refinement of the unit cube at exactly 25. Workers on the Freudenthal triangulation certificate cite it to lock the combinatorial size before checking zero deficits on the added hinges. The proof is a one-line decision procedure that unfolds the definition totalHingesSimp := cubeEdges + newHinges and evaluates the sum directly.
Claim. In the Freudenthal triangulation of the unit cube, the total number of hinges after simplicial refinement equals 25.
background
The module records the combinatorial facts for the Freudenthal triangulation certificate: the unit cube decomposes into six congruent tetrahedra sharing the body diagonal, with twelve original edges and thirteen new hinges (twelve face diagonals plus one body diagonal). The definition totalHingesSimp counts these as cubeEdges + newHinges. Upstream deficit at a hinge is 2π minus the sum of the dihedral angles meeting there; the certificate asserts that all new hinges are flat and therefore carry zero deficit.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to evaluate the arithmetic equality after unfolding the definition of totalHingesSimp.
why it matters
This equality fixes the hinge count at 25 for the Freudenthal certificate, which then shows that the thirteen new hinges each carry zero deficit angle. It supports the claim that the triangulation introduces no curvature at the added hinges, consistent with the flat-space embedding of the cube. The result closes the combinatorial step in the response to outstanding issues on the triangulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.