hasDerivAt_exactMidpointBlochSymbol_line
plain-language theorem explainer
Along the affine line of strain matrices H + t K, the closed 4D midpoint Bloch symbol is differentiable at t = 0, with derivative equal to the exact midpoint first-variation cross term. Gravity analysts cite this when packaging the Euclidean weak-field TT first-variation certificate. The proof rewrites the line restriction as an affine-quadratic polynomial and invokes the standard derivative-at-zero lemma for that shape.
Claim. For any $4\times 4$ strain matrices $H,K$ and any $4$-wavevector $k$, the map $t \mapsto S_{\mathrm{mid}}(H + t K, k)$ is differentiable at $t = 0$, and its derivative equals the exact midpoint first variation $\delta S_{\mathrm{mid}}(H,K;k)$.
background
This module works in the Euclidean weak-field transverse-traceless (TT) sector of the closed 4D midpoint Bloch continuum face. The midpoint Bloch symbol $S_{\mathrm{mid}}$ is the continuum face of the Recognition-derived midpoint strain action on a 4-torus mode; Mat4 and Wave4 are the ambient matrix and wavevector types from the Regge 4D continuum preflight layer.
The directional first variation $\delta S_{\mathrm{mid}}(H,K;k)$ is the genuine cross term obtained by polarizing the quadratic midpoint symbol in the two strain arguments. The module honesty block is binding: the result is only a TT Euclidean weak-field statement, not a sourced field equation, not Ricci/null focusing, and not GAP1 closure.
Upstream algebraic scaffolding includes the shifted cost $H(x)=J(x)+1$ (the d'Alembert form of the Recognition Composition Law) and the usual additive rewrites used when expanding the line restriction; those enter only as background identities, not as the derivative engine itself.
proof idea
First establish a pointwise identity: the line restriction equals the affine-quadratic
$S_{\mathrm{mid}}(H,k) + \delta S_{\mathrm{mid}}(H,K;k), t + S_{\mathrm{mid}}(K,k), t^2$
by funext and the already-proved expansion exactMidpointBlochSymbol_line, with commutative/associative additive rewrites.
Rewrite the target function by that identity, then apply hasDerivAt_affine_quad to the constant, linear, and quadratic coefficients. At $t=0$ the quadratic term drops from the derivative, leaving exactly $\delta S_{\mathrm{mid}}(H,K;k)$.
why it matters
This is the continuum-line differentiability leg of the TT first-variation package. Downstream, hasDerivAt_finiteExactMidpointBlochSymbol_normalized lifts the same idea to the normalized finite-mesh symbol (no continuum interchange), and srsTTFirstVariation4D_cert bundles this theorem with the polarization identity and the closed continuum TT first variation into the module certificate.
In the broader Recognition gravity program it supplies the directional derivative needed before transporting the torus-normalized continuum face via the banked $S_{\mathrm{RS}}\to\mathrm{EH}$ Tendsto on $H\pm K$ plus polarization. It does not close the sourced response: the missing future object remains a Recognition-derived Freudenthal exact-$J$ metric refinement identifying that response with this midpoint variation, followed by Lorentzian null-dyad Ricci/stress transport. Do not cite PixelAreaModel, LocalNullPatch, or the MODEL exact-$J$ mesh action as support.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.