`totalDeficit`

definition

show as: view math explainer →

module: IndisputableMonolith.Geometry.Schlaefli
domain: Geometry
line: 150 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Geometry.Schlaefli on GitHub at line 150.

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

 147    (∑ h : Fin nH, (hinges h).area * M.dThetadL h e) = 0 := hS e
 148
 149/-- Total deficit functional: `Σ_h A_h · δ_h = Σ_h A_h · (2π − totalTheta h)`. -/
 150def totalDeficit {nH : ℕ} (hinges : Fin nH → SimplicialHingeData) : ℝ :=
 151  ∑ h : Fin nH, (hinges h).area * (hinges h).deficit
 152
 153/-! ## §5. Flat baseline -/
 154
 155/-- If every hinge satisfies the flat-sum condition, the total deficit
 156    vanishes. -/
 157theorem totalDeficit_flat {nH : ℕ}
 158    (hinges : Fin nH → SimplicialHingeData)
 159    (hFlat : ∀ h : Fin nH,
 160      DihedralAngle.FlatSumCondition (hinges h).dihedrals) :
 161    totalDeficit hinges = 0 := by
 162  unfold totalDeficit
 163  apply Finset.sum_eq_zero
 164  intro h _
 165  have : (hinges h).deficit = 0 := by
 166    unfold SimplicialHingeData.deficit
 167    exact DihedralAngle.deficit_eq_zero_of_flat _ (hFlat h)
 168  rw [this]; ring
 169
 170/-! ## §6. Certificate -/
 171
 172/-- Phase C3 certificate. -/
 173structure SchlaefliCert where
 174  flat_total_zero : ∀ {nH : ℕ} (hinges : Fin nH → SimplicialHingeData),
 175    (∀ h, DihedralAngle.FlatSumCondition (hinges h).dihedrals) →
 176    totalDeficit hinges = 0
 177  schlaefli_kills_sum : ∀ {nH nE : ℕ}
 178    (hinges : Fin nH → SimplicialHingeData)
 179    (M : DeficitDerivativeMatrix nH nE),
 180    SchlaefliIdentity hinges M →

papers checked against this theorem

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