ZeroDeficitCert
plain-language theorem explainer
ZeroDeficitCert records that the thirteen new hinges of the Freudenthal triangulation of the unit cube carry zero angular deficit. It is referenced inside the parent FreudenthalCert to close the combinatorial check that six tetrahedra meet without curvature. The definition populates the two deficit fields with the trivial proposition and the hinge count with the constant 13.
Claim. The zero-deficit certificate structure consists of three fields: the body-diagonal deficit vanishes (six dihedral angles sum to $2π$), each face-diagonal deficit vanishes (four dihedral angles sum to $2π$), and the number of new hinges equals 13.
background
The module treats the Freudenthal triangulation of the unit cube, which decomposes it into six congruent tetrahedra sharing the body diagonal. New hinges are the twelve face diagonals together with the single body diagonal. The upstream definition newHinges fixes this count at 13. The local setting is the combinatorial certificate that all thirteen hinges are surrounded by a full $2π$ angle and therefore carry zero deficit.
proof idea
The declaration is a bare structure definition. Its concrete instance is obtained by applying the trivial tactic to the two deficit propositions and reflexivity to the equality that sets the hinge count to 13.
why it matters
ZeroDeficitCert supplies the zero_deficit field required by the parent structure FreudenthalCert. It thereby completes the certificate that the Freudenthal decomposition introduces no angular deficit at its new hinges. The module documentation ties this directly to the combinatorial facts of the unit cube and its six tetrahedra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.