deficit_angle

formal source

 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
 146  unfold deficit_angle; linarith
 147
 148/-! ## The Regge Action -/
 149
 150/-- The Regge action: sum over all hinges of (area × deficit angle).
 151    S_Regge = sum_h A_h * delta_h