linEinstein
plain-language theorem explainer
Defines the linearized Einstein tensor on a real plane-wave metric perturbation in flat 4D: G^{(1)}_{\mu\nu} equals the linearized Ricci tensor minus half the Kronecker delta times the linearized Ricci scalar. Anyone computing the continuum Einstein–Hilbert second variation under a cosine wave cites this. The body is a one-line algebraic combination of the already-defined linearized Ricci pieces.
Claim. For a constant polarization matrix $H$, wave covector $k$, indices $\mu,\nu\in\{0,1,2,3\}$, and spacetime point $x$, the linearized Einstein tensor is $G^{(1)}_{\mu\nu}(x)=R^{(1)}_{\mu\nu}(x)-\tfrac12\delta_{\mu\nu}R^{(1)}(x)$, where $R^{(1)}$ is the linearized Ricci tensor of the real cosine wave $h=H\cos(k\cdot x)$ and $R^{(1)}$ its flat-metric trace.
background
This module (Arc 2, step 7) derives the continuum second variation of $\int R\sqrt{g}$ on a real transverse-traceless plane wave in 4D, matched to the discrete Regge midpoint convention. It imports only Mathlib and edge TT linear algebra, so the continuum coefficient is independent of the banked discrete dictionary.
Coordinates are points $x:\mathrm{Fin},4\to\mathbb{R}$. The metric perturbation is the real cosine wave built from a constant $4\times4$ matrix $H$ and wave vector $k$. Upstream, the linearized Christoffel symbols (A1) feed the linearized Ricci tensor (A2): $R^{(1)}{\mu\nu}=\partial\lambda\Gamma^{(1)\lambda}{\mu\nu}-\partial\nu\Gamma^{(1)\lambda}{\mu\lambda}$, with $\Gamma\Gamma$ terms dropped as quadratic in $h$. The linearized Ricci scalar is the flat trace $\sum\mu R^{(1)}_{\mu\mu}$.
The classical Einstein tensor is $G_{\mu\nu}=R_{\mu\nu}-\tfrac12 g_{\mu\nu}R$. At linear order about flat space one replaces $g$ by $\delta$, so the correction is exactly half $\delta_{\mu\nu}$ times the linearized scalar.
proof idea
Pure definitional abbreviation: evaluate linearized Ricci at $(\mu,\nu,x)$, subtract $\tfrac12$ times the Kronecker factor $(\mu=\nu)$ times the linearized Ricci scalar at $x$. No lemmas, no tactics; the Kronecker is written as a Boolean conditional on index equality.
why it matters
This is the classical density that turns the EH second variation into a contraction against $h$. Downstream, ehSecondVariationDensity sets $d^2/dt^2\int\sqrt{g}R$ density equal to $-\sum_{\mu\nu}h_{\mu\nu}G^{(1)}{\mu\nu}$ (A3, Euler on the quadratic form $S^{(2)}[h]=-\tfrac12\int h,G^{(1)}$). Under the TT hypothesis, linEinstein_tt collapses the definition to $\tfrac12|k|^2 H{\mu\nu}\cos(k\cdot x)$, which then yields the closed TT second-variation density $-\tfrac12|k|^2|H|_F^2\cos^2(k\cdot x)$.
That continuum number is what step 7 compares, in a separate non-circular module, against the Regge exact-flat Hessian symbol, resolving the discrete bookkeeping factor of 2 that previously bridged $-1/8$ and $-1/4$ without derivation. It sits in the gravity analysis chain that anchors continuum GR coefficients used by the Recognition lattice dictionary; it does not itself invoke T0–T8 or the J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.