sqrt_minus_g

formal source

  28
  29/-- Square root of minus the metric determinant.
  30    STATUS: SCAFFOLD — Uses constant 1 as placeholder. -/
  31noncomputable def sqrt_minus_g (_g : MetricTensor) (_x : Fin 4 → ℝ) : ℝ := 1
  32
  33/-- Integrate a scalar function over spacetime volume (discrete approximation). -/
  34noncomputable def integrate_scalar
  35  (f : (Fin 4 → ℝ) → ℝ) (g : MetricTensor) (vol : VolumeElement) : ℝ :=
  36  let n := 10
  37  let Δx4 := vol.grid_spacing ^ 4
  38  Δx4 * Finset.sum (Finset.range n) (fun i =>
  39    sqrt_minus_g g (fun _ => (i : ℝ) * vol.grid_spacing) *
  40    f (fun _ => (i : ℝ) * vol.grid_spacing))
  41
  42/-- Kinetic action integral: (1/2) ∫ √(-g) g^{μν} (∂_μ ψ)(∂_ν ψ) d⁴x. -/
  43noncomputable def kinetic_action
  44  (φ : ScalarField) (g : MetricTensor) (vol : VolumeElement) : ℝ :=
  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. -/