LinearizationCoefficients

formal source

  84/-- Linearization coefficients: for each (hinge, edge) pair, the partial
  85    derivative of the deficit angle with respect to the edge length,
  86    evaluated at the flat background. -/
  87structure LinearizationCoefficients (nH nE : ℕ) extends
  88    DeficitDerivativeMatrix nH nE
  89
  90/-! ## §2. Predicted deficit
  91
  92Given linearization coefficients, the predicted deficit at each hinge
  93under perturbation `η` is
  94
  95  `δ̂_h = - Σ_e (∂θ_h / ∂L_e) · η_e`
  96
  97(the minus sign because deficit = 2π − totalTheta). -/
  98
  99/-- Linearized deficit at hinge `h` under perturbation `η`. -/
 100def linearizedDeficit {nH nE : ℕ}
 101    (M : LinearizationCoefficients nH nE) (η : EdgePerturbation nE)
 102    (h : Fin nH) : ℝ :=
 103  - (∑ e : Fin nE, M.dThetadL h e * η.eta e)
 104
 105/-! ## §3. The well-shapedness bundle
 106
 107A `WellShaped` package certifies that:
 108
 1091. The complex is flat at the background.
 1102. Linearization coefficients exist.
 1113. Schläfli's identity holds for those coefficients.
 112
 113This is exactly what Phase C5 needs. -/
 114
 115/-- A complete well-shapedness package for the linearization. -/
 116structure WellShapedData (nH nE : ℕ) where
 117  complex : FlatSimplicialComplex nH nE