exactMidpointBlochFirstVariation_polarization
plain-language theorem explainer
The midpoint Bloch first variation equals half the difference of the exact midpoint Bloch symbols at H+K and H-K. Anyone transporting continuum TT first-variation limits via polarization cites this identity. The proof evaluates the quadratic line formula at t=±1 and subtracts.
Claim. For $4\times 4$ matrices $H,K$ and wavevector $k$, the directional first variation of the exact midpoint Bloch symbol satisfies $$\delta Q(H;K,k)=\frac{Q(H+K,k)-Q(H-K,k)}{2},$$ where $Q$ is the finite trig polynomial over the unit-cell coupling table.
background
This module works in the Euclidean weak-field transverse-traceless (TT) sector of the closed 4D midpoint Bloch continuum face. The exact midpoint Bloch symbol $Q(H,k)$ is a finite trigonometric polynomial: a sum over the unit-cell coupling table of coupling weights times cosines of coupling phases. Matrices are $4\times 4$ continuum Regge data; wavevectors live on the dual torus.
The directional first variation $\delta Q(H;K,k)$ is the genuine cross term obtained by differentiating the symbol along the affine line $H+tK$. Upstream, the line formula expands $Q(H+tK,k)$ as a quadratic polynomial in $t$: constant term $Q(H)$, linear term the first variation, and quadratic term $Q(K)$. Algebraic TT means symmetric, Euclidean-traceless, and transverse.
The module honesty clause restricts theorems to this Euclidean weak-field TT sector: not a source equation, not Ricci/null focusing, and not GAP1 closure.
proof idea
Apply the line expansion of the midpoint Bloch symbol at $t=1$ and $t=-1$.
At $t=1$: $Q(H+K)=Q(H)+\delta Q(H;K)+Q(K)$ (via exactMidpointBlochSymbol_line and one_smul).
At $t=-1$: rewrite $H+(-1)\cdot K=H-K$, then $Q(H-K)=Q(H)-\delta Q(H;K)+Q(K)$ because $(-1)^2=1$.
Subtract the two identities and divide by 2; linarith closes the arithmetic.
why it matters
Polarization is the algebraic bridge that turns two continuum limits of $Q$ into one continuum limit of the first variation. Downstream, continuumTTFirstVariation_closed uses it with the banked Tendsto of $S_{RS}$ to the Einstein-Hilbert face on $H+K$ and $H-K$, yielding the headline Euclidean TT result: the torus-normalized midpoint first variation tends to $-\frac14$ times the Frobenius pairing.
The same identity is packaged into the certificate srsTTFirstVariation4D_cert alongside the line derivative and the closed continuum statement. In the Recognition gravity stack this is local analysis on the Regge/Bloch side, not yet the sourced Freudenthal exact-$J$ metric refinement or Lorentzian null-dyad Ricci transport flagged as the missing future object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.