newHinges
plain-language theorem explainer
The definition newHinges fixes the integer count of additional edges in the Freudenthal triangulation of the unit cube at 13. Researchers formalizing simplicial decompositions or zero-deficit angle sums in three-dimensional polyhedra cite this constant when assembling combinatorial certificates. It is supplied by direct assignment of the value 12 face diagonals plus 1 body diagonal. No lemmas or reductions are required.
Claim. In the Freudenthal triangulation of the unit cube $[0,1]^3$ into six tetrahedra, the number of new hinges is $13$, consisting of the twelve face diagonals together with the single body diagonal.
background
The module records the combinatorial skeleton of the Freudenthal decomposition of the unit cube. The cube itself supplies 8 vertices, 12 edges and 6 faces; the triangulation adds six tetrahedra that all share the body diagonal. New hinges are the edges absent from the original cube skeleton: the face diagonals on each of the six faces plus the internal body diagonal. These counts feed directly into structures that certify angular closure around every new hinge.
proof idea
The declaration is a direct constant definition that assigns the natural number 13. No tactics, lemmas or reductions appear; the value is introduced by immediate assignment.
why it matters
The constant supplies the new_hinges field required by the FreudenthalCert structure and the ZeroDeficitCert that asserts vanishing deficit angles. It therefore closes the combinatorial prerequisite for the three-dimensional case (D = 3) in the Recognition framework, linking the eight-tick octave to explicit hinge counts. The parent results are the decomposition theorem newHinges_decomp and the total-hinge summation totalHingesSimp.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.