cube_dihedral_is_right_angle
plain-language theorem explainer
The declaration states that the dihedral angle of a cube equals π/2. Workers on discrete gravity models in Recognition Science cite it to confirm zero curvature on cubic cells in the Regge action. The proof is a one-line term proof by reflexivity from the angle definition.
Claim. The dihedral angle of a cube equals $π/2$.
background
The module formalizes exact Regge calculus on the RS lattice, replacing linearized deficit-angle assumptions with piecewise-flat simplicial complexes. Curvature concentrates on codimension-2 hinges, and the Regge action is the sum over hinges of area times deficit angle. Edge lengths derive from the J-cost defect field on the Z³ × Z lattice. Simplex4D is a 4-simplex with ten edge lengths; HingeData records area and deficit at each hinge; DihedralAngle is obtained from the Cayley-Menger determinant.
proof idea
The proof is a one-line term proof by reflexivity (rfl). It holds because cube_dihedral_angle is defined to equal Real.pi / 2 exactly.
why it matters
The result verifies the flat-space case for cubic cells and supports regge_action_nonneg_flat together with deficit_from_dihedral in the same module. It aligns with the D = 3 spatial dimensions and eight-tick octave of the forcing chain, confirming that the Regge action vanishes on flat configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.