gradient_squared_minkowski_sum
plain-language theorem explainer
This lemma computes the contraction of a four-component gradient vector with the inverse Minkowski metric, producing the Lorentzian norm -(g^0)^2 + (g^1)^2 + (g^2)^2 + (g^3)^2. It is cited by the scalar-field gradient-squared theorem in the relativity fields module. The proof is a direct term reduction that expands the finite sum and substitutes the explicit diagonal components of the inverse metric.
Claim. For a vector $g = (g^0, g^1, g^2, g^3)$, the contraction with the inverse Minkowski metric satisfies $g_0 g^0 + g_1 g^1 + g_2 g^2 + g_3 g^3 = -(g^0)^2 + (g^1)^2 + (g^2)^2 + (g^3)^2$, where the metric is diagonal with signature $(-1, +1, +1, +1)$.
background
The Minkowski tensor is the flat metric tensor eta with components diag(-1,1,1,1). Its inverse is obtained via matrix inversion and remains diagonal with the same signs. The finset_sum_fin_4 lemma reduces any sum over the four-element index set Fin 4 to the explicit four-term sum. The inverse_minkowski_apply lemma supplies the component values: -1 on the time-time entry and +1 on the spatial diagonal entries, zero off-diagonal. The local setting is the geometry submodule of relativity, which supplies tensor and derivative operations for Minkowski spacetime.
proof idea
The proof is a term-mode reduction. It first rewrites the double sum via finset_sum_fin_4 to obtain four explicit terms, then substitutes the diagonal inverse-metric components using inverse_minkowski_apply, and finally applies simp followed by ring normalization to reach the signed sum of squares.
why it matters
The lemma supplies the explicit Minkowski contraction required by gradient_squared_minkowski in the scalar fields module, which in turn furnishes the kinetic term for scalar fields. It anchors the relativity geometry layer to the flat metric used throughout the Recognition framework, consistent with the eight-tick octave and D=3 spatial structure derived from the forcing chain. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.