finset_sum_fin_4
plain-language theorem explainer
The lemma asserts that the sum of any function f over the four-element index set Fin 4 equals the explicit sum of its four values, for any additive commutative monoid. It is cited in Minkowski metric contractions and gradient calculations within four-dimensional spacetime. The proof decides the universe equals the explicit set and reduces the sum with simplification and abelian tactics.
Claim. Let $α$ be an additive commutative monoid and let $f : Fin 4 → α$. Then $∑_{μ ∈ Finset.univ} f(μ) = f(0) + f(1) + f(2) + f(3)$.
background
In the Relativity.Geometry.Metric module spacetime indices run over Fin 4, separating one time and three spatial directions as fixed by D = 3 in the forcing chain. The gradient definition from Scalar.Fields assembles directional derivatives ∂_μ ψ over these four indices. The lemma supplies the explicit four-term expansion required for contractions with the Minkowski tensor eta.
proof idea
The proof decides that Finset.univ equals the explicit Finset {0,1,2,3}, rewrites the sum, applies simp to expand the terms, and invokes abel to collect them into the four-component sum.
why it matters
This lemma is applied directly in gradient_squared_minkowski_sum to reduce the double index sum over the inverse Minkowski metric to the diagonal form -(grad 0)^2 + (grad 1)^2 + (grad 2)^2 + (grad 3)^2. It also supports minkowski_preserves_inner by allowing explicit evaluation of constant inner products along curves in flat space. The step closes the index summation needed for the flat-space limit of the Recognition framework geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.