Mat4
plain-language theorem explainer
Type alias for real 4×4 matrices on Fin 4 indices. Gravity analysts cite it as the ambient linear-algebra carrier for weak-field Regge symbols, TT polarizations, and Frobenius norms in the 4D continuum preflight. The body is a one-line Mathlib Matrix abbrev with no proof content.
Claim. Write $\mathrm{Mat}_4$ for the space of $4\times 4$ real matrices, i.e. maps $(\mathrm{Fin}\,4)\times(\mathrm{Fin}\,4)\to\mathbb{R}$.
background
The module freezes independent continuum targets for a 4D Regge-to-Einstein–Hilbert recovery campaign before any continuum limit is proved. It names a canonical periodic Freudenthal 4-torus mesh of side $N\ge 3$, Frobenius-normalized Euclidean TT polarizations, and an independently defined linearized EH quadratic using kappa_einstein.
In that setting one repeatedly manipulates 4×4 real arrays: edge stencils, Bloch symbols, exact flat cross-term folds, and Frobenius norms. Mathlib already supplies Matrix (Fin n) (Fin m) ℝ; this abbrev pins $n=m=4$ once so sibling definitions (Wave4, frobeniusNormSq, mode maps) share a single carrier type.
Nothing in the module claims continuum recovery. OPEN items include Tendsto-style EH target Props and an uninhabited S_RS_converges_EH_4d.
proof idea
Pure definitional abbrev: expand to Mathlib Matrix (Fin 4) (Fin 4) ℝ. No tactics, no lemmas, no proof obligations.
why it matters
Gives a single named carrier for all 4D matrix data in the Regge continuum preflight (TT projectors, Hessian blocks, Bloch symbols, Frobenius pin lemmas). Downstream siblings in the same module build waves, integer modes, momentum norms, and the canonical Freudenthal torus on top of it. In the broader RS gravity track this is scaffolding for the first binding increment of 4D continuum closure: freeze mesh, TT data, and EH quadratic independently so later algebraic closers can only observe equality, never fit a scale. It does not itself touch T0–T8, RCL, or the mass ladder; it is linear-algebra infrastructure for the QG full-theory campaign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.