gradient_squared
The gradient_squared definition computes the metric contraction of the gradient of a scalar field at a spacetime point. Workers building scalar-field actions in curved spacetime cite it when forming the kinetic term of the Lagrangian. It is realized as an explicit double summation over the four indices that multiplies the inverse-metric component by the product of the two gradient values.
claimFor a scalar field $φ$ and metric tensor $g$, the squared gradient at spacetime point $x$ is $∑_{μ,ν} g^{μν}(x) (∂_μ φ(x)) (∂_ν φ(x))$, where $g^{μν}$ is supplied by the inverse-metric accessor.
background
A scalar field is a map from spacetime points (Fin 4 → ℝ) to ℝ. The metric tensor is a local bilinear form whose inverse is accessed through the placeholder inverse_metric function imported from the Hamiltonian module. The definition sits inside the four-dimensional spacetime setting declared at the top of the Scalar module.
proof idea
Direct definition that expands to a double Finset.sum over μ and ν. Each term multiplies the inverse_metric component (selected by the index-construction functions) by the product of the two gradient evaluations at x.
why it matters in Recognition Science
It supplies the local kinetic density that is integrated to obtain the kinetic_action in the Integration module and is specialized to the Minkowski case by gradient_squared_minkowski. The construction is consistent with the Recognition forcing chain that fixes D = 3 spatial dimensions while retaining the full 4D spacetime manifold for relativistic fields.
scope and limits
- Does not supply a concrete inverse metric; it only calls the placeholder accessor.
- Does not incorporate the volume element or integration measure.
- Does not enforce a metric signature or curvature conditions.
- Does not compute the gradient itself; it assumes the sibling gradient function is already available.
formal statement (Lean)
76noncomputable def gradient_squared (φ : ScalarField) (g : MetricTensor) (x : Fin 4 → ℝ) : ℝ :=
proof body
Definition body.
77 Finset.sum (Finset.univ : Finset (Fin 4)) (fun μ =>
78 Finset.sum (Finset.univ : Finset (Fin 4)) (fun ν =>
79 (inverse_metric g) x (fun i => if (i : ℕ) = 0 then μ else ν) (fun _ => 0) *
80 (gradient φ x μ) * (gradient φ x ν)))
81
82/-- Gradient squared for Minkowski metric. -/