DihedralAngleData
plain-language theorem explainer
DihedralAngleData packages a real cosine in the closed interval from negative one to one as the parameter for a dihedral angle, together with its arccos definition. Workers on discrete gravity and Regge calculus discretizations cite this record when parameterizing edge angles in tetrahedra for deficit calculations. The construction is a plain structure declaration that directly embeds the arccos definition with no additional lemmas.
Claim. A structure consisting of a real number $c$ satisfying $-1 ≤ c ≤ 1$, representing the cosine of a dihedral angle $θ$ defined by $θ = arccos(c)$.
background
This module sets up dihedral angles at edges and 2-faces of simplices from Cayley-Menger data as Phase C2 toward discharging the Regge deficit linearization hypothesis on general simplicial complexes. A dihedral angle at an edge of a tetrahedron is the angle between the two faces sharing that edge. The structure carries a cosine in [-1,1] and defines the angle via arccos, matching the parameterization in the upstream ReggeCalculus.DihedralAngleData which states: 'The dihedral angle of a tetrahedron along edge (0,1) is the angle between the two faces sharing that edge... parameterized by the cosine value directly.'
proof idea
The declaration is a structure definition that introduces the field cosine together with its bounds and the auxiliary definition theta as Real.arccos applied to that cosine. No tactics are required beyond the record construction itself.
why it matters
This structure is the foundational data type for all subsequent dihedral angle calculations in the module. It is used by cos_theta to recover the cosine, by cube_dihedral and regular_tet_dihedral to instantiate concrete values, by deficit to compute 2π minus the sum of thetas, and by DihedralAngleCert to certify flat sums. It advances Phase C2 of the program to formalize Regge calculus on simplicial complexes, enabling Schläfli's identity in Phase C3 and the flat-space sum condition Σ θ_σ = 2π at non-singular edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.