load_one
plain-language theorem explainer
The identity 4×4 matrix acts as the identity under the load map: applying load of I to any covector m recovers m componentwise. Gravity analysts working the 4D transverse-traceless algebraic layer cite this when simplifying projector identities. The proof is a short sum-singleton argument after unfolding the matrix-vector product.
Claim. For every covector $m:\mathrm{Fin}\,4\to\mathbb{R}$ and every index $i$, the load of the $4\times 4$ identity matrix against $m$ satisfies $(\mathrm{load}\,I\,m)_i=m_i$. Equivalently, $I m=m$ under the Euclidean matrix-vector product on $\mathbb{R}^4$.
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition: linear-algebra TT structure for symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. It lifts the 3D conventions (Euclidean trace, Euclidean transversality, symmetry) without a Frobenius pin; Minkowski specialization is deferred.
Mat4 is the type of real $4\times 4$ matrices. The load map is the ordinary matrix-vector product: $(\mathrm{load},H,m)i=\sum_j H{ij}m_j$. The identity matrix $I$ has $I_{ij}=\delta_{ij}$, so the claim is the elementary identity $Im=m$.
Sibling structure in the file includes the transverse projector, outer-square, gauge part, and the TT predicates used later in the decomposition.
proof idea
Term-mode proof by unfolding load, then simplifying the identity matrix entries via one_apply. The resulting finite sum $\sum_j \delta_{ij}m_j$ is reduced with Finset.sum_eq_single at index $i$: the diagonal term is $m_i$, off-diagonal terms vanish by $i\neq j$, and the missing-membership branch is impossible because $i$ is in the universe of $\mathrm{Fin},4$.
why it matters
Feeds directly into load_transverseProjector, which shows that the transverse projector annihilates its defining covector $m$ (when $m\cdot m\neq 0$). That identity is a building block of the 4D algebraic TT decomposition: projectors must kill the longitudinal direction so residual modes are transverse.
In the Recognition Science gravity lane this sits inside Wave 4 / W4-1, the smallest kernel-checked increment toward edge TT structure. It does not yet touch continuum Einstein-Hilbert recovery or gap-action closure; it only supplies the linear-algebra identity those later steps need when simplifying load of $I-\hat{m}\otimes\hat{m}$.
No forcing-chain landmark (T5-T8) is at stake here; the result is pure Euclidean matrix algebra on $\mathrm{Fin},4$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.