planeWaveAxisEdgePert
plain-language theorem explainer
Squared-length plane-wave perturbation amplitude on a 4D axis edge from base point x in direction a, induced by a matrix H. Equals the quadratic edge load of H on the unit axis displacement, times cos of the midpoint phase m·x + m_a/2. Gravity analysts cite it when attaching the Euclidean TT/gauge/transverse-trace split to plane-wave edge loadings on the 4-torus. Defined as a one-line product of the quadratic load and that cosine.
Claim. For a $4\times 4$ matrix $H$, wave covector $m$, covering-space point $x\in\mathbb{R}^4$, and axis index $a$, the plane-wave squared-length perturbation on the axis edge from $x$ to $x+e_a$ is $$\Bigl(\sum_{i,j} H_{ij}\,D^i D^j\Bigr)\cos\bigl(m\cdot x + m_a/2\bigr),$$ where $D=e_a$ is the unit displacement in direction $a$ (hence the load equals $H_{aa}$). This is the $t$-linear coefficient in the family $\ell^2=\ell^2_{\mathrm{flat}}+t\,c_d\cos(\mathrm{mid})$.
background
This module is the plane-wave layer of the 4D Regge edge TT attachment (QG campaign Wave 4 / lane W4-1). It sits directly above the algebraic EdgeTTDecomposition4D layer and attaches the Euclidean $4\times 4$ TT / gauge / transverse-trace split to plane-wave loadings on axis edges of the 4-torus, using the same quadratic-form convention as the 3D chain ($D^\top H D$).
Three local ingredients enter the definition. The quadratic edge load of a matrix $H$ on a displacement $D$ is $\sum_{i,j} H_{ij} D^i D^j$. The unit axis displacement in direction $a$ is the standard basis vector $e_a$. The midpoint phase of the axis edge based at $x$ with covector $m$ is $m\cdot x + m_a/2$, matching the 3D midpoint convention.
On an axis edge the load collapses to the diagonal entry $H_{aa}$. The plane-wave perturbation is that scalar times the cosine of the midpoint phase.
proof idea
Pure definition: the product of the quadratic edge load of $H$ on the unit axis displacement $e_a$ with $\cos$ of the midpoint phase $m\cdot x + m_a/2$. No proof obligations; downstream lemmas unfold this abbreviation and rewrite via linearity of the load.
why it matters
This is the basic plane-wave edge map of the 4D attachment layer. Downstream, additivity and scalar-homogeneity of the perturbation follow immediately from the corresponding load identities. The TT decomposition transports: the perturbation of $H$ equals the sum of the perturbations of its TT, gauge, and residual transverse-trace parts (via linearity plus the algebraic edge-TT decomposition). On pure gauge matrices the load is $2 m_a v_a$, so the perturbation equals $2 m_a v_a \cos(\mathrm{mid})$; whenever $\sin(m_a/2)\neq 0$ this matches a discrete Lie loading of the plane-wave vertex field up to the exact lattice factor $m_a/(2\sin(m_a/2))$. The 4D edge-class stencil identifies the axis-0 class coefficient with this quantity. The module explicitly does not close full 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.