cubeFaces
plain-language theorem explainer
The declaration delivers the integer six as the face count of the unit cube. Researchers formalizing Freudenthal triangulations or cardinality spectra in Recognition Science would cite it when decomposing the cube into tetrahedra. The definition proceeds by direct constant assignment with no lemmas applied.
Claim. The unit cube has six faces, expressed as the natural number $6$.
background
The module formalizes combinatorial facts for the Freudenthal triangulation of the unit cube $[0,1]^3$, which decomposes into six congruent tetrahedra sharing the body diagonal. All thirteen new hinges (twelve face diagonals plus one body diagonal) carry zero deficit angle. Upstream definitions in the cardinality spectrum and paradigm shift lattice modules introduce the identical constant six, often annotated as twice the spatial dimension.
proof idea
The definition is a direct constant assignment of six.
why it matters
This constant supplies the cube face count to the CardinalitySpectrumCert structure, where it satisfies the relation equating faces to twice the spatial dimension and thereby confirms three spatial dimensions. It aligns with the eight-tick octave in the unified forcing chain and supports downstream theorems that equate six to two times three and compute $6^3 = 216$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.