couplingPhase
plain-language theorem explainer
Phase of one unit-cell edge-pair coupling against a 4D Bloch wavevector: the real inner product of k with the coupling's doubled midpoint offset. Gravity analysts cite it when assembling the exact midpoint Bloch trig polynomial and when expanding discrete Hessian symbols. Defined directly as a four-term sum; no proof content.
Claim. For a unit-cell edge-pair coupling $c$ and wavevector $k\in\mathbb{R}^4$, the coupling phase is $\sum_{i=0}^{3} k_i\,\delta_i(c)$, where $\delta(c)\in\mathbb{R}^4$ is the doubled midpoint offset $2(\mathrm{mid}_e-\mathrm{mid}_{e'})$ of the pair.
background
This module names the Stage-1 unit-cell exact flat Hessian as a finite trigonometric polynomial over the 1208-entry couplingTable. Each table entry is a Coupling: integer numerator/denominator weight data plus integer edge vectors De, Dep and a doubled midpoint offset (the phase carrier).
Wave4 is simply a map Fin 4 → ℝ, i.e. a real 4-component Bloch wavevector on the 4D lattice. The phase that multiplies a coupling in the Bloch symbol is the linear form pairing that wavevector with the coupling's midpoint offset.
Upstream, Coupling is the unit-cell edge-pair record from ReggeExactFlatHessianBlochData4D. The continuum gate is a centered Tendsto of the trig polynomial to the cosine two-jet; algebraic normalization recovers the frozen -1/4 factor via the norm gate.
proof idea
Pure definition: expand as the finite sum $\sum_{i:\mathrm{Fin},4} k_i\cdot c.\delta_i$. No tactics, no lemmas. Homogeneity and vanishing at $k=0$ are proved downstream by unfolding this sum and applying Finset.mul_sum / zero_mul.
why it matters
Local building block of the named exact midpoint Bloch symbol. Indexed form couplingPhaseIdx evaluates it on couplingTable[i]; the full symbol is the weighted sum of $\cos$ (or two-jet) terms in these phases.
Feeds couplingPhase_smul and couplingPhase_zero (scale and null identities used in Tendsto bookkeeping), and term_expand in the midpoint $M_2$ TT identity, where $-(\mathrm{phase})^2/2$ is expanded into multi-index monomials in De/Dep.
Sits inside the gravity continuum-symbol program: mesh geometric Tendsto is the ledger gate for S_RS_converges_EH_4d / gap-action recovery, which remain open. Not itself a forcing-chain (T0–T8) step; it is discrete-geometry infrastructure for the 4D Regge Hessian analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.