`deficit`

definition

show as: view math explainer →

module: IndisputableMonolith.Geometry.DihedralAngle
domain: Geometry
line: 134 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Geometry.DihedralAngle on GitHub at line 134.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 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
 157
 158/-! ## §4. Certificate -/
 159
 160structure DihedralAngleCert where
 161  cube_is_right_angle : cube_dihedral.theta = Real.pi / 2
 162  regular_tet_in_range :
 163    0 < regular_tet_dihedral.theta ∧ regular_tet_dihedral.theta < Real.pi
 164  cubic_flat_sum :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.