exactMidpointBlochM2_gaugePart_eq_zero
plain-language theorem explainer
On pure-gauge edge data built from two 4-wavevectors, the exact midpoint Bloch m² coefficient vanishes when evaluated at the first wavevector. Lattice gravity and Regge-calculus workers cite this when checking that gauge modes contribute zero mass-squared in the 4D midpoint TT identity. The proof is a one-line alias of the already-proved gauge-vanishing theorem, kept for packing-route name compatibility.
Claim. For any two real 4-vectors $m,v\in\mathbb{R}^4$, if $H$ is the pure-gauge matrix $H_{ij}=m_i v_j+v_i m_j$, then the exact midpoint Bloch $m^2$ coefficient of $H$ at wavevector $m$ is zero: $\mathrm{exactMidpointBlochM}^2(H,m)=0$.
background
This module closes the exact midpoint $m^2$ TT identity in 4D Regge calculus (script lineage regge_4d_m2_tt_identity). The ambient objects are edge matrices Mat4 and wavevectors Wave4 (maps $\mathrm{Fin},4\to\mathbb{R}$).
The pure-gauge part of an edge mode is the symmetric rank-at-most-two matrix $(m,v)\mapsto(i,j)\mapsto m_i v_j+v_i m_j$. The exact midpoint Bloch $m^2$ is the cosine two-jet coefficient of the centered Bloch symbol: a weighted sum over coupling indices of $-(\mathrm{phase})^2/2$ times coupling weights of $H$.
Upstream, exactMidpointBlochM2_eq_zero_of_gaugePart already states the same identity and proves it by reducing the midpoint symbol on a symmetric matrix to a closed form, then showing that closed form vanishes on pure gauge pairs.
proof idea
One-line term wrapper: the statement is definitionally the same as exactMidpointBlochM2_eq_zero_of_gaugePart m v, so the proof is just that application. The real work lives upstream: rewrite via the closed-form expression of the midpoint $m^2$ on symmetric matrices (using symmetry of gaugePart), then invoke the algebraic identity that the closed form is zero on pure gauge pairs.
why it matters
In the 4D Regge exact-midpoint analysis, transverse-traceless (TT) mass-squared identities must be clean of pure-gauge contamination. This alias packages the gauge-vanishing fact under the packing-route name expected by the midpoint $m^2$ TT identity closure (exact_midpoint_m2_tt_identity).
It sits in the gravity analysis stack that certifies the Bloch symbol kernel and assembles numerical $m^2$ coefficients. No downstream Lean users are recorded yet; the declaration exists for name-stable citation along the packing route rather than as a new mathematical step. Framework-wise it is local lattice-gravity bookkeeping, not a T0–T8 forcing landmark, but it is required hygiene for claiming that only physical TT modes carry the midpoint mass-squared content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.