exactMidpointBlochFirstVariation_eq_irred
plain-language theorem explainer
Identifies the directional first variation of the exact midpoint Bloch symbol with its irreducible coupling-sum form: a finite sum of cross edge-strain weights times cosines of Bloch phases. Anyone expanding the closed 4D midpoint symbol along a TT line cites this. The proof is pure definitional unfolding of the cross-weight, phase, and coupling-universe abbreviations.
Claim. For $4\times 4$ matrices $H,K$ and wavevector $k$, the directional first variation of the exact midpoint Bloch symbol at $H$ in direction $K$ equals $\sum_{i\in U} w_\times(H,K;i)\,\cos(\theta(k;i))$, where $U$ is the finite coupling universe and $w_\times$, $\theta$ are the irreducible cross-weight and phase maps on couplings.
background
The module works in the Euclidean weak-field transverse-traceless (TT) sector of the closed 4D midpoint Bloch continuum face. Matrices are Mat4 and wavevectors Wave4 from the Regge 4D continuum preflight layer. The object being varied is the exact midpoint Bloch symbol $Q(H;k)$, a finite coupling sum of edge-strain weights times cosines of Bloch phases.
The directional first variation at $H$ in direction $K$ is defined as the sum over coupling indices of the cross edge-strain factor times $\cos$ of the coupling phase. That definition is written with index-typed summands. The present statement rewrites it in irreducible form: an explicit finite sum over a named coupling universe with named cross-weight and phase functions.
Upstream, the cost algebra $H(x)=J(x)+1$ and the bridge ratio $K=\varphi^{1/2}$ appear only as name collisions in the dependency graph; the parameters here are the two strain matrices, not those scalars.
proof idea
Term-mode, three-line definitional identity. Rewrite the irreducible cross-weight, phase, and coupling-universe abbreviations by their defining equations, then close by rfl against the index-sum definition of the first variation. No algebraic cancellation or analysis is involved.
why it matters
Feeds the line expansion exactMidpointBlochSymbol_line: $Q(H+tK)=Q(H)+t\cdot\mathrm{FV}(H,K)+t^2 Q(K)$. That expansion is the algebraic engine for transporting the torus-normalized continuum face via the banked $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ Tendsto on $H\pm K$ plus polarization.
In the Recognition gravity stack this sits strictly inside the Euclidean weak-field TT analysis of the closed midpoint Bloch symbol. Module honesty forbids reading it as a source equation, Ricci/null focusing, or GAP1 closure. The missing future object remains a Recognition-derived Freudenthal exact-$J$ metric refinement that would identify the sourced response with this midpoint variation, then Lorentzian null-dyad transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.