sumThetas

formal source

 123We formalize this as a condition on a `List DihedralAngleData`. -/
 124
 125/-- The sum of the `theta` values over a list of dihedral data. -/
 126def sumThetas (ds : List DihedralAngleData) : ℝ :=
 127  (ds.map DihedralAngleData.theta).sum
 128
 129/-- The flat-sum condition: the total dihedral angle at a hinge equals `2π`. -/
 130def FlatSumCondition (ds : List DihedralAngleData) : Prop :=
 131  sumThetas ds = 2 * Real.pi
 132
 133/-- The deficit at a hinge is `2π − Σ θ`. -/
 134def deficit (ds : List DihedralAngleData) : ℝ :=
 135  2 * Real.pi - sumThetas ds
 136
 137/-- At a flat hinge, the deficit is zero. -/
 138theorem deficit_eq_zero_of_flat (ds : List DihedralAngleData)
 139    (h : FlatSumCondition ds) : deficit ds = 0 := by
 140  unfold deficit
 141  rw [h]; ring
 142
 143/-- Four cube-dihedral angles (`π/2 + π/2 + π/2 + π/2 = 2π`) sum to `2π`:
 144    the classical "Z³ lattice is flat" statement. -/
 145theorem cubic_lattice_flatSum :
 146    FlatSumCondition [cube_dihedral, cube_dihedral, cube_dihedral, cube_dihedral] := by
 147  unfold FlatSumCondition sumThetas
 148  simp only [List.map, List.sum_cons, List.sum_nil, cube_dihedral_theta]
 149  ring
 150
 151/-- The deficit at a flat cubic hinge is zero (the baseline identity
 152    already present in `ReggeCalculus.cubic_lattice_flat` for the
 153    π/2 × 4 = 2π case, now lifted to the `DihedralAngle` API). -/
 154theorem cubic_lattice_deficit_zero :
 155    deficit [cube_dihedral, cube_dihedral, cube_dihedral, cube_dihedral] = 0 :=
 156  deficit_eq_zero_of_flat _ cubic_lattice_flatSum