`deficit`

definition

show as: view math explainer →

module: IndisputableMonolith.Geometry.Schlaefli
domain: Geometry
line: 96 · 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 96.

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

  93  DihedralAngle.sumThetas h.dihedrals
  94
  95/-- Deficit at the hinge: `2π − Σ θ`. -/
  96def deficit (h : SimplicialHingeData) : ℝ :=
  97  DihedralAngle.deficit h.dihedrals
  98
  99theorem deficit_eq (h : SimplicialHingeData) :
 100    h.deficit = 2 * Real.pi - h.totalTheta := rfl
 101
 102end SimplicialHingeData
 103
 104/-! ## §2. Variational data
 105
 106For Schläfli's identity we need derivatives of `θ_h` with respect to each
 107edge length `L_e`. We package these as a matrix of real numbers, one per
 108(hinge, edge) pair. The identity below constrains this matrix. -/
 109
 110/-- A matrix of deficit-angle derivatives: `dThetadL h e` is intended
 111    to be `∂(totalTheta h) / ∂(len e)`. -/
 112structure DeficitDerivativeMatrix (nH nE : ℕ) where
 113  dThetadL : Fin nH → Fin nE → ℝ
 114
 115/-! ## §3. Schläfli's identity as a hypothesis -/
 116
 117/-- **SCHLÄFLI'S IDENTITY** (piecewise-flat form).
 118
 119    For a finite collection of hinges (indexed by `Fin nH`) with areas
 120    `A_h` and a matrix `dThetadL` of dihedral-angle derivatives with
 121    respect to edge lengths, the weighted sum vanishes:
 122
 123    `∀ e, Σ_h A_h · (∂θ_h / ∂L_e) = 0`.
 124
 125    This is the classical local identity; see Regge (1961, eq. 2.8) and
 126    Brewin (2000). We record it as a hypothesis structure because the

papers checked against this theorem

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