Mat4
plain-language theorem explainer
Type alias for real 4×4 matrices indexed by Fin 4. Every subsequent Lorentzian TT predicate and projector in this module is stated on this carrier. Citation is mechanical: any proof that manipulates symmetric covariant tensors, Minkowski traces, or null/non-null projectors imports it by name. The body is a one-line Mathlib Matrix abbreviation.
Claim. Write $\mathrm{Mat}_4$ for the type of real $4\times 4$ matrices with indices in $\{0,1,2,3\}$, i.e. maps $(\mathrm{Fin}\,4)\times(\mathrm{Fin}\,4)\to\mathbb{R}$.
background
This module is the Lorentzian algebraic layer of the QG campaign lane edge_tt_decomposition (Wave 4 / W4-1). It specializes the Euclidean TT layer of EdgeTTDecomposition4D to signature $(-+++)$ on Fin 4, including the physically relevant null wave-covector case.
Conventions fixed here: covectors are lowered by default; index raising negates the time component; the Minkowski pairing is $\eta(a,b)=-(a_0)(b_0)+\sum_{i=1}^3 a_i b_i$; the metric-trace of a covariant symmetric matrix is $\eta^{ij}H_{ij}=-(H_{00})+H_{11}+H_{22}+H_{33}$. Lorentz transversality contracts the second index of $H$ against the raised wave covector.
Mat4 is the common carrier for all of those objects: symmetric matrices, gauge pieces, outer-square projectors, and the TT residual.
proof idea
One-line abbreviation: Mat4 is definitionally Matrix (Fin 4) (Fin 4) ℝ from Mathlib. No proof obligations.
why it matters
Gives a single short name to the 4D real matrix type used by every Lorentzian TT predicate in the file (IsSymmetric, IsLorentzTraceless, IsLorentzTransverse, IsLorentzTT, gaugePart, projectors). Without it the signatures of the algebraic TT layer would repeat the full Mathlib matrix type. It sits strictly inside the linear-algebra tier: the module doc explicitly states that this layer does not decompose Regge EDGE perturbations, does not prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, and attaches no polarization normalization. Downstream gravity closing names that need a Lorentzian TT split will import this carrier first.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.