IsSymmetric
plain-language theorem explainer
The definition IsSymmetric specifies that a rank-(0,2) tensor T on 4D spacetime obeys T(x, μ, ν) = T(x, ν, μ) for every point x and index pair. Workers on tensor structures inside the Recognition framework cite it when imposing symmetry on bilinear forms or metrics. The definition is realized directly by equating each tensor evaluation to the version with its two lower indices transposed.
Claim. A tensor $T$ of type $(0,2)$ on 4D spacetime is symmetric when $T(x, u, l) = T(x, u, l')$ holds for all $x$, upper indices $u$, and lower indices $l$, where $l'$ is the transposition of the two components of $l$.
background
The Relativity.Geometry.Tensor module is explicitly marked as a scaffold outside the certificate chain. Its central abbrev Tensor (p q : ℕ) maps a spacetime point (Fin 4 → ℝ) together with p upper and q lower index tuples (each Fin 4) to a real value; the present declaration specialises to p=0, q=2. The supplied doc-comment states the intended meaning: symmetry condition T_μν = T_νμ. Upstream references include the generic Tensor abbrev itself and the unrelated function-level IsSymmetric from DAlembert.Inevitability that encodes F(x) = F(1/x).
proof idea
Direct definition. The body asserts the required equality for every x, upper tuple, and lower tuple by replacing the lower tuple with the index-swapped version (Fin-2 component 0 receives the original component 1 and vice versa).
why it matters
The declaration supplies the tensor-level symmetry predicate used by downstream results such as bilinear_family_forced and symmetry_and_normalization_constrain_P in DAlembert.Inevitability, which force unique bilinear families once symmetry of the combiner P is assumed. It supplies the geometric counterpart to the function symmetry already present in the same inevitability theorems. Because the module is scaffold, the definition sits outside the T0–T8 forcing chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.