axisMidpointPhase
plain-language theorem explainer
Defines the midpoint phase of a 4D axis edge from covering-space point x along direction a under wave covector m: the scalar m·x + m_a/2. Lattice gravity and Regge-calculus analyses cite it whenever a plane-wave edge loading must be evaluated at the edge midpoint rather than a vertex. The body is the direct arithmetic expansion of that inner product.
Claim. For wave covector $m \in \mathbb{R}^4$, base point $x \in \mathbb{R}^4$, and axis index $a \in \{0,1,2,3\}$, the midpoint phase is $\sum_{i=0}^{3} m_i x_i + m_a/2$, i.e. $m \cdot (x + e_a/2)$.
background
This module sits in the QG full-theory campaign (Wave 4 / lane W4-1): it attaches 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, where edge coefficients are of the form $\sum_{ij} E_{ij} D^i D^j$.
An axis edge runs from covering-space coordinate $x$ to $x+e_a$. Plane-wave squared-length perturbations are written $\ell^2 = \ell^2_{\mathrm{flat}} + t, c_d, \cos(\mathrm{mid})$, so the phase must be evaluated at the geometric midpoint of the edge. The midpoint phase is exactly that argument: $m\cdot x + m_a/2$.
Downstream, the plane-wave axis-edge perturbation multiplies the edge load of a matrix $H$ by $\cos$ of this phase. The same phase appears in the exact finite-difference identity relating gauge-matrix edge loads to discrete Lie loadings of a vertex field $\xi_b(x)=v_b\sin(m\cdot x)$.
proof idea
Pure definition: expand $m\cdot(x+e_a/2)$ componentwise as the sum $\sum_i m_i x_i$ plus the half-step $m_a/2$. No lemmas or tactics.
why it matters
This is the shared phase kernel for the entire plane-wave edge layer. It is unfolded into planeWaveAxisEdgePert (load times cosine of the midpoint phase), into the exact trig identity discreteLieAxis_eq that expands discrete Lie loading as $2 v_a,(\mathrm{lattice,deriv}),\cos(\mathrm{midpoint,phase})$, and into the gauge-part specialization planeWaveAxisEdgePert_gaugePart. The stencil bridge planeWaveClassPert_axis0 equates class-level and axis-edge plane-wave perturbations by matching this phase to the class midpoint phase. The witness non-vanishing check for a TT-projected edge also evaluates it.
Within Recognition Science gravity analysis it is scaffolding for the edge TT decomposition story, not a continuum Einstein-Hilbert claim. Module scope explicitly withholds full 4D Regge action recovery, continuum EH limits, and the ledger names edge_tt_decomposition, S_RS_converges_EH_4d, and gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.