linChristoffel
plain-language theorem explainer
Defines the linearized Christoffel symbol Γ⁽¹⁾_{λμν} for a real transverse-traceless plane-wave metric perturbation on flat 4D Euclidean space. Anyone deriving the continuum second variation of the Einstein-Hilbert action under h = H cos(k·x) cites this as classical input A1. The body is the standard Levi-Civita linearization written with the module's partials and standing-wave field.
Claim. For a constant polarization matrix $H$, wavevector $k$, and indices $\lambda,\mu,\nu\in\{0,1,2,3\}$, the linearized Christoffel symbol at a point $x\in\mathbb{R}^4$ is $$\Gamma^{(1)}_{\lambda\mu\nu}(x)=\tfrac12\bigl(\partial_\mu h_{\lambda\nu}+\partial_\nu h_{\lambda\mu}-\partial_\lambda h_{\mu\nu}\bigr),$$ where $h_{ab}(x)=H_{ab}\cos(k\cdot x)$ and indices are raised with the flat Euclidean metric.
background
This module (Arc 2, step 7) derives the continuum second variation of $\int R\sqrt{g}$ on a real TT plane wave in 4D, matching the discrete Regge midpoint convention, without importing any banked coefficient or norm gate.
Coordinates are points $x:\mathrm{Fin},4\to\mathbb{R}$. The partial $\partial_\mu$ is the ordinary directional derivative along coordinate $\mu$. The metric perturbation is the real standing wave $h_{ab}(x)=H_{ab}\cos(k\cdot x)$, chosen so the continuum phase average lines up with the lattice average of $\cos(k\cdot m_e)\cos(k\cdot m_e')$ on the discrete side.
Named classical input A1 is the first-order Levi-Civita connection on flat space: the usual $\Gamma^{(1)}{\lambda\mu\nu}=\tfrac12(\partial\mu h_{\lambda\nu}+\partial_\nu h_{\lambda\mu}-\partial_\lambda h_{\mu\nu})$. Quadratic $\Gamma\Gamma$ pieces are deferred; they drop out of the linearized Ricci tensor used later.
proof idea
Pure definition, not a theorem. The body is the textbook linearization: half the sum of $\partial_\mu$ of the $(\lambda\nu)$ component of the standing wave, $\partial_\nu$ of the $(\lambda\mu)$ component, minus $\partial_\lambda$ of the $(\mu\nu)$ component, evaluated at $x$. No lemmas are applied; the closed form on the cosine wave is proved separately by unfolding and the cosine derivative rules.
why it matters
A1 is the first named classical input in the continuum TT second-variation derivation. Downstream, linChristoffel_eq extracts the sine amplitude of this symbol on the plane wave; linRicci contracts its derivatives into the linearized Ricci tensor $R^{(1)}{\mu\nu}=\partial\lambda\Gamma^{(1)\lambda}{\mu\nu}-\partial\nu\Gamma^{(1)\lambda}_{\mu\lambda}$; and linRicci_eq closes that amplitude. Those steps feed the independent continuum number that is later compared, in a separate non-circular module, against the banked Regge dictionary factor. The point is structural honesty: the continuum side is rebuilt from Levi-Civita alone so the $-(1/8)$ versus $-(1/4)$ bookkeeping gap is not smuggled in by import.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.