pith. machine review for the scientific record. sign in
structure definition def or abbrev

DeficitDerivativeMatrix

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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
 127    full proof requires boundary-integration machinery not yet in
 128    Mathlib. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.