IsSymmetric
plain-language theorem explainer
A real 4×4 matrix is symmetric when every entry equals its transpose partner. TT-decomposition and edge-gravity lemmas cite this as the first conjunct of the transverse-traceless package on Fin 4. The body is the standard index-swap equality; no proof work.
Claim. A matrix $H \in M_4(\mathbb{R})$ is symmetric when $H_{ij} = H_{ji}$ for all indices $i,j \in \{0,1,2,3\}$.
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition: the linear-algebra transverse-traceless split of symmetric real 4×4 matrices against a nonzero Euclidean wave covector on Fin 4. It lifts the three 3D conjuncts (symmetry, Euclidean trace, Euclidean transversality) without a Frobenius pin; Minkowski specialization is deferred.
Mat4 is the abbreviation for Matrix (Fin 4) (Fin 4) ℝ. Symmetry here is ordinary matrix symmetry (equal to its transpose), matching the tensor convention $T_{\mu\nu}=T_{\nu\mu}$ used elsewhere in the relativity geometry layer and the Lorentzian twin of this file. It is not the reciprocal cost symmetry $F(x)=F(1/x)$ from the d'Alembert inevitability chain, despite the shared name.
proof idea
Definition only: the proposition is the universal statement that every pair of entries is unchanged under index swap. No tactics, lemmas, or obligations.
why it matters
Symmetry is the first of the three conjuncts that define the TT package on Fin 4 (with tracelessness and transversality). Downstream predicates such as IsTT and the gauge/load projectors in this module take it as a hypothesis, so every algebraic identity in the edge-TT decomposition rests on it.
The module explicitly does not yet decompose Regge EDGE perturbations, prove continuum EH recovery, or close gap_action_recovery; this definition is the kernel-checked base type for that later work. In the broader RS gravity lane it supplies the 4D lift of the 3D IsTTPolarization conventions used when counting two independent polarizations on an axis wave vector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.