DeficitDerivativeMatrix

formal source

 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
 127    full proof requires boundary-integration machinery not yet in
 128    Mathlib. -/
 129def SchlaefliIdentity {nH nE : ℕ}
 130    (hinges : Fin nH → SimplicialHingeData)
 131    (M : DeficitDerivativeMatrix nH nE) : Prop :=
 132  ∀ e : Fin nE,
 133    (∑ h : Fin nH, (hinges h).area * M.dThetadL h e) = 0
 134
 135/-! ## §4. Consequences of Schläfli's identity
 136
 137Schläfli's identity makes the second term of the Regge variation vanish,
 138leaving only the `∂A/∂L · δ` piece. This is what the Regge equations of
 139motion look like. -/
 140
 141/-- Under Schläfli, the `Σ A · dθ/dL` term in the Regge variation is
 142    identically zero. -/