Mat4
plain-language theorem explainer
Local alias for the 4×4 real matrix type used in the 4D Regge continuum preflight. Gravity analysts cite it when stating mesh-symbol limits, Einstein–Hilbert faces, and transverse-traceless polarizations in this scope module. The body is a one-line re-export with no proof content.
Claim. Write $\mathrm{Mat}_4$ for the $4\times 4$ matrix type already fixed in the Regge 4D continuum preflight layer (the carrier for polarization tensors $E$ and related continuum faces in this module).
background
This module sits outside the ledger export SRSConvergesEH4D and restates, as theorems, what Arc 2 step 8 actually proves about four-dimensional continuum limits of the Recognition Science mesh symbol. The reading is that the dictionary (algebraic midpoint Bloch) mesh sequence, normalized by mesh momentum, converges to the Regge transverse-traceless second-variation face, equal to $\rho$ times the Einstein–Hilbert face with $\rho=1/2$, not to the bare EH face.
Throughout that analysis one needs a fixed carrier for $4\times 4$ tensors: polarization data $E$, Frobenius norms $|E|_F$, and the explicit continuum faces built from them. The preflight layer already names that carrier; this abbrev only brings it into the scope module under a short local name, parallel to the companion wave-type alias in the same file.
proof idea
Definitional abbrev only: a one-line transparent alias of the preflight Mat4 type. No tactics, no lemmas, no computational content.
why it matters
Keeps the scope theorems (srs_limit_is_regge_normalization_times_eh, mesh non-convergence to the EH face, conditional R1 failure, and the step-8 scoped verdict) readable without repeatedly qualifying the preflight namespace. It does not advance the forcing chain (T0–T8) or the Recognition Composition Law; it is bookkeeping so the gravity analysis can state cleanly that the dictionary limit is the Regge face $-(1/8)|E|_F^2$ and is provably distinct from the EH face on any polarization of nonzero Frobenius mass. The open hinge remains geometric fold vs dictionary (uninhabited R1), which this alias does not touch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.