IndisputableMonolith.Foundation.FreudenthalTriangulationCert
FreudenthalTriangulationCert supplies the basic combinatorial definitions for the unit cube and its standard Freudenthal triangulation into tetrahedra. Workers in certified geometry or computational topology would reference the vertex, edge, face, and tetrahedron counts. The module contains only definitions and equality statements with no proof content.
claimThe unit cube has eight vertices, twelve edges and six faces. Its Freudenthal triangulation decomposes it into six tetrahedra, with additional structure for body diagonals and new hinges.
background
Located in the Foundation layer, this module introduces the cube's vertex set, edge set and face set along with their cardinalities. It further defines the tetrahedron count in the Freudenthal decomposition and related objects such as bodyDiagonalTetrahedra and newHinges. These serve as the discrete geometric base for any subsequent triangulation arguments, drawing only on Mathlib and standing apart from the J-function or phi-based constructions in the main theory.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
These definitions establish the triangulation certificate that supports parent results on spatial decompositions within the Foundation. No specific downstream theorems are yet linked, but the module completes the basic count data required for Freudenthal-based arguments in three dimensions.
declarations in this module (18)
-
def
cubeVertices -
def
cubeEdges -
def
cubeFaces -
theorem
cubeVertices_eq -
theorem
cubeEdges_eq -
theorem
cubeFaces_eq -
def
freudenthalTetCount -
theorem
freudenthal_count -
def
bodyDiagonalTetrahedra -
theorem
body_diagonal_full_angle -
def
newHinges -
theorem
newHinges_decomp -
def
totalHingesSimp -
theorem
totalHinges_eq -
structure
ZeroDeficitCert -
def
zeroDeficitCert -
structure
FreudenthalCert -
def
freudenthalCert