axisDisp
plain-language theorem explainer
Unit coordinate displacement along a chosen axis of the 4-torus: the standard Kronecker vector e_a on Fin 4. Gravity analysts cite it when loading a metric matrix onto axis edges via the quadratic form Dᵀ H D. The body is the obvious indicator definition, not a derived claim.
Claim. For each axis index $a \in \{0,1,2,3\}$, the unit axis displacement is the map $D_a : \{0,1,2,3\} \to \mathbb{R}$ given by $D_a(i) = 1$ if $i = a$ and $D_a(i) = 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: an edge-class coefficient is $\sum_{ij} E_{ij} D^i D^j$ (as in polEdgeCoeff).
Axis edges are the four pure lattice steps $e_a$. Their displacement vectors are the standard basis of $\mathbb{R}^4$ indexed by Fin 4. Downstream, the edge load of a matrix $H$ on such a displacement collapses to the diagonal entry $H_{aa}$, and plane-wave midpoint phases multiply that load by a cosine of $m\cdot x + m_a/2$.
The definition is pure linear algebra scaffolding for those identities; it does not encode curvature, continuum limits, or the full Freudenthal edge-class stencil.
proof idea
Definition only: the function sending coordinate index $i$ to $1$ when $i$ equals the chosen axis $a$, and to $0$ otherwise. No lemmas, no tactics. The companion lemma axisDisp_apply is definitional equality (rfl).
why it matters
Axis displacements are the primitive inputs to edge loading in 4D. edgeLoad_axis uses them to prove edgeLoad H (axisDisp a) = H a a. The stencil layer identifies class displacements for pure axis classes with these vectors (classDisp_axis0), so class coefficients and plane-wave class perturbations reduce to axis-edge formulas (classCoeff_axis0, planeWaveClassPert_axis0).
Within the attachment file itself they feed gauge-versus-discrete-Lie identities on axis edges (exact finite-difference form, not continuum $\delta\ell^2 = 2\partial_a\xi_a$) and decoy TT checks. They are the 4D counterpart of the 3D displacement classes used in polEdgeCoeff.
Scope remains honest: this does not close edge_tt_decomposition, continuum Einstein-Hilbert recovery, or gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.