zeroDeficitCert
plain-language theorem explainer
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.
Claim. Let 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.