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. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.