newHinges_decomp
plain-language theorem explainer
The declaration decomposes the total count of new hinges in the Freudenthal triangulation of the unit cube into twelve face diagonals plus one body diagonal. Combinatorial geometers or researchers formalizing deficit angles in simplicial refinements would cite this equality when tracking hinge contributions. The proof is a direct reflexivity step once the definition newHinges := 13 is in place.
Claim. The number of new hinges introduced by the Freudenthal triangulation of the unit cube equals twelve face diagonals plus one body diagonal, i.e., $13 = 12 + 1$.
background
The module establishes the combinatorial skeleton of the Freudenthal triangulation of the unit cube [0,1]³, which decomposes into six congruent tetrahedra. Key facts listed are eight vertices, twelve edges, six faces, and the observation that the six tetrahedra share the body diagonal while four tetrahedra meet along each face diagonal. The upstream definition newHinges : ℕ := 13 records the total of these added hinges (twelve face diagonals plus one body diagonal). The imported refinement theorem from DraftV1 supplies surjectivity of quotient maps but is not invoked in the present equality.
proof idea
The proof is a one-line term-mode wrapper that applies reflexivity (rfl) directly to the definition newHinges := 13, which is definitionally equal to 12 + 1.
why it matters
The equality supplies the explicit decomposition required by the module's claim that all thirteen new hinges carry zero deficit angle (twelve face diagonals each tiled by four tetrahedra summing to 2π, and the body diagonal tiled by six tetrahedra each at dihedral angle π/3). It therefore closes the combinatorial step in the Beltracchi response §4 before any geometric or curvature arguments are introduced. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.