bodyDiagonalTetrahedra
plain-language theorem explainer
In the Freudenthal triangulation of the unit cube the body diagonal is shared by six tetrahedra. Researchers verifying zero angular deficit in discrete decompositions cite this count when summing dihedral contributions around that edge. The definition supplies the integer directly to support the check that six times one sixth equals one.
Claim. In the Freudenthal triangulation of the unit cube $[0,1]^3$, the body diagonal is shared by exactly six tetrahedra.
background
The module records the combinatorial facts of the Freudenthal decomposition: the unit cube splits into six congruent tetrahedra that all meet along one common body diagonal. Each tetrahedron meets the diagonal at a dihedral angle of one third of $2π$, so the total around the diagonal closes with zero deficit. The local setting is the certificate that all thirteen new hinges (twelve face diagonals plus the body diagonal) carry zero angular deficit.
proof idea
The definition is a direct constant assignment of the natural number six. A single comment records the symbolic angle sum check.
why it matters
This count enters the verification that the body diagonal contributes zero deficit in the Freudenthal certificate. The certificate itself supplies the combinatorial layer for the Recognition Science claim that the cube decomposition introduces no new curvature. It anchors the discrete geometry step that precedes the forcing chain from T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.