sum_k_chrAmp
plain-language theorem explainer
For a symmetric, k-transverse 4×4 polarization H, contracting the wavevector into the linearized Christoffel amplitude yields half the squared momentum times H_μν. Anyone reducing the continuum Ricci amplitude on real TT plane waves cites this identity. The proof expands the closed-form Christoffel amplitude, applies the transverse row-sum twice, and cancels the off-diagonal terms.
Claim. Let $H$ be a symmetric real $4\times 4$ matrix and $k\in\mathbb{R}^4$ a wavevector such that $H$ is transverse to $k$. Write $\Gamma^{(1)}_{l\mu\nu}(H,k)=\tfrac12(k_l H_{\mu\nu}-k_\mu H_{l\nu}-k_\nu H_{l\mu})$ for the plane-wave amplitude of the linearized Christoffel symbol. Then for all indices $\mu,\nu\in\{0,1,2,3\}$, $\sum_l k_l\,\Gamma^{(1)}_{l\mu\nu}(H,k)=\tfrac12 |k|^2 H_{\mu\nu}$.
background
This module (Arc 2, step 7) derives the continuum second variation of $\int R\sqrt{g}$ on a real transverse-traceless plane wave $h(x)=H\cos(k\cdot x)$ in 4D, matching the discrete Regge midpoint convention. It imports only Mathlib and linear-algebra edge decomposition, so the continuum coefficient is obtained independently of the banked discrete dictionary.
The linearized Levi-Civita connection is $\Gamma^{(1)}{\lambda\mu\nu}=\tfrac12(\partial\mu h_{\lambda\nu}+\partial_\nu h_{\lambda\mu}-\partial_\lambda h_{\mu\nu})$. On the cosine wave its amplitude collapses to the closed form chrAmp: $\tfrac12(k_l H_{\mu\nu}-k_\mu H_{l\nu}-k_\nu H_{l\mu})$. Here $k$ is a point of type $\mathrm{Fin},4\to\mathbb{R}$, and $H$ is assumed symmetric and transverse ($\sum_l k_l H_{l\nu}=0$).
The companion row identity sum_k_mul_row packages that transversality after summing against $k$, and is the only nontrivial input beyond algebra.
proof idea
Invoke the transverse row-sum identity once at index $\mu$ and once at $\nu$. For each $l$, expand $k_l$ times the Christoffel amplitude by unfolding the closed form and rearranging with ring; the summand splits into three pieces: $\tfrac12 H_{\mu\nu},k_l^2$ minus two cross terms linear in the rows of $H$.
Rewrite the full sum by congruence, distribute over the two subtractions, and pull the constant factors out of each sum. The two cross sums are exactly the row-sum identity, hence vanish. What remains is $\tfrac12 H_{\mu\nu}\sum_l k_l^2$, which is $\tfrac12$ times momentum-squared times $H_{\mu\nu}$ after unfolding the momentum-square definition and a final ring.
why it matters
This is the contraction step that turns the linearized Christoffel amplitude into the Ricci amplitude on TT data. The sole downstream consumer is ricciAmp_tt, which unfolds the Ricci amplitude, applies this sum together with the trace-sum identity, and concludes $\mathrm{ricciAmp}(H,k){\mu\nu}=\tfrac12 |k|^2 H{\mu\nu}$ for every TT polarization.
That Ricci amplitude is the continuum input to the second variation of $\int R\sqrt{g}$ under a real cosine wave, the object the module exists to compute. The larger Arc 2 goal is to derive the continuum Hessian coefficient independently and compare it with the discrete Regge symbol (which carries a frozen bookkeeping factor of 2). Because the module never imports the coupling table or the norm gate, the number that emerges here is non-circular.
In the Recognition gravity stack this sits on the continuum side of the Regge-normalization comparison, not on the forcing chain (T0–T8) or the J-cost algebra; those appear only as ambient imports.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.