srsTTFirstVariation4D_cert
plain-language theorem explainer
Packages three proved facts about the 4D midpoint Bloch symbol into one certificate: the directional derivative along H+tK at t=0, the polarization identity relating that derivative to the (H+K)−(H−K) difference, and the continuum TT limit equal to −(1/4) times the Frobenius pairing. Gravity analysts cite it as the closed Euclidean weak-field TT first-variation package. The proof is a three-field term constructor.
Claim. The following three statements hold simultaneously: (i) for all $4\times 4$ matrices $H,K$ and wavevector $k$, the map $t\mapsto$ midpoint Bloch symbol of $H+tK$ at $k$ is differentiable at $t=0$ with derivative equal to the midpoint first variation; (ii) that first variation equals $\bigl(S(H+K,k)-S(H-K,k)\bigr)/2$; (iii) for every nonzero integer 4-mode $m$ and TT matrices $H,K$ relative to $m$, the torus-normalized continuum face of the first variation tends to $-\tfrac14$ times the Frobenius pairing of $H$ and $K$.
background
The module works in the Euclidean weak-field transverse-traceless (TT) sector of the closed 4D midpoint Bloch continuum face. Matrices live in Mat4; wavevectors in Wave4; integer lattice modes in IntMode4. The midpoint Bloch symbol is the exact finite-difference symbol whose continuum face is already known (via the banked S_RS_converges_EH_4d_closed Tendsto on $H+K$ and $H-K$) to recover the Einstein–Hilbert quadratic form.
The first-variation object is the directional derivative of that symbol along the affine line $H+tK$. Polarization rewrites it as a centered difference, which is the algebraic bridge that lets the two-sided continuum Tendsto produce a single cross-term limit. The Frobenius pairing is the natural inner product on $4\times 4$ matrices that appears as the continuum coefficient $-1/4$.
Upstream, hasDerivAt_exactMidpointBlochSymbol_line establishes the finite-line derivative at $t=0$; exactMidpointBlochFirstVariation_polarization is the polarization identity; continuumTTFirstVariation_closed is the headline continuum theorem: the torus-normalized midpoint first variation tends to $-\tfrac14$ Frobenius pairing under TT hypotheses.
proof idea
Pure term-mode certificate assembly. The goal type SRSTTFirstVariation4DCert is a three-way conjunction (line derivative, polarization identity, continuum TT theorem). The proof supplies the three already-proved inhabitants in order:
hasDerivAt_exactMidpointBlochSymbol_linefills the universalHasDerivAtclause;exactMidpointBlochFirstVariation_polarizationfills the polarization equality;continuumTTFirstVariation_closedfills the TT continuumTendstoclause.
No additional rewriting or tactics: the certificate is definitionally the product of those three theorems.
why it matters
This is the module's export seal for the TT directional first variation of the closed 4D midpoint Bloch symbol. It freezes the Euclidean weak-field cross-term package that any later Recognition-to-Einstein bridge must match: line derivative, polarization, and continuum limit $-\tfrac14\langle H,K\rangle_F$.
No downstream consumers are wired yet (used_by_count = 0). The module honesty block is binding: the result is not a source equation, not Ricci or null focusing, and not GAP1 closure. The exact missing future object is a Recognition-derived Freudenthal exact-$J$ metric refinement (or pullback) that identifies the sourced response with this midpoint variation, followed by Lorentzian null-dyad Ricci/stress transport. Until that bridge exists, the certificate stands as the closed continuum face against which any candidate sourced theory must be checked.
Within the broader RS gravity stack it sits downstream of the banked 4D EH continuum convergence and upstream of any future null-sector or sourced-field-equation work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.