`JCostToEFE`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
domain: Foundation
line: 238 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge on GitHub at line 238.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 235-/
 236
 237/-- The complete J-cost → EFE derivation chain. -/
 238structure JCostToEFE where
 239  step1_jcost_defined : True
 240  step2_quadratic : ∀ (ε : ℝ), J_log_quadratic ε = ε ^ 2 / 2
 241  step3_laplacian_structure :
 242    ∀ (n : ℕ) (G : WeightedLedgerGraph n) (ε : Fin n → ℝ),
 243      (∀ i, discrete_laplacian G ε i = 0) →
 244      ∀ i, ∑ j : Fin n, G.weight i j * (ε i - ε j) = 0
 245  step4_kappa : jcost_to_regge_factor = 8 * phi ^ 5
 246  step5_kappa_pos : 0 < jcost_to_regge_factor
 247
 248/-- The chain is instantiated. -/
 249theorem jcost_to_efe_chain : JCostToEFE where
 250  step1_jcost_defined := trivial
 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. -/
 261theorem flat_is_vacuum {n : ℕ} (G : WeightedLedgerGraph n) :
 262    ∀ i, discrete_laplacian G (fun _ => (0 : ℝ)) i = 0 := by
 263  intro i
 264  unfold discrete_laplacian
 265  simp only [sub_self, mul_zero]
 266  exact Finset.sum_const_zero
 267
 268/-- Flat spacetime has zero J-cost. -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.