axisDisp_apply
plain-language theorem explainer
The unit axis displacement in direction a on Fin 4 evaluates componentwise to the Kronecker delta: 1 on the a-slot and 0 elsewhere. Anyone computing quadratic edge loadings H_{aa} on 4-torus axis edges cites this to unfold the displacement vector. The proof is pure definitional equality via rfl.
Claim. For all $a,i\in\{0,1,2,3\}$, the $i$-th component of the unit axis displacement in direction $a$ equals $1$ if $i=a$ and equals $0$ otherwise.
background
This module sits in the QG full-theory campaign (Wave 4 / lane W4-1): attach the Euclidean $4\times 4$ TT / gauge / transverse-trace split to plane-wave edge loadings on axis edges of the 4-torus. The quadratic-form convention matches the 3D chain, $D^\top H D=\sum_{ij} H_{ij} D^i D^j$.
The unit axis displacement in direction $a$ is the map $i\mapsto 1$ if $i=a$ else $0$. Edge load of a matrix $H$ against a displacement $D$ is that quadratic form; on an axis edge it collapses to the diagonal entry $H_{aa}$. Plane-wave squared-length perturbations then multiply the load by a midpoint cosine phase.
The present lemma is the pointwise evaluation of that displacement, the first elementary fact in the edge-load algebra section.
proof idea
One-line definitional proof: rfl unfolds the lambda body of the unit axis displacement and matches the stated if-then-else. No lemmas are applied.
why it matters
Without a clean evaluation rule for the axis displacement, every later identity that reduces edge load on axis edges to $H_{aa}$, or transports the TT/gauge/residual split through that load, would re-unfold the same if-expression by hand. The module's honest scope lists exactly that reduction as item (1) of what is proved: axis-edge squared-length loading equals $H_{aa}$, and the midpoint plane-wave perturbation is that load times $\cos(m\cdot x+m_a/2)$.
No downstream consumers are recorded yet in the graph; the lemma is local scaffolding for the elementary edge-load algebra (linearity, gauge finite-difference identity) that feeds the larger edge_tt_decomposition lane. It does not touch continuum Einstein-Hilbert recovery, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, or gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.