pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.FreudenthalTriangulationCert

show as:
view Lean formalization →

This module enumerates the combinatorial elements of the Freudenthal triangulation of the unit cube in three dimensions. It supplies explicit vertex, edge, face, and tetrahedron counts together with body-diagonal and hinge decompositions. The content consists entirely of direct definitions and equalities with no proofs, providing the discrete geometric base for spatial structure in Recognition Science.

claimThe unit cube has vertex set $V = (0,1)^3$ with $|V|=8$, edge set $E$ with $|E|=12$, face set $F$ with $|F|=6$, and Freudenthal triangulation into $T=6$ tetrahedra whose body diagonals and new hinges are enumerated explicitly.

background

Recognition Science models three-dimensional space via the eight-tick octave and D=3 forcing step, which requires a concrete triangulation of the unit cube. This module introduces the vertex set cubeVertices, the twelve cubeEdges, the six cubeFaces, and the freudenthalTetCount of tetrahedra. It further defines bodyDiagonalTetrahedra together with newHinges and newHinges_decomp to record the hinge structure that arises when the cube is subdivided along its space diagonals. All objects are constructed inside Mathlib's finite-set and enumeration machinery.

proof idea

This is a definition module, no proofs. It consists of direct enumerations of the eight vertices, twelve edges, six faces, and the six tetrahedra of the Freudenthal subdivision, together with equality lemmas that confirm the counts and the hinge decomposition.

why it matters in Recognition Science

The module supplies the base combinatorial counts that feed into any later theorem on spatial discretization or hinge-based dynamics within the Recognition framework. It directly supports the T8 step that forces D=3 and the geometric scaffolding needed for mass formulas on the phi-ladder. No downstream theorems are yet recorded, but the definitions close the combinatorial foundation for cube triangulations.

scope and limits

declarations in this module (18)