cube_dihedral_angle
plain-language theorem explainer
The dihedral angle of a cube is defined as exactly π/2. Researchers modeling discrete gravity on cubic lattices in Recognition Science cite this when verifying flat configurations and zero deficit sums. The definition is a direct constant assignment that matches the geometric right-angle property of all cube faces.
Claim. For a cube with all edges of equal length and all face angles right angles, the dihedral angle equals $π/2$.
background
The module formalizes exact Regge calculus on the RS lattice Z³ × Z. Curvature concentrates on codimension-2 hinges, with the Regge action given by the sum over hinges of (area × deficit angle). Edge lengths are supplied by the J-cost defect field from the simplicial ledger. Key supporting structures include Simplex4D (a 4-simplex with 10 edge lengths), HingeData (area and deficit at each hinge), and DihedralAngle (computed via Cayley-Menger determinant). Upstream results on phi-forcing and spectral emergence supply the discrete length scales and gauge content that fix the lattice geometry.
proof idea
One-line definition that directly assigns the constant Real.pi / 2, matching the known right-angle dihedral property of Euclidean cubes.
why it matters
This definition supplies the exact input required by the downstream theorem cube_dihedral_is_right_angle and by deficit-angle calculations in flat cubic lattices. It anchors the Regge action for the RS discrete gravity programme, consistent with the eight-tick octave and D = 3 spatial dimensions. The value closes the flat-configuration case where total deficit sums to zero, aligning with the paper's replacement of linearized deficit ansatzes by full Regge machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.