cube_dihedral
plain-language theorem explainer
The dihedral angle of a cube is defined as π/2 radians. Researchers modeling Regge calculus on cubic lattices cite this as the exact flat-space reference before summing angles around edges. The declaration is a direct constant assignment in the reals.
Claim. The dihedral angle of a cube equals $π/2$.
background
The module develops discrete curvature from deficit angles on deformed cubic lattices, following Regge's 1961 approach where the action sums deficit times area and converges to the Einstein-Hilbert integral. In the flat case, four dihedral angles of π/2 sum to 2π around each edge, yielding zero deficit. This rests on the J-cost structure from PhiForcingDerived.of and the Q3 lattice forcing from SpectralEmergence.of, which encode the strain that deforms angles away from the flat value.
proof idea
The definition is a one-line assignment of the constant Real.pi / 2, providing the exact right angle for all subsequent deficit formulas.
why it matters
It supplies the reference angle for vertex_angular_deficit in AlphaDerivation, which computes 2π - 3*(π/2) as the discrete curvature concentration at vertices of Q3. This anchors the connection between ledger J-cost strain and Regge curvature, supporting the flat-sum identity in cubic_lattice_deficit_zero and the overall derivation of D=3 from the eight-tick octave in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.