NonlinearDeficitFunctional

formal source

 256    linear functional to strong-field configurations. Concretely
 257    it is a `DeficitAngleFunctional` that additionally satisfies
 258    the non-linear matching identity below. -/
 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`. -/
 266def NonlinearReggeJCostIdentity
 267    {n : ℕ} (D : NonlinearDeficitFunctional n) (a : ℝ) (ha : 0 < a)
 268    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n) : Prop :=
 269  ∀ ε : LogPotential n,
 270    regge_sum D.functional (conformal_edge_length_field a ha ε) hinges
 271      = jcost_to_regge_factor * exactJCostAction G ε
 272
 273/-- **THEOREM (under hypothesis).** If the non-linear matching
 274    identity holds, then the J-cost Dirichlet principle reproduces
 275    the Regge equations in the **full non-linear regime**, not just
 276    the weak-field one. Stated: `exactJCostAction` is `(1/κ)` times
 277    the full Regge sum. -/
 278theorem nonlinear_field_curvature_identity
 279    {n : ℕ} (D : NonlinearDeficitFunctional n) (a : ℝ) (ha : 0 < a)
 280    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n)
 281    (hNL : NonlinearReggeJCostIdentity D a ha hinges G)
 282    (ε : LogPotential n) :
 283    exactJCostAction G ε
 284      = (1 / jcost_to_regge_factor) *
 285          regge_sum D.functional (conformal_edge_length_field a ha ε) hinges := by
 286  have hκ : jcost_to_regge_factor ≠ 0 := jcost_to_regge_factor_ne_zero
 287  have hid := hNL ε
 288  calc
 289    exactJCostAction G ε