freudenthalCert
plain-language theorem explainer
The freudenthalCert definition supplies an explicit witness to the FreudenthalCert structure for the unit cube. It records eight vertices, twelve edges, six faces, six tetrahedra under the Freudenthal decomposition, thirteen new hinges, and zero angular deficit at every hinge. Researchers checking combinatorial flatness in three-dimensional simplicial complexes cite this object. The construction assembles the record by direct substitution of reflexivity proofs together with the freudenthal_count and body_diagonal_full_angle lemmas.
Claim. Let $C$ be the structure asserting that the unit cube has eight vertices, twelve edges and six faces, that the Freudenthal triangulation produces six tetrahedra, that thirteen new hinges appear, that the normalized sum of the six dihedral contributions around the body diagonal equals one, and that the zero-deficit certificate holds on every new hinge. Then freudenthalCert is the explicit term witnessing $C$.
background
The module records the combinatorial certificate for the Freudenthal triangulation of the unit cube $[0,1]^3$. The module documentation states that this decomposition yields six congruent tetrahedra sharing the body diagonal and that all thirteen new hinges (twelve face diagonals plus one body diagonal) carry zero angular deficit. The FreudenthalCert structure packages the vertex-edge-face counts, the tetrahedron count, the hinge count, the body-angle identity, and the zero-deficit record. Upstream results include the freudenthal_count theorem establishing the tetrahedron count, the body_diagonal_full_angle theorem stating that six times one-sixth equals one, and the zeroDeficitCert definition whose body-diagonal and face-diagonal deficits are recorded as trivial.
proof idea
The definition constructs the FreudenthalCert record directly. It populates the cube_data field with a triple of reflexivity proofs, invokes the freudenthal_count theorem for the tetrahedron count, uses reflexivity for the new-hinge count, applies the body_diagonal_full_angle theorem for the angle check, and inserts the zeroDeficitCert definition for the deficit field.
why it matters
This definition supplies the concrete combinatorial certificate required by the Freudenthal triangulation argument in the Beltracchi response. It closes the verification that the unit-cube decomposition introduces no angular deficit at the new hinges, thereby confirming local flatness in the discrete setting. The construction relies on the three-dimensional structure implicit in the Recognition Science forcing chain, though it remains purely combinatorial. No downstream theorems are recorded yet, leaving open its integration into curvature calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.