linRicci
plain-language theorem explainer
Linearized Ricci tensor on a real plane-wave metric perturbation in 4D Euclidean signature: first derivatives of the linearized Christoffel symbols only, with the quadratic ΓΓ pieces dropped. Anyone deriving the continuum second variation of the Einstein–Hilbert action on a TT wave cites this as the classical A2 input. The body is a direct transcription of the standard linearization formula in coordinates.
Claim. For a constant polarization matrix $H$, wave vector $k$, and point $x\in\mathbb{R}^4$, the linearized Ricci component is $$R^{(1)}_{\mu\nu}(x)=\partial_\lambda\Gamma^{(1)\lambda}_{\mu\nu}(x)-\partial_\nu\Gamma^{(1)\lambda}_{\mu\lambda}(x),$$ where $\Gamma^{(1)}$ is the linearized Levi-Civita connection of the real cosine wave $h_{ab}(x)=H_{ab}\cos(k\cdot x)$, and indices are raised with the flat metric. Quadratic $\Gamma\Gamma$ terms are omitted as $O(h^2)$.
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 same real-cosine convention used by the banked Regge midpoint dictionary. It imports only Mathlib and edge TT linear algebra, so the continuum coefficient is independent of any discrete coupling table or preflight norm gate.
Coordinates are $x:\mathrm{Fin},4\to\mathbb{R}$. Partial derivatives pd are ordinary one-variable derivatives along a single coordinate. The metric perturbation is the real wave $h=H\cos(k\cdot x)$. Upstream A1 defines 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})$$ with indices raised by the flat Euclidean metric.
Classical Ricci linearization drops the products of Christoffels: those are quadratic in $h$ and vanish at first order. The definition here is exactly that first-order remainder.
proof idea
Definitional, not a proof. The body writes the coordinate formula as a finite sum over the dummy index $\lambda$ of $\partial_\lambda\Gamma^{(1)\lambda}{\mu\nu}$, minus the $\nu$-derivative of the contracted $\sum\lambda\Gamma^{(1)\lambda}_{\mu\lambda}$. Both pieces call the sibling linearized Christoffel and the coordinate partial pd. No algebraic simplification is performed at this stage; closed-form amplitudes appear in later lemmas.
why it matters
A2 in the module's named classical inputs. Downstream, linRicci_eq factors the plane-wave dependence as amplitude times $\cos(k\cdot x)$; on the TT subspace, linRicci_tt collapses that amplitude to $\tfrac12|k|^2 H_{\mu\nu}\cos(k\cdot x)$, i.e. half the massless wave operator on $h$. The trace linRicciScalar and the linearized Einstein tensor $G^{(1)}{\mu\nu}=R^{(1)}{\mu\nu}-\tfrac12\delta_{\mu\nu}R^{(1)}$ are built directly from this definition.
Those objects feed the continuum second-variation density that is compared, in a separate non-circular module, against the Regge discrete Hessian. The comparison settles whether the continuum side produces $-1/8$ or $-1/4$ per unit volume for a normalized TT wave, closing the bookkeeping gap that previously required an underived factor of 2. Within Recognition gravity this is pure classical GR input (Levi-Civita only), not a forcing-chain step; it anchors the continuum half of the discrete-to-continuum dictionary for the TT sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.