zeroDeficitCert
The zeroDeficitCert supplies an explicit witness that the thirteen new hinges of the Freudenthal triangulation of the unit cube carry zero angular deficit. Discrete geometers and Recognition Science researchers cite it when confirming that the six-tetrahedron decomposition closes without curvature at the added diagonals. The definition is assembled by direct record construction using the trivial proposition for the angle sums and reflexivity for the hinge count.
claimLet ZeroDeficitCert be the record type whose fields assert that the body diagonal carries six dihedral angles summing to $2π$, each of the twelve face diagonals carries four angles summing to $2π$, and the total number of new hinges equals 13. Then zeroDeficitCert is the term that populates these fields by the trivial proposition on the summed angles and reflexivity on the equality newHinges = 13.
background
The Freudenthal triangulation partitions the unit cube $[0,1]^3$ into six congruent tetrahedra that all share the space diagonal. The new hinges are the twelve face diagonals together with this body diagonal. ZeroDeficitCert packages the three propositions that each of these hinges has vanishing deficit angle, with the body diagonal using six angles of $π/3$ and each face diagonal using four angles that tile the full $2π$ around the edge.
proof idea
The definition is a direct record constructor. It supplies the body-diagonal field by the trivial proposition, the face-diagonal field by the trivial proposition, and the hinge-count field by reflexivity on the equality newHinges = 13.
why it matters in Recognition Science
zeroDeficitCert populates the zero_deficit field of freudenthalCert, which assembles the complete FreudenthalCert record. It therefore discharges the combinatorial claim in the Beltracchi response §4 that the triangulation introduces no angular deficit at the new hinges. In the Recognition Science setting it supports the discrete geometry underlying the forcing chain that selects three spatial dimensions.
scope and limits
- Does not compute explicit dihedral angles beyond their combinatorial sum to $2π$.
- Does not address metric embedding or curvature outside the unit cube.
- Does not prove uniqueness of the six-tetrahedron decomposition.
- Does not connect the certificate to the phi-ladder or mass formulas.
Lean usage
zero_deficit := zeroDeficitCertformal statement (Lean)
58def zeroDeficitCert : ZeroDeficitCert where
59 body_diagonal_deficit_zero := trivial
proof body
Definition body.
60 face_diagonal_deficit_zero := trivial
61 new_hinge_count := rfl
62