jcost_stationarity_to_regge_nonlinear

formal source

 301    equivalence is a direct consequence of
 302    `nonlinear_field_curvature_identity` and the non-vanishing of
 303    `κ`. -/
 304theorem jcost_stationarity_to_regge_nonlinear
 305    {n : ℕ} (D : NonlinearDeficitFunctional n) (a : ℝ) (ha : 0 < a)
 306    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n)
 307    (hNL : NonlinearReggeJCostIdentity D a ha hinges G)
 308    (ε : LogPotential n) :
 309    exactJCostAction G ε = 0
 310      ↔ regge_sum D.functional (conformal_edge_length_field a ha ε) hinges = 0 := by
 311  have hκne : jcost_to_regge_factor ≠ 0 := jcost_to_regge_factor_ne_zero
 312  have hid := hNL ε
 313  constructor
 314  · intro h; rw [hid, h]; ring
 315  · intro h
 316    have hprod : jcost_to_regge_factor * exactJCostAction G ε = 0 := by
 317      rw [← hid]; exact h
 318    rcases mul_eq_zero.mp hprod with h1 | h2
 319    · exact absurd h1 hκne
 320    · exact h2
 321
 322/-! ## §6. Honest separation: weak-field is theorem, strong-field
 323    is theorem under one named hypothesis
 324
 325Philip's §6 concern is that the J ↔ Regge identification is
 326proved only in the weak-field regime. The decomposition
 327`exactJCostAction = laplacian_action + quarticRemainder` makes
 328the gap explicit at the J-cost side. The Regge side gap is
 329captured by `NonlinearReggeJCostIdentity`, which is proved for
 330cubic lattices at leading order by `cubic_linearization_discharge`
 331and which in the full non-linear regime requires either the
 332Cayley-Menger computation on simplicial meshes or the
 333Cheeger-Müller-Schrader theorem.
 334