edgeLoad_axis
plain-language theorem explainer
On a unit axis edge of the 4-torus, the quadratic edge loading of a 4×4 matrix equals its corresponding diagonal entry. Gravity analysts cite this when transporting the Euclidean TT/gauge split onto plane-wave axis edges. The proof unfolds the double-sum definition and collapses the indicator sums.
Claim. For every real $4\times 4$ matrix $H$ and every axis index $a\in\{0,1,2,3\}$, if $D=e_a$ is the unit axis displacement ($D_i=1$ iff $i=a$), then the quadratic edge loading $D^\top H D=\sum_{i,j} H_{ij} D_i D_j$ equals the diagonal entry $H_{aa}$.
background
This module is the plane-wave layer of the 4D Regge edge TT attachment (QG campaign Wave 4 / lane W4-1). It attaches the Euclidean $4\times 4$ TT / gauge / transverse-trace split to axis-edge loadings on the 4-torus, using the same quadratic-form convention as the 3D chain: $\mathrm{polEdgeCoeff},E,d=\sum_{ij} E_{ij} D^i D^j$.
Two local definitions set the stage. The unit axis displacement $\mathrm{axisDisp},a$ is the standard basis vector $e_a$ on $\mathrm{Fin},4$. The edge load of a matrix $H$ against a displacement $d$ is the quadratic form $\sum_{i,j} H_{ij},d_i,d_j$. The module doc states the target identity explicitly: axis-edge squared-length loading satisfies $\mathrm{edgeLoad},H,(\mathrm{axisDisp},a)=H_{aa}$.
The ambient goal is not continuum GR recovery; it is a kernel-checked finite-difference identity layer that later feeds linearity of the load under the TT decomposition and an exact lattice gauge-to-discrete-Lie comparison.
proof idea
Term-mode proof by definition chase. Unfold the edge-load double sum and the piecewise definition of the unit axis displacement. Every factor $d_i$ or $d_j$ is then an indicator $i=a$ or $j=a$, so the double sum reduces to the single diagonal term $H_{aa}$ via the standard Finset identity that sums an if-then-else over a singleton index. No external lemmas beyond Finset.sum_ite_eq' are required.
why it matters
This is item (1) of the module's honest scope: the 4D plane-wave edge map on axis edges. Downstream, decoy and witness theorems use it to evaluate concrete loads without expanding sums: decoyTT_edgeLoad_axis2 obtains load 1 on axis 2; witness_edgeLoad_tt_ne_zero and witness_tt_edge_ne_zero show the TT projection of the witness matrix has nonzero axis-edge load and nonzero plane-wave edge perturbation.
In the broader Recognition gravity stack this is the bridge from the algebraic EdgeTTDecomposition4D layer to plane-wave edge observables, matching the 3D polEdgeCoeff convention. It does not close the ledger name edge_tt_decomposition, nor S_RS_converges_EH_4d, nor gap_action_recovery; those remain open campaign targets. The result is pure linear algebra on $\mathbb{R}^{4\times 4}$, not a continuum Einstein-Hilbert statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.