cube_dihedral_angle

formal source

  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
 124/-- For a flat configuration, all hinges have zero deficit. -/
 125theorem flat_deficit_zero (h : HingeData)
 126    (h_flat : h.dihedral_angles.sum = 2 * Real.pi) :
 127    deficit_angle h = 0 := by
 128  unfold deficit_angle; linarith
 129
 130/-- On the flat cubic lattice Z^3, each edge is shared by 4 cubes.
 131    Each cube contributes dihedral angle pi/2.