Mat4
plain-language theorem explainer
Local type alias for the preflight 4×4 matrix carrier used throughout the Recognition-mesh exact-J bridge on the periodic Freudenthal 4-torus. Gravity analysts cite it whenever mesh Hessians, Bloch symbols, or continuum faces need a clash-free matrix type. The body is a pure abbreviation re-exporting the preflight definition; no proof obligations.
Claim. Write $\mathrm{Mat}_4$ for the preflight $4\times 4$ matrix type of the Regge 4D continuum analysis (local alias chosen to avoid name clash with a transported matrix abbrev in the same module).
background
This module sits in the QG full-theory campaign at the Recognition gate of 4D continuum closure. It builds a canonical Recognition mesh on the periodic Freudenthal 4-torus and attaches a value-level action whose amplitude Hessian is the geometric Option-C midpoint Bloch symbol on that torus family.
The preflight layer already fixes notation for matrix carriers, wave carriers, and continuum-limit faces used by Regge Hessian assembly, Bloch transport, and exact midpoint $m^2$ TT identities. A local alias is needed because a transported matrix abbrev would otherwise collide with the preflight name inside the same file.
Preferred limit shape in this setting is amplitude Hessian at fixed mesh, then $N\to\infty$. The module does not treat the exact-$J$ object as a nonlinear Regge action via Schläfli; that elevation remains open.
proof idea
One-line abbreviation: re-export Regge4DContinuumPreflight.Mat4 under the local name. No tactics, no lemmas, no obligations.
why it matters
Gives the mesh and Hessian constructions in this file a stable matrix type without import-name collisions, so later identities (exact-$J$ action on the mesh equal to the true-Regge quadratic Hessian; iterated continuum Tendsto to the scale-explicit Option-C Einstein-Hilbert face) can be stated cleanly.
It supports the Recognition gate of 4D continuum closure on the Freudenthal torus, upstream of amplitude-Hessian equality and the discrete-torus bridge composed with exact midpoint $m^2$ TT / gauge faces. It does not close gap-action recovery or inhabit the full $S_{\mathrm{RS}}\to\mathrm{EH}$ 4D convergence theorem; those remain outside this module's honesty boundary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.