def
definition
sample_grid
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Relativity.Fields.Integration on GitHub at line 24.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
21 grid_spacing_pos : 0 < grid_spacing
22
23/-- Sample points for discrete integration (uniform grid). -/
24def sample_grid (vol : VolumeElement) (n_points : ℕ) : List (Fin 4 → ℝ) :=
25 -- Simplified: n_points^4 grid over [0, L]^4
26 -- Full version would use adaptive quadrature
27 [] -- Placeholder
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) :