`kinetic_nonneg`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.Fields.Integration
domain: Relativity
line: 78 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Relativity.Fields.Integration on GitHub at line 78.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  75
  76/-- Kinetic action is nonnegative for positive-signature spatial parts.
  77    STATUS: SCAFFOLD — Proof simplified with placeholder sqrt_minus_g = 1. -/
  78theorem kinetic_nonneg (φ : ScalarField) (g : MetricTensor) (vol : VolumeElement)
  79    (hSign : ∀ x, 0 ≤ gradient_squared φ g x) :
  80  0 ≤ kinetic_action φ g vol := by
  81  unfold kinetic_action integrate_scalar sqrt_minus_g
  82  apply mul_nonneg (by norm_num)
  83  apply mul_nonneg (pow_nonneg (le_of_lt vol.grid_spacing_pos) 4)
  84  apply Finset.sum_nonneg
  85  intro i _
  86  apply mul_nonneg (by norm_num : (0 : ℝ) ≤ 1)
  87  apply hSign
  88
  89
  90/-- Einstein-Hilbert action: (M_P^2/2) ∫ √(-g) R d^4x. -/
  91noncomputable def einstein_hilbert_action
  92  (g : MetricTensor) (M_P_squared : ℝ) (vol : VolumeElement) : ℝ :=
  93  (M_P_squared / 2) * integrate_scalar (ricci_scalar g) g vol
  94
  95/-- For Minkowski (R=0), EH action vanishes. -/
  96theorem eh_action_minkowski (M_P_squared : ℝ) (vol : VolumeElement) :
  97  einstein_hilbert_action minkowski_tensor M_P_squared vol = 0 := by
  98  simp only [einstein_hilbert_action, integrate_scalar]
  99  rw [Finset.sum_eq_zero]
 100  · simp
 101  · intro i _
 102    simp [minkowski_ricci_scalar_zero]
 103
 104end Fields
 105end Relativity
 106end IndisputableMonolith

papers checked against this theorem

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