NonlinearReggeJCostIdentity

formal source

 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 ε
 290        = ((1 / jcost_to_regge_factor) * jcost_to_regge_factor)
 291            * exactJCostAction G ε := by field_simp [hκ]
 292    _   = (1 / jcost_to_regge_factor)
 293            * (jcost_to_regge_factor * exactJCostAction G ε) := by ring
 294    _   = (1 / jcost_to_regge_factor)
 295            * regge_sum D.functional (conformal_edge_length_field a ha ε) hinges := by
 296              rw [← hid]