DihedralAngleData

formal source

  90
  91    The exact formula involves the Cayley-Menger determinant, but for
  92    formalization we parameterize by the cosine value directly. -/
  93structure DihedralAngleData where
  94  cosine : ℝ
  95  cosine_bound : -1 ≤ cosine ∧ cosine ≤ 1
  96
  97noncomputable def dihedral_from_cosine (d : DihedralAngleData) : ℝ :=
  98  Real.arccos d.cosine
  99
 100/-- For a CUBE (all edges = a, all right angles), the dihedral angle is pi/2. -/
 101noncomputable def cube_dihedral_angle : ℝ := Real.pi / 2
 102
 103/-- The dihedral angle of a cube is pi/2 (90 degrees). -/
 104theorem cube_dihedral_is_right_angle :
 105    cube_dihedral_angle = Real.pi / 2 := rfl
 106
 107/-! ## Deficit Angles -/
 108
 109/-- A hinge in Regge calculus is a codimension-2 face.
 110    In 4D: a hinge is a triangle (2-face).
 111    In 3D: a hinge is an edge (1-face).
 112
 113    The deficit angle at a hinge is 2*pi minus the sum of dihedral
 114    angles of all simplices meeting at that hinge. -/
 115structure HingeData where
 116  area : ℝ
 117  dihedral_angles : List ℝ
 118  area_pos : 0 < area
 119
 120/-- The deficit angle at a hinge: 2*pi - sum of dihedral angles. -/
 121noncomputable def deficit_angle (h : HingeData) : ℝ :=
 122  2 * Real.pi - h.dihedral_angles.sum
 123