HingeData

formal source

 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.
 132    Sum = 4 * pi/2 = 2*pi, so deficit = 0. -/
 133theorem cubic_lattice_flat :
 134    2 * Real.pi - 4 * (Real.pi / 2) = 0 := by ring
 135
 136/-- Deficit angle is positive when total angle < 2*pi (positive curvature). -/
 137theorem deficit_pos_of_angle_deficit (h : HingeData)
 138    (h_less : h.dihedral_angles.sum < 2 * Real.pi) :
 139    0 < deficit_angle h := by
 140  unfold deficit_angle; linarith
 141
 142/-- Deficit angle is negative when total angle > 2*pi (negative curvature). -/
 143theorem deficit_neg_of_angle_excess (h : HingeData)
 144    (h_more : 2 * Real.pi < h.dihedral_angles.sum) :
 145    deficit_angle h < 0 := by