sum_fin_four
plain-language theorem explainer
For any additive commutative monoid and any map on four indices, the Finset sum over Fin 4 equals the explicit four-term sum. Gravity and Clausius–Einstein bridge lemmas cite it whenever a 4×4 quadratic contraction is expanded by hand. The proof decides that the universe equals {0,1,2,3}, rewrites, simplifies, and finishes by abelian cancellation.
Claim. Let $\alpha$ be an additive commutative monoid and let $f:\{0,1,2,3\}\to\alpha$. Then $\sum_{i=0}^{3} f(i)=f(0)+f(1)+f(2)+f(3)$.
background
The ambient module is the Phase 5 algebraic prerequisite on null-cone quadratic tensor classes: finite-dimensional real linear algebra showing that the values of a symmetric quadratic form on all Minkowski-null covectors determine the symmetric matrix modulo a scalar multiple of $\eta=\mathrm{diag}(-1,1,1,1)$. Honesty tags keep geometric curvature, continuum Ricci, and the Einstein field equation open.
Quadratic contraction is the double sum $\mathrm{quadContr}(A,k)=\sum_{i,j} A_{ij}k_i k_j$ over Fin 4. Expanding that sum (and the related symmetrization identities) repeatedly needs the universe of Fin 4 written as four concrete summands. The same expansion already appears as a private lemma in ClausiusEinsteinBridge; this copy serves the local null-cone package without re-importing heavier geometry.
proof idea
Tactic proof in four steps. First decide proves Finset.univ = ({0,1,2,3} : Finset (Fin 4)). Rewrite the sum along that equality, simp unfolds the finite-set sum into the four-term expression (up to monoid commutativity/associativity), and abel normalizes the additive monoid expression to the ordered sum $f,0+f,1+f,2+f,3$. No external mathematical lemmas beyond the Fin 4 decision procedure and abelian monoid normalization.
why it matters
Bookkeeping that unlocks every explicit 4D quadratic-form identity in the null-cone package. Downstream it is applied in quadContr_eq_quadContr_symmetrize4 ("quadratic contraction sees only the symmetric part"), in the bridge theorems quadContr_minkowskiEta4 and null_quadratic_zero_eq_scalar_eta (four-dimensional Lorentzian null-contraction rigidity: a symmetric matrix vanishing on every Minkowski-null vector is a scalar multiple of $\eta$), and in the twin expansion inside ClausiusEinsteinBridge. Those results are the algebraic half of the Phase 5 rigidity package; they do not construct an independent geometric $G$ from Recognition area/focusing ancestry, so Tier A and the EFE remain open as the module header states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.