freudenthalTetCount
plain-language theorem explainer
freudenthalTetCount records that the Freudenthal decomposition of the unit cube uses six tetrahedra. Workers on discrete Regge calculus or hinge-angle calculations cite this number when checking deficit closure around the body diagonal. The definition is a direct constant assignment with no further computation.
Claim. The Freudenthal decomposition partitions the unit cube $[0,1]^3$ into exactly six tetrahedra.
background
The Freudenthal Triangulation Certificate module encodes the combinatorial facts needed to certify zero angular deficit in the unit-cube triangulation. The unit cube has eight vertices, twelve edges and six faces. Its Freudenthal decomposition consists of six tetrahedra that all share the body diagonal; each tetrahedron contributes a dihedral angle of one-sixth of a full turn around that diagonal.
proof idea
The declaration is a one-line definition that directly assigns the natural number 6. No tactics or lemmas are invoked; the value is supplied by the known combinatorial count of the Freudenthal decomposition.
why it matters
This count supplies the tet_count field inside the FreudenthalCert structure. The structure in turn certifies that the body diagonal is covered by exactly six tetrahedra, so that the sum of dihedral angles equals 2π and the deficit vanishes. The result therefore closes one of the combinatorial steps required by the Beltracchi response to confirm flatness of the triangulated cube.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.