SchlaefliIdentity

formal source

 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. -/
 143theorem schlaefli_kills_dtheta {nH nE : ℕ}
 144    (hinges : Fin nH → SimplicialHingeData)
 145    (M : DeficitDerivativeMatrix nH nE)
 146    (hS : SchlaefliIdentity hinges M) (e : Fin nE) :
 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,