flat_deficit_zero

formal source

 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
 152
 153    This is the discrete analog of the Einstein-Hilbert action:
 154    S_EH = (1/2kappa) * integral R * sqrt(g) d^4x
 155