Mat4
plain-language theorem explainer
A 4-by-4 real matrix type used throughout the exact flat Regge cross-term symbol analysis. Gravity analysts cite it when assembling plane-wave strain tensors, Hessians, and Bloch-transported deficit phases on the Freudenthal torus. It is a pure type abbreviation 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 studies the exact flat cross-term continuum symbol of the Regge action Hessian on the Freudenthal torus. At flat background, deficits vanish and Schläfli reduces the second variation to the cross term $S''=\sum_h(dA_h)(d\delta_h)$. Strains and wave modes are packaged as 4-by-4 real matrices so that hinge areas, deficit phases, and Bloch transports act by ordinary matrix arithmetic.
Sibling abbreviations in the same file introduce strains, four-component waves, cube offsets, and star-member transports. All of those objects are valued in, or act on, this matrix type. The surrounding imports supply Regge hinge kernels, edge stencils, and orbit-wise Bloch transport in 4D.
proof idea
Pure type abbreviation: Mat4 is definitionally Matrix (Fin 4) (Fin 4) ℝ. No lemmas or tactics.
why it matters
Gives a single short name for the ambient linear algebra of the exact flat Regge Hessian symbol. Downstream structural lemmas (homogeneity, zero-momentum member drop, phased deficit dots, fold assembly) all speak in this type, so the continuum-symbol bookkeeping stays uniform across t11 star-member offsets and t12/t13 edge-origin transports. It does not itself close any open continuum limit (FoldAlongM2Tendsto, ledger $S_{RS}$); it only standardizes the matrix carrier those arguments use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.