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

jcost_to_efe_chain

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)

 249theorem jcost_to_efe_chain : JCostToEFE where
 250  step1_jcost_defined := trivial

proof body

Term-mode proof.

 251  step2_quadratic := fun _ => rfl
 252  step3_laplacian_structure := fun _ G ε h i => stationarity_iff_laplacian_zero G ε h i
 253  step4_kappa := jcost_to_regge_factor_eq
 254  step5_kappa_pos := jcost_to_regge_factor_pos
 255
 256/-! ## Vacuum Solution Compatibility
 257
 258Flat spacetime (ε = 0 everywhere) is the vacuum solution. -/
 259
 260/-- Zero potential is a stationary point of J-cost. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (21)

Lean names referenced from this declaration's body.