minkowskiTrace
plain-language theorem explainer
Defines the Minkowski metric trace of a covariant 4×4 matrix as η^{ij} H_{ij} in signature (−,+,+,+): −H_{00}+H_{11}+H_{22}+H_{33}. Anyone working the Lorentzian transverse-traceless layer cites it as the scalar that vanishes for traceless modes. The body is a direct four-term expansion of the raised-index contraction.
Claim. For a real $4\times 4$ matrix $H$, the Minkowski metric trace is $\operatorname{tr}_\eta(H) := \eta^{ij} H_{ij} = -H_{00} + H_{11} + H_{22} + H_{33}$, with signature $(-\!,+\!,+\!,+)$.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1): transverse-traceless splitting of symmetric real $4\times 4$ matrices against a Minkowski wave covector on $\mathrm{Fin},4$, including the null case. Conventions fix signature $(-!,+!,+!,+)$; covectors are lowered by default; index raising negates the time component.
Matrices are plain Mat4 objects (real $4\times 4$ arrays). The companion Minkowski pairing of covectors is $a\cdot b = -(a_0)(b_0)+\sum_{i=1}^3 a_i b_i$. The metric trace is the scalar contraction $\eta^{ij} H_{ij}$ written out componentwise, matching the module convention that Lorentz transversality contracts the second index of $H$ against the raised wave covector.
The two upstream H symbols in the dependency graph are the Recognition cost reparametrizations $H(x)=J(x)+1$ from the cost algebra; they are name collisions only and do not enter this definition.
proof idea
Pure definition: the right-hand side is the expanded contraction $\eta^{ij} H_{ij}$ under $\eta=\mathrm{diag}(-1,1,1,1)$. No lemmas are applied; later identities (minkowskiTrace_eq_sum, additivity, homogeneity) recover the sum form $\sum_{i,j}\eta_{ij} H_{ij}$ and the usual linear algebra rules by unfolding.
why it matters
This scalar is the gate for the Lorentz-traceless predicate: a matrix is Lorentz-traceless precisely when the metric trace vanishes. Downstream lemmas establish linearity (minkowskiTrace_add, minkowskiTrace_smul, minkowskiTrace_sub), the normalization $\operatorname{tr}\eta(\eta)=4$, and the identities $\operatorname{tr}\eta(m\otimes m)=m\cdot m$ and the symmetrized-outer analogue, which feed the gauge-part projectors for both non-null and null wave covectors.
In the Recognition gravity stack it is the Lorentzian counterpart of the Euclidean TT trace used in the edge TT decomposition ledger name. The module explicitly does not yet decompose Regge EDGE perturbations, prove $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, or flip gap-action recovery; this definition only supplies the algebraic trace those later steps will need when polarizations are imposed on the eight-tick / $D=3$ spacetime scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.