Mat4
plain-language theorem explainer
Type alias for real 4×4 matrices, the ambient space for polarization tensors and quadratic-form data in the 4D Regge TT analysis. Anyone working the distinct-hinge moment or continuum-face evaluations in this module cites it as the carrier type. The body is a one-line Mathlib abbreviation; there is nothing to prove.
Claim. Write $\mathrm{Mat}_4$ for the vector space of $4\times 4$ matrices with real entries, i.e. $\mathrm{Mat}_4 := M_{4\times 4}(\mathbb{R})$.
background
The module is the 4D counterpart of the 3D Regge TT algebraic closer. It banks the transported distinct-hinge $m^2$ as a quadratic form in the pair $(E,\mathrm{dir})$ on the transverse-traceless variety, with closed ray evaluations already available, while a universal adjugate-style tensor contraction remains open.
In that setting one needs a fixed carrier for bilinear and quadratic data on 4-component polarizations and direction vectors. Real $4\times 4$ matrices are the natural home for such forms (and for any later continuum-face or symbol-direction contractions). The abbreviation simply names that carrier once for the rest of the file.
Upstream continuum and hinge infrastructure (simplicial ledger continuum bridge, hinge-aware zero modes, glued-pent hinge witnesses) supplies the geometric meaning of the moments being packaged; this alias does not encode that geometry.
proof idea
No proof. One-line abbreviation equating the local name to Mathlib's Matrix (Fin 4) (Fin 4) ℝ. Noncomputable section follows only because later quadratic-form objects in the module are noncomputable.
why it matters
Local scaffolding for the banked 4D theorem list: homogeneity of the transported distinct-hinge moment under scaling of $E$, the symbol-direction plus/cross evaluations (normalized $-1/8$), and the $e_0$-direction plus/cross values. Those closed-form ray facts live as quadratic forms on this matrix space.
The module header marks the full closed-form equality to a universal bilinear tensor contraction as open (Regge4DDistinctHingeTensorClosedFormOpen), and the residual factor-4 mismatch versus Einstein-Hilbert as a separate geometric question. The alias itself does not close either gap and does not flip gap_action_recovery. It is the typed substrate on which those open identities would be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.