Mat4
plain-language theorem explainer
Local type alias for the four-by-four matrix type already fixed in the Regge 4D continuum preflight layer. Analysts of the flat-seed Schläfli second-variation pipeline use it for short notation inside this module. The body is a one-line re-export abbrev with no extra structure.
Claim. Write $\mathrm{Mat}_4$ for the same type as the continuum-preflight $4\times 4$ matrix type used in the Regge 4D flat analysis.
background
This module studies the 4D Regge flat second variation and the status of Schläfli elevation of the nonlinear action. In 3D the analogous elevation is closed; in 4D only the flat-seed Freudenthal closed form, flat directional Schläfli kill, and seed-angle differentiability are theorems, while full off-flat pathwise Schläfli remains open.
The continuum preflight layer already fixes a concrete $4\times 4$ matrix type for Hessian and symbol work (axis TT faces, Bloch continuum symbols, density-dictionary checks). The present declaration simply imports that type under a short local name so later Schläfli-candidate and fold identities can refer to matrices without repeating the long qualified path.
No new linear-algebra axioms are introduced here; the alias sits at the head of the flat-seed Schläfli progress section.
proof idea
One-line abbrev: the name is definitionally equal to the preflight matrix type. No tactics, no lemmas, no rewriting beyond the alias.
why it matters
Purely notational scaffolding inside the 4D Regge flat second-variation file. It keeps signatures for flat Freudenthal Schläfli tables, directional kills, and candidate Hessian faces readable while the module records what is theorem versus open.
It does not advance the open elevation gap (nonlinear $S''(0)$ equal to the candidate Hessian) and does not touch continuum EH recovery or gap-action recovery. Downstream use is local to this analysis module; the supplied graph lists no external consumers. Framework landmarks T0–T8, RCL, and the phi ladder are not implicated by a matrix alias.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.