pith. machine review for the scientific record. sign in
theorem proved tactic proof

jcost_stationarity_to_regge_nonlinear

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Tactic-mode proof.

 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
 335Under the named hypothesis, the identity becomes strong-field
 336valid, and the J-cost stationarity implies the Regge
 337stationarity (and hence EFE) without a weak-field restriction. -/
 338
 339/-- **MASTER CERTIFICATE.** The non-linear bridge with its hypothesis
 340    explicitly separated. -/

depends on (39)

Lean names referenced from this declaration's body.

… and 9 more