259structure NonlinearDeficitFunctional (n : ℕ) where 260 functional : DeficitAngleFunctional n 261 262/-- The **non-linear Regge ↔ J-cost matching hypothesis.** Under 263 this hypothesis, the Regge sum on the non-linear deficit 264 functional equals `κ · exactJCostAction`, not merely 265 `κ · laplacian_action`. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.