linEinstein_tt
plain-language theorem explainer
For a transverse-traceless real cosine plane wave with amplitude matrix H and wavevector k, every component of the linearized Einstein tensor equals (1/2) times the squared momentum of k, times H_μν, times cos(k·x). Anyone matching continuum EH second variation to the Regge TT dictionary cites this. The proof unfolds the linearized Einstein definition, substitutes the TT Ricci and scalar formulas, and finishes by ring.
Claim. Let $H$ be a $4\times 4$ real matrix and $k\in\mathbb{R}^4$ a wavevector such that $H$ is transverse-traceless relative to $k$. Write $h_{\mu\nu}(x)=H_{\mu\nu}\cos(k\cdot x)$. Then at every point $x$ and every pair of indices $\mu,\nu\in\{0,1,2,3\}$, the linearized Einstein tensor of $h$ satisfies $G^{(1)}_{\mu\nu}(x)=\tfrac12\,|k|^2\,H_{\mu\nu}\,\cos(k\cdot x)$.
background
This module (Arc 2, step 7) derives, from the Levi-Civita connection alone, the continuum Einstein-Hilbert second variation on a real transverse-traceless plane wave in 4D, in the same convention as the banked Regge midpoint dictionary. It imports only Mathlib and a linear-algebra edge-TT decomposition, so the continuum coefficient is obtained independently of the discrete coupling table and norm gate.
Coordinates are points $x:\mathrm{Fin},4\to\mathbb{R}$. The perturbation is the real cosine wave $h(x)=H\cos(k\cdot x)$ (not a complex exponential), matching the discrete symbol's unit-cell average under real-cos perturbations. Transverse-traceless means the usual continuum TT conditions on $H$ relative to $k$. The linearized Einstein tensor is built from the linearized Ricci tensor and scalar via the standard combination $G^{(1)}=R^{(1)}-\tfrac12 R^{(1)}\eta$ about flat space; those Ricci ingredients are already specialized to TT waves in sibling lemmas.
Named classical input A1 is the linearized Christoffel symbol $\Gamma^{(1)}{\lambda\mu\nu}=\tfrac12(\partial\mu h_{\lambda\nu}+\partial_\nu h_{\lambda\mu}-\partial_\lambda h_{\mu\nu})$.
proof idea
Term-mode proof in three steps. Unfold the definition of the linearized Einstein tensor (the flat-space combination of linearized Ricci and linearized scalar curvature). Rewrite both pieces by the TT-specialized lemmas linRicci_tt and linRicciScalar_tt, which already insert the factor $\tfrac12|k|^2 H_{\mu\nu}\cos(k\cdot x)$ structure under the transverse-traceless hypothesis. The remaining identity is purely algebraic and is discharged by ring.
why it matters
This is the componentwise Einstein-tensor evaluation that the second-variation density needs. Downstream, ehSecondVariationDensity_tt (doc-commented as A3) contracts $h_{\mu\nu}G^{(1)\mu\nu}$ and obtains
$d^2/dt^2$ density $= -\tfrac12|k|^2|H|F^2\cos^2(k\cdot x)$, quoting Euler's theorem for the quadratic form $S^{(2)}[h]=-\tfrac12\int h,G^{(1)}$ coming from $\delta(\sqrt{g}R)/\delta g{\mu\nu}=-\sqrt{g}G^{\mu\nu}$ about flat space.
The module exists because the Regge exact-flat Hessian norm gate bridged a computed $-1/8$ to a frozen preflight $-1/4$ by an underived bookkeeping factor 2. Deriving the continuum side here, without reading the discrete answer, lets ReggeNormalizationDerived4D compare the two numbers honestly. Framework role: continuum gravity side of the discrete-to-continuum matching chain for the EH Hessian on TT modes in 4D (D=3 spatial plus time), not a forcing-chain T0–T8 step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.