freudenthal_count
plain-language theorem explainer
The Freudenthal triangulation decomposes the unit cube into precisely six tetrahedra. Researchers verifying zero-deficit hinge conditions in cubic lattices cite this count when assembling the full certificate for the body diagonal and face diagonals. The proof is a direct reflexivity step on the explicit definition of the tetrahedron count.
Claim. The Freudenthal decomposition of the unit cube $[0,1]^3$ into tetrahedra satisfies $N = 6$, where $N$ is the number of tetrahedra in the decomposition.
background
The module records the combinatorial facts of the Freudenthal triangulation of the unit cube: eight vertices, twelve edges, six faces, and a decomposition into six tetrahedra that share the body diagonal. The definition freudenthalTetCount : ℕ := 6 supplies the explicit count used for subsequent hinge and deficit calculations. The local setting is the zero-deficit certificate for all thirteen new hinges (twelve face diagonals plus one body diagonal) in three dimensions.
proof idea
This is a one-line wrapper that applies reflexivity directly to the definition freudenthalTetCount := 6.
why it matters
The result supplies the tetrahedron count to the freudenthalCert structure, which assembles the full zero-deficit certificate including body diagonal angle and hinge data. It fills the combinatorial step required for the three-dimensional spatial structure (T8) in the Recognition Science framework, where the cube decomposition guarantees flat curvature at the new hinges. The parent theorem freudenthalCert uses this count to close the certificate for the Beltracchi response.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.