planeWaveClassPert_axis0
plain-language theorem explainer
At Freudenthal class index 0, the 4D plane-wave squared-length load equals the pure axis-0 edge attachment load. Anyone matching the class stencil to the earlier TT axis-edge packaging cites this identification. The proof unfolds both sides, rewrites the displacement via classDisp_axis0, and collapses the midpoint dot product to m_0.
Claim. For every $4\times 4$ real matrix $H$ and vectors $m,x\in\mathbb{R}^4$, the plane-wave class perturbation at class index $0$ equals the axis-edge plane-wave perturbation on axis $0$: $c_0(H)\,\cos(m\cdot x+m\cdot D_0/2)$ matches the corresponding axis-$0$ edge load times its midpoint cosine, where $D_0$ is the axis-$0$ displacement.
background
Module ReggeEdgeStencil4D is the next kernel-checked step after the 4D TT axis-edge attachment: it packages the 15 nonzero Freudenthal edge classes of the 4-cube (nonzero vectors in ${0,1}^4$, indexed by bit masks). Per class $d$, the coefficient is $c_d(H)=D^\top H D$ (same convention as 3D polEdgeCoeff / 4D edge load), and the midpoint Bloch phase is $m\cdot(x+D/2)$.
The plane-wave class perturbation is then $c_d(H)\cos(m\cdot x+m\cdot D/2)$. On the attachment side, axis displacements and axis midpoint phases play the same role for the four pure coordinate edges. Upstream, classDisp_axis0 already identifies the class-$0$ displacement vector with the axis-$0$ displacement: the bit-mask for index $0$ is exactly the first standard basis direction.
Weights in the provisional finite quadratic are still OPEN (all-ones, not true 4D Regge Hessian weights). This lemma is only about matching the class-$0$ plane-wave load to the axis packaging.
proof idea
Tactic proof by definitional reduction. Unfold both plane-wave loads and their coefficient/phase ingredients (classCoeff, classMidpointPhase, axisMidpointPhase). Rewrite the class displacement with classDisp_axis0, so class $0$ and axis $0$ share the same $D$. The remaining midpoint correction is the dot product $\sum_i m_i,(\mathrm{axisDisp},0,i)$; unfolding axisDisp and simplifying the indicator sum yields $m_0$. Rewrite that identity and both sides agree.
why it matters
Closes the class-vs-axis dictionary at the first pure edge: class index $0$ is not an exotic diagonal class, it is literally the axis-$0$ edge already treated in ReggeEdgeTTAttachment4D. That makes the 15-class stencil a conservative extension of the axis packaging rather than a competing convention.
No downstream consumers are wired yet (used_by empty). In the QG campaign this is bookkeeping infrastructure for plane-wave / Bloch analysis of the provisional finite TT quadratic, not a continuum or Einstein-Hilbert limit. Module scope is explicit: it does not prove $S_{\mathrm{RS}}$ converges to EH in 4D, does not finish the ledger name edge_tt_decomposition, and does not flip gap_action_recovery. True 4D Regge class weights remain OPEN.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.