Mat4
plain-language theorem explainer
Four-by-four real matrices are the ambient type for linearized metric perturbations on the sixteen-site Freudenthal patch. Gravity analysts cite the alias whenever a strain current or edge image is built from a flat-patch metric shift. The declaration is a one-line type abbreviation with no proof content.
Claim. Write $\mathrm{Mat}_4$ for the vector 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 finite linearized metric edge image on the Freudenthal patch: a frozen world-metric null from the Order-Sensitive Gravity plan. A matrix $F$ lies in the metric edge image when it equals the strain current of some $4\times 4$ real perturbation on the sixteen-site unit hypercube.
Binary site coordinates on that hypercube are read bit-wise from the vertex index $v\in{0,\ldots,15}$ along each of the four axes. The strain formula and those coordinates are reproduced locally so the module need not import the heavy Freudenthal cover analysis chain. The ambient type of every such perturbation is exactly the $4\times 4$ real matrices.
proof idea
Pure type abbreviation: $\mathrm{Mat}_4$ is defined to be $\mathrm{Matrix},(\mathrm{Fin},4),(\mathrm{Fin},4),\mathbb{R}$. No lemmas, tactics, or obligations.
why it matters
Every subsequent object in the module (patch displacement, edge strain, strain current, the metric edge image itself, and the axis TT-cross membership lemmas) is typed against this alias. It pins the linearized flat-patch setting of the gravity analysis: metric perturbations live in $\mathrm{Mat}_4$, and the edge image is the set of strain currents they induce. Downstream used-by edges are empty at present; the alias is infrastructure for the nontriviality, symmetry, and properness theorems stated in the module honesty block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.