pith. machine review for the scientific record. sign in
def definition def or abbrev high

symmetrize

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  25noncomputable def symmetrize (T : Tensor 0 2) : Tensor 0 2 :=

proof body

Definition body.

  26  fun x up low => (1/2 : ℝ) * (T x up low + T x up (fun i => if (i : ℕ) = 0 then low 1 else low 0))
  27
  28/-- Antisymmetrisation: T_[μν] = 1/2 (T_μν - T_νμ). -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.