potential_action

formal source

  45  (1/2) * integrate_scalar (gradient_squared φ g) g vol
  46
  47/-- Potential action integral: (1/2) ∫ √(-g) m² ψ² d⁴x. -/
  48noncomputable def potential_action
  49  (φ : ScalarField) (m_squared : ℝ) (g : MetricTensor) (vol : VolumeElement) : ℝ :=
  50  (m_squared / 2) * integrate_scalar (field_squared φ) g vol
  51
  52/-- Integration is linear (finite weighted sum).
  53    STATUS: PROVED — Linearity of finite sums. -/
  54theorem integrate_add (f₁ f₂ : (Fin 4 → ℝ) → ℝ) (g : MetricTensor) (vol : VolumeElement) :
  55    integrate_scalar (fun x => f₁ x + f₂ x) g vol =
  56      integrate_scalar f₁ g vol + integrate_scalar f₂ g vol := by
  57  unfold integrate_scalar
  58  simp [Finset.sum_add_distrib, mul_add]
  59
  60/-- Integration scaling property.
  61    STATUS: PROVED — Scaling of finite sums. -/
  62theorem integrate_smul (c : ℝ) (f : (Fin 4 → ℝ) → ℝ) (g : MetricTensor) (vol : VolumeElement) :
  63    integrate_scalar (fun x => c * f x) g vol =
  64      c * integrate_scalar f g vol := by
  65  unfold integrate_scalar
  66  -- LHS: Δx4 * Σᵢ (sqrt_g * (c * f)) = Δx4 * Σᵢ (c * sqrt_g * f)
  67  -- RHS: c * (Δx4 * Σᵢ sqrt_g * f)
  68  have h : ∀ i : ℕ, sqrt_minus_g g (fun _ => (i : ℝ) * vol.grid_spacing) *
  69      (c * f (fun _ => (i : ℝ) * vol.grid_spacing)) =
  70    c * (sqrt_minus_g g (fun _ => (i : ℝ) * vol.grid_spacing) *
  71      f (fun _ => (i : ℝ) * vol.grid_spacing)) := by intro i; ring
  72  simp_rw [h]
  73  rw [← Finset.mul_sum]
  74  ring
  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)