Mat4
plain-language theorem explainer
Local type alias for the preflight 4-by-4 matrix type, so the 4D torus continuum-limit file can talk about matrices without colliding with a transported Bloch-orbit abbrev of the same short name. Readers of the mesh-cardinality and density-weight section meet this name first. The body is a one-line re-export with no proof content.
Claim. Write $\mathrm{Mat}_4$ for the same type as the preflight four-by-four matrix type used in the Regge 4D continuum analysis (local alias only, to avoid a name clash with a transported abbrev).
background
This module builds the action-to-symbol dictionary for a finite periodic Freudenthal sequence on the side-$N$ 4-torus ($N=j+3$), with $N^4$ sites and density weight $N^{-4}$, frozen against the wrong-power decoy $N^{-2}$. The 3D closed path cancels as $(2/N^3)\cdot(N^3/2)=1$; the 4D bookkeeping aims at the same pattern with $N^4$, so the canonical finite Hamiltonian matches the distinct-hinge Bloch fold once Schläfli elevation and the 4D cell-sum identity close.
The continuum preflight already fixes the matrix type used in that dictionary. This file only re-exports that type under a short local name, because a transported Bloch-orbit abbrev would otherwise occupy the same identifier.
proof idea
Definitional abbreviation: a one-line re-export of the preflight matrix type. No lemmas, tactics, or proof obligations.
why it matters
Namespace hygiene for the 4D torus continuum-limit dictionary. Mesh cardinality, density weight, second-difference bookkeeping, and the canonical finite Hamiltonian in this module all need a short matrix type name without clashing with the transported Bloch-orbit abbrev. The module status is explicit: product mesh and density identities and the algebraic factor $(2/N^4)\cdot(N^4/2)=1$ are theorem-shaped; continuum Tendsto binds to the Option-C midpoint trig-poly mesh; open named items are the 4D cosine cell-sum identity and residual star-member offsets on the legacy fold. This alias does not flip gap_action_recovery and carries no new physics beyond naming.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.