continuumTTFirstVariation_closed
plain-language theorem explainer
In the Euclidean weak-field TT sector, the torus-normalized midpoint Bloch first variation of two TT strain matrices converges, as the lattice refines, to minus one-fourth their Frobenius pairing. Gravity analysts cite this as the continuum face of the directional cross-term. The proof polarizes the banked SRS→EH continuum limits on H+K and H−K and matches the discrete first-variation sequence.
Claim. For every nonzero integer 4-mode $m$ and every pair of $4\times 4$ matrices $H,K$ that are algebraically TT with respect to $m$ (symmetric, Euclidean-traceless, and transverse to $m$), the sequence $$\frac{\delta S_{\mathrm{mid}}(H,K;\,m_j)}{\|p_j(m)\|^2}$$ tends, as the torus side length $j\to\infty$, to $-\tfrac14\,\langle H,K\rangle_{\mathrm{Frob}}$, where $m_j$ is the real mode of $m$ on the side-$j$ torus.
background
This module treats the directional (cross-term) first variation of the closed 4D exact midpoint Bloch symbol in the Euclidean weak-field TT sector. Algebraic TT means a matrix is symmetric, Euclidean-traceless, and transverse to a fixed mode $m$ (the IsTT predicate from the edge TT decomposition). The Frobenius pairing is the natural inner product on these $4\times 4$ strain matrices; the first-variation functional is the polarized cross term of the midpoint Bloch symbol along two TT directions.
The continuum face of the quadratic (diagonal) symbol is already banked: S_RS_converges_EH_4d_closed supplies a Tendsto of the torus-normalized finite midpoint Bloch symbol to an explicit continuum EH face scale. The present result lifts that diagonal continuum limit to the off-diagonal first variation by polarization on $H+K$ and $H-K$.
Local honesty is binding: the theorem lives only in the Euclidean weak-field TT sector of the closed midpoint Bloch continuum face. It is not a sourced field equation and not Ricci or null-focusing transport.
proof idea
Fix nonzero mode $m$ and TT matrices $H,K$. Closure of TT under addition and subtraction gives TT for $H+K$ and $H-K$. Apply the banked continuum theorem S_RS_converges_EH_4d_closed to both sums, then subtract the two Tendstos and divide by 2 to obtain convergence of the polarized continuum faces.
A short sequence identity equates that polarized discrete quotient to the torus-normalized exact midpoint Bloch first variation: expand the first-variation polarization identity, cancel the nonzero momentum-norm denominator by field_simp, and finish with linarith. Rewrite the polarized Tendsto along this equality, then simplify the continuum face difference by the algebraic identity that the polarized continuum face equals $-\tfrac14$ times the Frobenius pairing.
why it matters
This is the headline continuum theorem of the TT first-variation module: it converts the banked SRS→EH continuum face into a genuine directional cross-term limit equal to $-\tfrac14$ Frobenius. Downstream it is packaged, with the line derivative and the discrete polarization identity, into srsTTFirstVariation4D_cert.
In the Recognition gravity stack this is the continuum TT face of the midpoint Bloch symbol, not yet a sourced Einstein or null-focusing equation. The module doc states the missing future object explicitly: a Recognition-derived Freudenthal exact-$J$ metric refinement identifying the sourced response with this midpoint variation, followed by Lorentzian null-dyad Ricci/stress transport. Until that bridge exists, the result must not be cited as GAP1 closure or as a source equation. It does sit on the continuum side of the closed 4D Regge/SRS analysis that feeds the weak-field gravity sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.