Mat4
plain-language theorem explainer
Notation for real 4-by-4 matrices indexed by Fin 4, the ambient space for the algebraic transverse-traceless layer of the edge TT decomposition campaign. Anyone working the 4D gravity analysis (symmetry, Euclidean trace, transversality to a wave covector) cites this type. It is a one-line Mathlib Matrix abbreviation with no proof content.
Claim. Write $\mathrm{Mat}_4$ for the type of real $4\times 4$ matrices, i.e. maps $(\mathrm{Fin}\,4)\times(\mathrm{Fin}\,4)\to\mathbb{R}$.
background
This module is the algebraic layer of the QG full-theory campaign item edge_tt_decomposition (Wave 4 / lane W4-1). It lifts the 3D TT polarization conventions (Euclidean trace, Euclidean transversality, symmetry) to Fin 4, without a Frobenius pin and without Minkowski specialization.
The ambient object is a real matrix on a 4-dimensional index set. Downstream predicates in the same file (symmetry, tracelessness, transversality to a nonzero Euclidean wave covector, and the composite TT condition) are all stated on this type. The module explicitly does not decompose Regge edge perturbations or close continuum gravity recovery theorems.
proof idea
One-line abbreviation: identify the name with Mathlib's Matrix type at index type Fin 4 over the reals. No lemmas, no tactics.
why it matters
Gives a short ambient type for every subsequent predicate and projector in the 4D edge TT algebraic kernel (symmetry, Euclidean trace, transversality, TT, gauge part, transverse projector). That kernel is the smallest kernel-checked increment toward the ledger name edge_tt_decomposition. It does not itself flip gap_action_recovery or prove S_RS_converges_EH_4d; those remain separate campaign targets. In the broader Recognition gravity stack this is pure linear-algebra scaffolding under the Euclidean conventions inherited from the 3D IsTTPolarization chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.