classMidpointPhase
plain-language theorem explainer
Defines the midpoint Bloch phase of a Freudenthal edge class d at covering coordinate x as the real number m·(x + D/2), where D is the {0,1}^4 displacement of class d. Anyone building plane-wave Regge symbols or Bloch folds in 4D cites it as the phase argument of the cosine loading. The body is a direct two-sum definition: momentum dotted with base plus half the class displacement.
Claim. For wavevector $m\in\mathbb{R}^4$, base point $x\in\mathbb{R}^4$, and edge class $d\in\{1,\ldots,15\}$ with displacement $D_d\in\{0,1\}^4$, the midpoint Bloch phase is $$m\cdot x + \tfrac12 m\cdot D_d.$$
background
The module packages the 4D Regge edge stencil after the TT-attachment layer: fifteen nonzero Freudenthal displacement classes in ${0,1}^4$, indexed by bit masks on Fin 15. Each class $d$ has a displacement vector $D_d$ whose $i$-th entry is $1$ precisely when the corresponding bit of the mask is set (the sibling classDisp).
Plane-wave analysis of the provisional finite quadratic needs a phase evaluated at the midpoint of each edge class rather than at a vertex. That midpoint is $x + D_d/2$ in the covering lattice, so the Bloch phase is the ordinary Euclidean dot product $m\cdot(x+D_d/2)$.
Upstream, classDisp supplies the ${0,1}$ vector; the surrounding campaign uses the same midpoint convention as the 3D polEdgeCoeff / hinge packaging. Dimension labels $D=3$ appearing in the dependency graph are the forced spatial dimension of the broader RS chain and are not parameters of this four-coordinate stencil.
proof idea
Pure definition, no proof obligations. Expand $m\cdot(x+D_d/2)$ coordinatewise into two finite sums over Fin 4: the base term $\sum_i m_i x_i$ plus half the displacement term $\sum_i m_i (D_d)_i$. The second sum reads classDisp d i for the $i$-th component of $D_d$.
why it matters
This phase is the argument of the cosine in the plane-wave class perturbation planeWaveClassPert, which multiplies the squared-length coefficient $c_d(H)=D_d^\top H D_d$ by $\cos(m\cdot x+m\cdot D_d/2)$. Downstream Bloch and symbol modules rely on it: scaling identities (classMidpointPhase_scaleDir, classMidpointPhase_symbolDir), exact quarter-turn evaluation at the star wavevector (classMidpointPhase_waveStar), zero-momentum collapse of phased class dots, and reindexing lemmas for slot-deficit kernels.
In the QG campaign it is the 4D lift of the 3D midpoint loading used for hinge-aware TT symbols. It does not touch the OPEN problem of true 4D Regge class weights, nor does it claim Einstein-Hilbert recovery or full edge-TT decomposition. It is scaffolding infrastructure for the provisional all-ones quadratic and the exact (non-fake) gauge-entry identities recorded in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.