exactMidpointBlochSymbol_eq_irred
plain-language theorem explainer
The exact midpoint Bloch symbol on a 4D metric strain and wavevector equals the finite sum of coupling weights times cosines of coupling phases, written over the coupling universe Finset. Anyone expanding the symbol along a line in strain space cites this form. The proof is definitional: unfold the three component abbreviations and close by rfl.
Claim. For every $4\times 4$ strain matrix $H$ and every $4$-wavevector $k$, the exact midpoint Bloch symbol $Q(H,k)$ equals $\sum_{i\in U} w_H(i)\,\cos(\theta_k(i))$, where $U$ is the unit-cell coupling universe, $w_H$ the coupling weight function of $H$, and $\theta_k$ the coupling phase function of $k$.
background
The ambient module studies the Euclidean weak-field transverse-traceless (TT) first variation of the closed $4$D midpoint Bloch continuum face of the Recognition Science Regge action. The midpoint Bloch symbol is the finite trigonometric polynomial that encodes the exact flat Hessian of that face on a unit cell: a sum of coupling weights times cosines of coupling phases.
Upstream, exactMidpointBlochSymbol is defined as that sum indexed by the discrete coupling type. The present statement rewrites the same quantity with three named components: the coupling universe Finset, a weight function of the strain, and a phase function of the wavevector. The cost algebra $H(x)=J(x)+1$ appears only as ambient infrastructure; the identity itself is purely combinatorial on the coupling table.
Local honesty constraints (from the module doc) restrict all claims to the Euclidean weak-field TT sector of the closed midpoint face: not a source equation, not Ricci/null focusing, and not GAP1 closure.
proof idea
One-line definitional proof. Rewrite by the three component definitions (weight function, phase function, coupling universe), then close by reflexivity: the resulting sum is definitionally identical to the upstream midpoint Bloch symbol.
why it matters
This irreducible presentation is the entry point for the line expansion of the midpoint symbol. Downstream, the line theorem expands $Q(H+tK)=Q(H)+t,\mathrm{FV}(H,K)+t^2 Q(K)$ by rewriting through this equality and then differentiating the weight factors. That first-variation term is the genuine cross-term the module transports, via the banked continuum convergence on $H\pm K$ plus polarization, toward the Euclidean TT continuum face.
In the broader Recognition gravity chain the midpoint Bloch face sits under the closed $4$D continuum limit of the RS action; the module explicitly withholds source equations, null focusing, and GAP1. The missing future object remains a Recognition-derived Freudenthal exact-$J$ metric refinement that would identify the sourced response with this midpoint variation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.