body_diagonal_full_angle
plain-language theorem explainer
The theorem confirms that six tetrahedra meeting along the body diagonal each contribute an angle of one-sixth of a full turn and therefore sum exactly to one full turn. It is invoked inside the Freudenthal triangulation certificate to record zero angular deficit at that hinge. The verification is performed by a single rational normalization step.
Claim. The normalized angular sum around the body diagonal satisfies $6 · (1/6) = 1$.
background
The module treats the unit cube [0,1]³ decomposed into six congruent tetrahedra via the Freudenthal triangulation. All thirteen new hinges (twelve face diagonals plus the single body diagonal) are required to carry zero deficit angle. For the body diagonal the six tetrahedra meet and each supplies a dihedral angle normalized to 1/6 of a full rotation, so their total contribution must equal 1 to close the link without deficit.
proof idea
The proof is a one-line term wrapper that applies norm_num to the rational arithmetic 6 * (1/6).
why it matters
The result supplies the body_angle field inside the freudenthalCert definition. That certificate records the combinatorial facts (cube data, tet count, new hinges, zero deficit) needed for the triangulation statement in the foundation layer. It thereby closes the zero-deficit check for the body diagonal that the module doc lists as essential for the six-tetrahedron decomposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.