Pith. sign in
module module low

IndisputableMonolith.Foundation.FreudenthalTriangulationCert

show as:
view Lean formalization →

FreudenthalTriangulationCert supplies Lean definitions for vertex, edge, face, and tetrahedra counts under the Freudenthal triangulation of the unit cube. Researchers in discrete geometry or lattice-based physics models would cite these certified counts for 3D simplicial decompositions. The module consists entirely of direct definitions with no proof obligations or external Recognition Science dependencies.

claimThe module defines $\mathrm{cubeVertices}=8$, $\mathrm{cubeEdges}=12$, $\mathrm{cubeFaces}=6$, $\mathrm{freudenthalTetCount}=6$, and related body-diagonal tetrahedra decompositions for the unit cube.

background

The module sits in the Foundation domain and introduces explicit geometric counts for the unit cube. cubeVertices records the eight corners, cubeEdges the twelve edges, and cubeFaces the six faces. Further definitions cover the tetrahedra count in the Freudenthal triangulation together with body diagonal tetrahedra and new hinge decompositions. The local setting is a self-contained certificate of the standard 3-cube simplicial decomposition, preparatory for later volume or angle work; the supplied doc comment flags the unit cube vertex count as the central object.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the base geometric counts that feed parent theorems on spatial discretization and triangulation within the Recognition Science framework. It directly supports the D=3 spatial dimension and eight-tick octave landmarks by certifying the cube decomposition into six tetrahedra. No specific downstream theorems are recorded in the dependency graph.

scope and limits

declarations in this module (18)