symmetrize
plain-language theorem explainer
symmetrize defines the standard averaging operator for (0,2) tensors over 4D spacetime indices. Researchers formalizing tensor symmetries in relativistic settings or spin-statistics relations would cite this construction. The implementation is a direct functional definition that swaps the two covariant indices and scales their sum by one half.
Claim. For a rank-(0,2) tensor field on four-dimensional spacetime, the symmetrized version satisfies $T_{ (μν) } = ½ (T_{μν} + T_{νμ} )$.
background
The Tensor abbrev represents a (p,q)-tensor field on 4-dimensional spacetime, mapping a point in ℝ⁴ to linear maps on the index spaces. This module serves as scaffolding for relativity geometry and is explicitly excluded from the main certificate chain. Upstream definitions include the period T as natural numbers in Breath1024 and the triangular number function in SyncMinimization, providing foundational arithmetic for the broader framework.
proof idea
The definition directly encodes the symmetrization formula by averaging the tensor value with its version under swapped lower indices. The swap is implemented via a case distinction on the Fin 2 index: replacing 0 with 1 and 1 with 0. No external lemmas are invoked; it is a pure functional expression.
why it matters
This construction feeds into the spin_statistics_theorem, which equates exchange symmetry with rotation phases under the eight-tick octave. It supplies the symmetrization step required for bosons in the RS spin-statistics correspondence. The module remains a scaffold outside the forcing chain T0-T8 and the main certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.