FreudenthalCert
plain-language theorem explainer
FreudenthalCert packages the combinatorial invariants of the unit cube's decomposition into six tetrahedra, asserting eight vertices, twelve edges, six faces, six tetrahedra, thirteen new hinges, a normalized body-angle sum of one, and zero angular deficit at the new hinges. Discrete geometers or Recognition Science researchers working on spatial discretizations cite this structure to certify topological and angular consistency of the Freudenthal triangulation. The definition assembles these facts directly from sibling combinatorial constants.
Claim. A Freudenthal triangulation certificate for the unit cube is a record containing the conjunction of equalities asserting eight vertices, twelve edges and six faces; the count of six tetrahedra; thirteen new hinges; the identity $6 times (1/6) = 1$; and a zero-deficit certificate requiring that the body diagonal (six angles summing to $2pi$) and face diagonals (four angles summing to $2pi$) each carry zero angular deficit.
background
The module formalizes the Freudenthal triangulation of the unit cube $[0,1]^3$ into six congruent tetrahedra, as described in the Beltracchi response section 4. The cube has eight vertices, twelve edges and six faces by definition; the decomposition introduces six tetrahedra sharing the body diagonal and creates thirteen new hinges (twelve face diagonals plus one body diagonal). Upstream definitions fix cubeVertices as eight, cubeEdges as twelve, cubeFaces as six and freudenthalTetCount as six. The referenced ZeroDeficitCert structure requires body-diagonal deficit zero (six angles sum to $2pi$), face-diagonal deficit zero (four angles sum to $2pi$), and newHinges equal to thirteen.
proof idea
As a structure definition with an empty proof body, FreudenthalCert simply records the required fields by direct reference to the pre-established combinatorial constants cubeVertices, cubeEdges, cubeFaces, freudenthalTetCount, newHinges and the ZeroDeficitCert structure. No tactics or lemmas are invoked beyond these equality assertions.
why it matters
This certificate is instantiated by the downstream freudenthalCert definition in the same module, which supplies concrete values to confirm the triangulation. It supplies the combinatorial content of the Freudenthal decomposition required by the Recognition Science framework for three-dimensional space (D=3), ensuring zero deficit angles around new hinges and supporting the zero-deficit condition used in the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.