chrAmp
plain-language theorem explainer
Closed-form prefactor of the linearized Christoffel symbol for a real cosine plane wave h = H cos(k·x) in 4D. Anyone deriving the continuum TT second variation of ∫R√g cites it as the algebraic kernel of Γ⁽¹⁾. The body is the standard Levi-Civita linearization with ∂ → k factors pulled out, leaving a pure tensor amplitude times sin(k·x).
Claim. For a symmetric $4\times 4$ amplitude matrix $H$, wave covector $k\in\mathbb{R}^4$, and indices $\lambda,\mu,\nu\in\{0,1,2,3\}$, the Christoffel amplitude is $\mathrm{chrAmp}(H,k)_{\lambda\mu\nu} := \tfrac12\bigl(k_\lambda H_{\mu\nu}-k_\mu H_{\lambda\nu}-k_\nu H_{\lambda\mu}\bigr)$.
background
This module (Arc 2, step 7) derives the continuum transverse-traceless second variation of the Einstein-Hilbert action on a real cosine plane wave in 4D, matched to the banked Regge midpoint convention. It imports only Mathlib and edge TT linear algebra, so the continuum coefficient is independent of the discrete dictionary.
Named classical input A1 is the linearized Levi-Civita connection $\Gamma^{(1)}{\lambda\mu\nu}=\tfrac12(\partial\mu h_{\lambda\nu}+\partial_\nu h_{\lambda\mu}-\partial_\lambda h_{\mu\nu})$. The metric perturbation is the real wave $h(x)=H\cos(k\cdot x)$, with phase $k\cdot x$ on coordinate space $\mathrm{Pt}:=\mathrm{Fin},4\to\mathbb{R}$. Partial derivatives of $\cos(k\cdot x)$ produce $\pm k_i\sin(k\cdot x)$, so $\Gamma^{(1)}$ factors as a $k$- and $H$-dependent amplitude times $\sin(k\cdot x)$.
That amplitude is exactly the object defined here: the closed-form coefficient of the linearized Christoffel symbol on the plane wave.
proof idea
Pure definitional abbreviation, not a proof. Substitute the plane-wave ansatz into A1, replace each partial by the corresponding $k$-component times $-\sin$ (or $+\sin$ after sign bookkeeping), and collect the overall $\sin(k\cdot x)$ factor. What remains is $\tfrac12(k_\lambda H_{\mu\nu}-k_\mu H_{\lambda\nu}-k_\nu H_{\lambda\mu})$. No lemmas are invoked; the equality to the pointwise linearized Christoffel is discharged later by linChristoffel_eq via pd_cos and ring.
why it matters
This is the algebraic seed of the continuum TT Hessian derivation. Downstream, linChristoffel_eq states that the pointwise linearized Christoffel equals this amplitude times $\sin(k\cdot x)$. The Ricci amplitude ricciAmp is built by contracting $k_\ell\cdot\mathrm{chrAmp}$ and a trace term; linRicci_eq then factors the linearized Ricci as that amplitude times $\cos(k\cdot x)$.
Under transverse-traceless hypotheses, sum_k_chrAmp collapses $\sum_\ell k_\ell,\mathrm{chrAmp}$ to $\tfrac12|k|^2 H_{\mu\nu}$, and sum_chrAmp_trace kills the residual trace sum. Those identities feed the second-variation assembly that produces the continuum number compared, in a separate non-circular module, against the Regge dictionary factor. Within RS gravity analysis this closes the honest continuum side of the $-(1/8)$ vs $-(1/4)$ bookkeeping question without reading the discrete answer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.