gradient_squared_minkowski
plain-language theorem explainer
This result supplies the explicit Minkowski-signature form of the squared gradient for any scalar field on spacetime. Field theorists cite it when reducing the general kinetic term to the familiar wave operator in flat space. The proof is a one-line wrapper that unfolds the double-sum definition and invokes the Minkowski sum lemma.
Claim. Let ϕ be a scalar field on ℝ⁴ and x ∈ ℝ⁴. Then the squared gradient contracted with the Minkowski metric satisfies ∇²ϕ(x) = −(∂₀ϕ(x))² + (∂₁ϕ(x))² + (∂₂ϕ(x))² + (∂₃ϕ(x))², where ∂_μ denotes the directional derivative in the μ-direction.
background
A scalar field assigns a real value to each point in 4-dimensional spacetime via a map from Fin 4 → ℝ to ℝ. The gradient collects the four directional derivatives at a point. The squared gradient is defined as the double sum over inverse-metric components times the product of gradient components, using the general MetricTensor structure.
proof idea
The proof unfolds the definition of gradient_squared to expose the double Finset.sum over the inverse metric. It then applies the upstream lemma gradient_squared_minkowski_sum, which reduces the contraction for the Minkowski tensor to the explicit signature expression via finset_sum_fin_4.
why it matters
This supplies the concrete flat-space expression required for relativistic scalar dynamics and the wave equation. It depends on the general gradient_squared definition and the minkowski_tensor construction in the geometry module. The result anchors the translation of field Lagrangians into the geometric setting used by the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.