planeWaveClassPert
plain-language theorem explainer
Plane-wave squared-length perturbation on Freudenthal edge class d: the class load c_d(H)=D^T H D times the midpoint Bloch factor cos(m·x + m·D/2). Bloch-fold and orbit-symbol lemmas cite it as the per-class plane-wave ingredient. The body is the one-line product of the class coefficient and the midpoint cosine.
Claim. For a $4\times 4$ matrix $H$, Bloch wavevector $m$, base point $x\in\mathbb{R}^4$, and edge class $d\in\{0,\ldots,14\}$, the plane-wave class perturbation is $c_d(H)\cdot\cos(m\cdot x+m\cdot D_d/2)$, where $c_d(H)=D_d^\top H D_d$ and $D_d$ is the nonzero $\{0,1\}^4$ displacement of class $d$.
background
The module packages the 4D Regge edge stencil after the TT-attachment layer: fifteen Freudenthal-style edge classes, namely the nonzero displacement vectors in ${0,1}^4$, indexed by bit masks. Each class carries a squared-length coefficient and a Bloch phase at the edge midpoint.
The class coefficient is $c_d(H)=D^\top H D$ (same convention as the 3D polarized edge coefficient and the 4D edge load). The midpoint phase is $m\cdot x+m\cdot D/2$, i.e. the covering-coordinate phase plus half the class displacement phase. Their product is the plane-wave squared-length perturbation used throughout the Bloch analysis.
Local scope is deliberately provisional: class weights in the finite quadratic aggregate are all-ones, not the true 4D Regge Hessian weights at flat. Gauge invariance of that aggregate fails exactly; only the pure-gauge load identity is recorded.
proof idea
Definition, not a theorem. Body is the product of the class coefficient with the cosine of the midpoint Bloch phase. No lemmas are applied; both factors are sibling defs in the same module.
why it matters
This is the per-class plane-wave load that the 4D Bloch fold sums against class weights. The weighted sum phasedClassDot is literally $\sum_d v_d$ times this perturbation, and almost every identity in the fold and orbit-symbol layers unfolds through it: zero evaluations on axis TT for area-mask pairs, transported-deficit reindexing, master area evaluation at waveStar, and the scaled-direction phase form.
In the QG campaign it is the 4D analogue of the 3D polarized edge coefficient times a hinge phase. It does not close the open weight problem, nor the EH-convergence or gap-action ledgers; it only supplies the plane-wave packaging those later steps need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.