cube_dihedral_theta
plain-language theorem explainer
The declaration establishes that the dihedral angle of the cube equals exactly π/2. Researchers working on Regge calculus or simplicial discretizations of gravity cite it to anchor the flat cubic lattice case. The term-mode proof reduces the claim by unfolding the angle data structure and invoking the library identity arccos(0) = π/2.
Claim. The dihedral angle θ associated to the cube satisfies θ = π/2.
background
The module constructs dihedral angles for simplices from Cayley-Menger data. DihedralAngleData carries a cosine value in [-1,1] and defines θ as arccos of that cosine. The cube case draws on the upstream definition that sets the relevant cosine to zero, yielding the right angle between faces. The local setting is Phase C2 of the program to discharge the Regge deficit linearization hypothesis on general simplicial complexes, with parallel results for the regular tetrahedron angle arccos(1/3).
proof idea
The proof is a one-line term wrapper. It unfolds the theta projection from DihedralAngleData together with the cube definition, then applies the exact fact Real.arccos_zero.
why it matters
This supplies the cube_is_right_angle field inside dihedralAngleCert and is invoked by cubic_lattice_flatSum to show that four such angles sum to 2π. The result closes the cube case in Phase C2, feeding the development of Schläfli identities and the final simplicial discharge. It aligns with the framework requirement of D = 3 spatial dimensions and the flat-space sum condition at non-singular edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.