cube_dihedral
plain-language theorem explainer
The cube dihedral supplies the DihedralAngleData record whose cosine field is exactly zero. Workers on discrete curvature, Regge calculus, and simplicial complexes cite it to anchor the flat cubic lattice baseline. The definition is a direct record construction that discharges the cosine bounds via norm_num.
Claim. Let $d$ be the dihedral angle data for the cube. Then $d$ has cosine component $0$ satisfying $-1 ≤ 0 ≤ 1$, so the associated angle is $θ = arccos(0) = π/2$.
background
DihedralAngleData is the structure that carries a real cosine value together with explicit proofs that the value lies in [-1, 1]. The module defines the dihedral angle itself by $θ = arccos(cos)$ and proves the range [0, π]. The local theoretical setting is Phase C2 of the program to discharge the Regge deficit linearization hypothesis on general simplicial complexes, using the same minimal Cayley-Menger approach as the preceding phase.
proof idea
The definition constructs the DihedralAngleData record by setting the cosine field to 0 and discharging the lower-bound and upper-bound obligations with norm_num.
why it matters
This definition supplies the cube case that feeds vertex_angular_deficit and vertex_deficit_eq in AlphaDerivation as well as cube_dihedral_theta, cubic_lattice_flatSum and cubic_lattice_deficit_zero inside the same module. It fills the Phase C2 slot that anchors the flat-space sum Σ θ_σ = 2π at a non-singular edge, the D = 3 spatial dimension, and the baseline for the eight-tick octave in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.