closedForm_gaugePart_eq_zero
plain-language theorem explainer
On a pure gauge edge pair H = m⊗v + v⊗m, the closed-form midpoint Bloch m² expression evaluates identically to zero when the wave covector is m. Anyone proving gauge-invariance of the exact midpoint TT identity cites this. The proof unfolds the closed form and the gauge embedding, expands the four-index sums, and finishes by ring.
Claim. For any real 4-covectors $m,v\in\mathbb{R}^4$, if $H_{ij}=m_i v_j+v_i m_j$ is the pure gauge matrix built from $m$ and $v$, then the closed-form midpoint Bloch expression $\mathrm{CF}(H,m)$ is identically zero.
background
This module closes the exact midpoint Bloch $m^2$ TT identity in 4D Regge calculus (script lineage regge_4d_m2_tt_identity). The closed form packages the continuum quadratic form that the discrete midpoint Bloch mass-squared is proved equal to on symmetric edge data:
$$\mathrm{CF}(H,k)=(-1/8)|H|_F^2|k|^2+(1/4)\mathrm{load}(H,k)+(1/8)(\mathrm{tr},H)\bigl((\mathrm{tr},H)|k|^2-2,q(H,k)\bigr).$$
A pure gauge pair is the symmetric rank-at-most-two matrix $H_{ij}=m_i v_j+v_i m_j$ (the Euclidean edge TT decomposition's gauge part). Wave covectors are just maps $\mathrm{Fin},4\to\mathbb{R}$. Frobenius and Euclidean squared norms are the usual double and single sums of squares. The identity says this continuum expression vanishes when $H$ is pure gauge and the probe wave is the first gauge leg $m$.
proof idea
Term-mode algebraic identity, no external lemmas. Unfold closedForm together with Frobenius norm, wave norm, load norm, the quadratic form, Euclidean trace, and the gauge-part embedding. Expand every Fin 4 sum with Fin.sum_univ_four, then discharge the resulting polynomial identity by ring. The cancellation is purely combinatorial in the four coordinates.
why it matters
Feeds the parent theorem exactMidpointBlochM2_eq_zero_of_gaugePart, which rewrites the exact midpoint Bloch $m^2$ through the closed-form equality on symmetric data and then applies this vanishing. That parent is the gauge half of the exact midpoint $m^2$ TT identity the module is written to close: continuum TT polarizations should see a nonzero mass-squared coefficient while pure gauge pairs must contribute zero. In the broader Regge-to-continuum preflight, this is the algebraic certificate that the midpoint Bloch kernel is gauge-clean before any continuum TT pin or Frobenius normalization is imposed. It does not itself touch the Recognition forcing chain (T0–T8) or the mass ladder; it is local gravity analysis supporting the discrete-to-continuum match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.