`deficit_eq_zero_of_flat`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Geometry.DihedralAngle on GitHub at line 138.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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 :
 165    FlatSumCondition [cube_dihedral, cube_dihedral, cube_dihedral, cube_dihedral]
 166  cubic_deficit_zero :
 167    deficit [cube_dihedral, cube_dihedral, cube_dihedral, cube_dihedral] = 0
 168  theta_in_range : ∀ d : DihedralAngleData, 0 ≤ d.theta ∧ d.theta ≤ Real.pi

papers checked against this theorem

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