ehSecondVariationDensity
plain-language theorem explainer
Defines the continuum Einstein–Hilbert second-variation density at a spacetime point: minus the contraction of a real cosine metric wave with the linearized Einstein tensor. Anyone comparing continuum EH to the Regge midpoint dictionary cites this as the local integrand before phase averaging. It is a direct definition encoding Euler’s identity for the quadratic form S⁽²⁾[h] = −½ ∫ h G⁽¹⁾.
Claim. For a constant polarization matrix $H$, wavevector $k$, and point $x\in\mathbb{R}^4$, the second-variation density of the Einstein–Hilbert action along $g=\delta+t h$ is $\rho(H,k,x)=-\sum_{\mu,\nu=0}^{3} h_{\mu\nu}(x)\,G^{(1)\mu\nu}(x)$, where $h_{\mu\nu}(x)=H_{\mu\nu}\cos(k\cdot x)$ is the real standing wave and $G^{(1)}$ is the linearized Einstein tensor of $h$.
background
This module (Arc 2, step 7) derives the continuum transverse-traceless second variation of $\int R\sqrt{g}$ in 4D from the Levi-Civita connection alone, in the same real-cosine convention as the banked Regge midpoint dictionary. It deliberately imports only Mathlib and linear-algebra edge decomposition, so the continuum number cannot have read the discrete answer.
Coordinates are maps $\mathrm{Pt}=\mathrm{Fin},4\to\mathbb{R}$. The metric perturbation is the real standing wave $h_{ab}(x)=H_{ab}\cos(k\cdot x)$, matching the discrete side’s $h(x)=H\cos(k\cdot x)$ rather than a complex exponential. The linearized Einstein tensor is $G^{(1)}{\mu\nu}=R^{(1)}{\mu\nu}-\tfrac12\delta_{\mu\nu}R^{(1)}$, built from the linearized Christoffel symbols (A1) and Ricci.
Classical input A3 records that the second derivative of $\int\sqrt{g}R$ along $g=\delta+th$ is the density $-\int h_{\mu\nu}G^{(1)\mu\nu}$. That identity is Euler’s theorem for the quadratic form $S^{(2)}[h]=-\tfrac12\int h,G^{(1)}$, itself the flat-space expansion of $\delta(\sqrt{g}R)/\delta g_{\mu\nu}=-\sqrt{g}G^{\mu\nu}$.
proof idea
Pure definition: the body is the pointwise double sum $-\sum_{\mu}\sum_{\nu} h_{\mu\nu}(x),G^{(1)}_{\mu\nu}(x)$, with $h$ expanded via the real cosine wave and $G^{(1)}$ via the linearized Einstein tensor. No lemmas or tactics; the mathematical content is the classical A3 contraction written as a Lean function of polarization, wavevector, and point.
why it matters
This density is the local continuum object that later gets phase-averaged to produce the continuum Einstein–Hilbert face used against the Regge dictionary. Downstream, ehSecondVariationDensity_tt evaluates it on transverse-traceless polarizations to $-\tfrac12|k|^2|H|_F^2\cos^2(k\cdot x)$; density_factors_through_phase packages that as a pure function of the phase; and ehFace_eq_average_of_density identifies the continuum face with the phase average of that density.
The module exists because the discrete bookkeeping factor 2 bridging $-(1/8)$ and $-(1/4)$ was previously underived. Deriving this continuum integrand independently (no coupling table, Bloch symbol, or norm gate) lets the comparison module decide which number is forced. Within Recognition gravity, it is the continuum half of the TT second-variation match that underwrites the discrete curvature cost on the eight-tick, $D=3$ lattice side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.