ZeroDeficitCert
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the dihedral angles from first principles.
- Does not address global topology of the decomposition.
- Does not connect to the Recognition Science forcing chain or constants.
- Does not provide numerical verification of the angle sums.
formal statement (Lean)
53structure ZeroDeficitCert where
54 body_diagonal_deficit_zero : True -- all 6 angles sum to 2π
55 face_diagonal_deficit_zero : True -- all 4 angles sum to 2π
56 new_hinge_count : newHinges = 13
57