antisymmetrize
plain-language theorem explainer
The antisymmetrize definition supplies the standard antisymmetrization operator for (0,2) tensors over 4D spacetime, T_{[μν]} = ½(T_μν − T_νμ). Researchers working on the RS spin-statistics theorem cite this when constructing antisymmetric tensor fields for fermions. The implementation is a direct functional definition that swaps the two lower indices and subtracts.
Claim. For a (0,2) tensor field $T$ on 4D spacetime, the antisymmetrized version is $T_{ [μν] } = ½ (T_{μν} - T_{νμ} )$.
background
The Tensor abbrev defines a (p,q)-tensor as a map from a spacetime point (Fin 4 → ℝ) to maps on p contravariant and q covariant indices each valued in Fin 4. This module is explicitly marked scaffold and lies outside the certificate chain. The definition draws only on the local Tensor type and the standard real-number arithmetic; no upstream lemmas from the forcing chain or phi-ladder are invoked.
proof idea
One-line wrapper that directly encodes the textbook formula: it applies the input tensor T, subtracts the version with the two lower indices swapped via a conditional on Fin 2, and scales by 1/2.
why it matters
The definition is referenced by spin_statistics_theorem, which equates the exchange sign of a two-particle state to the rotation phase under 2π. It therefore supplies the geometric ingredient needed to realize the RS spin-statistics link (fermions antisymmetric under 4-tick exchange). As a scaffold object it remains outside the main T0-T8 chain but closes the tensorial language required for the relativity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.