WellShapedData

formal source

 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
 118  coeffs : LinearizationCoefficients nH nE
 119  schlaefli : SchlaefliIdentity complex.hinges coeffs.toDeficitDerivativeMatrix
 120
 121/-! ## §4. Linearized action vanishes at first order
 122
 123The key consequence: under the flat background and Schläfli's identity,
 124the *first-order* Regge action vanishes. This means the leading
 125non-trivial Regge action is *quadratic* in the perturbation, precisely
 126matching the J-cost Dirichlet energy.
 127
 128The statement we need:
 129
 130  `Σ_h A_h · linearizedDeficit_h(η) = - Σ_e (Σ_h A_h · ∂θ_h/∂L_e) · η_e
 131                                   = 0       (by Schläfli per edge).`
 132-/
 133
 134/-- The linear (first-order) part of the Regge action vanishes under
 135    Schläfli's identity. -/
 136theorem linear_regge_vanishes {nH nE : ℕ}
 137    (W : WellShapedData nH nE) (η : EdgePerturbation nE) :
 138    (∑ h : Fin nH, (W.complex.hinges h).area *
 139      linearizedDeficit W.coeffs η h) = 0 := by
 140  unfold linearizedDeficit
 141  -- Rewrite the sum: move the minus sign out, then swap summation order.
 142  have h_swap :
 143      (∑ h : Fin nH, (W.complex.hinges h).area *
 144        -(∑ e : Fin nE, W.coeffs.dThetadL h e * η.eta e))
 145      = - ∑ e : Fin nE,
 146          η.eta e * (∑ h : Fin nH, (W.complex.hinges h).area * W.coeffs.dThetadL h e) := by