exactMidpointBlochFirstVariation
plain-language theorem explainer
Directional first variation of the exact midpoint Bloch symbol at a 4D matrix H in direction K, given as a finite sum over unit-cell couplings of cross edge-strain weights times cosines of coupling phases. Cited by the continuum TT first-variation limit, the polarization identity, and the finite-line derivative theorems in the Euclidean weak-field TT sector. The body is the defining coupling sum, not a derived proof.
Claim. For $4\times 4$ matrices $H,K$ and wavevector $k\in\mathbb{R}^4$, the directional first variation of the exact midpoint Bloch symbol at $H$ in direction $K$ is $\sum_i w^\times_i(H,K)\,\cos(\theta_i(k))$, where the sum runs over the finite unit-cell coupling index set, $w^\times_i$ are the cross edge-strain weight factors of the pair $(H,K)$, and $\theta_i(k)$ are the coupling phases at $k$.
background
The module works in the Euclidean weak-field transverse-traceless (TT) sector of the closed 4D midpoint Bloch continuum face. The exact midpoint Bloch symbol is a finite trigonometric polynomial over a fixed unit-cell coupling table: each coupling contributes a weight times $\cos$ of a phase linear in the wavevector.
Here $H$ and $K$ are $4\times 4$ matrices (edge-strain data in the Regge continuum preflight), and $k$ is a 4D wavevector. The cross weights $w^\times_i(H,K)$ are the bilinear cross edge-strain factors for coupling $i$; the phases $\theta_i(k)$ come from the same coupling table used by the symbol itself.
The module honesty clause restricts all theorems here to that Euclidean weak-field TT sector: not a source equation, not Ricci/null focusing, and not GAP1 closure. Upstream cost objects $H$ (shifted $J$-cost) and bridge ratio $K=\varphi^{1/2}$ appear in the dependency graph but are not free parameters of this definition.
proof idea
Definition, not a theorem. The body is the finite sum over CouplingIdx of couplingWeightCrossIdx H K i times Real.cos (couplingPhaseIdx k i). No tactics, no lemmas applied: the declaration is the closed-form cross-term that later polarization and line-expansion theorems identify with the directional derivative of the midpoint symbol.
why it matters
This is the concrete cross-term object the rest of the module differentiates and continuum-limits. Downstream, exactMidpointBlochFirstVariation_polarization equates it to half the difference of the midpoint symbol on $H+K$ and $H-K$; exactMidpointBlochSymbol_line expands $Q(H+tK)=Q(H)+t,\mathrm{FV}(H,K)+t^2 Q(K)$; and hasDerivAt_exactMidpointBlochSymbol_line records the directional derivative at $t=0$.
The headline continuum theorem continuumTTFirstVariation_closed then shows the torus-normalized midpoint first variation tends to $-\tfrac14$ times the Frobenius pairing in the TT sector, via the banked S_RS_converges_EH_4d_closed Tendsto on $H\pm K$ plus polarization. The certificate SRSTTFirstVariation4DCert packages that chain.
Framework role: a gravity-analysis step toward matching Recognition-derived continuum response to Einstein-Hilbert structure in the weak-field TT face. Explicitly not GAP1 closure; the missing future object is a Recognition-derived Freudenthal exact-$J$ metric refinement identifying 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.