sum_chrAmp_trace
plain-language theorem explainer
For a symmetric traceless 4×4 polarization and wavevector k, the sum over the repeated index of the linearized Christoffel amplitude with pattern (l, μ, l) is identically zero. Anyone reducing the continuum Ricci amplitude on transverse-traceless plane waves cites this cancellation. The proof rewrites each summand as a multiple of the diagonal entry H_ll and invokes tracelessness.
Claim. Let $H$ be a real symmetric traceless $4\times 4$ matrix and $k\in\mathbb{R}^4$. Write the linearized Christoffel amplitude as $\Gamma^{\mathrm{amp}}_{l\mu\nu}(H,k)=\tfrac12(k_l H_{\mu\nu}-k_\mu H_{l\nu}-k_\nu H_{l\mu})$. Then for every fixed index $\mu\in\{0,1,2,3\}$, $$\sum_{l=0}^{3}\Gamma^{\mathrm{amp}}_{l\mu l}(H,k)=0.$$
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, matching the discrete Regge midpoint convention. It imports only Mathlib and the edge TT linear-algebra layer, so the continuum coefficient is independent of the banked discrete dictionary.
The amplitude chrAmp is the closed form of the linearized Levi-Civita symbol on $h(x)=H\cos(k\cdot x)$: $\Gamma^{\mathrm{amp}}{l\mu\nu}=\tfrac12(k_l H{\mu\nu}-k_\mu H_{l\nu}-k_\nu H_{l\mu})$. Symmetry of $H$ is $H_{ij}=H_{ji}$; tracelessness is $\sum_l H_{ll}=0$. The wavevector lives in $\mathrm{Pt}:=\mathrm{Fin},4\to\mathbb{R}$.
The Ricci amplitude on TT modes is assembled from two summed Christoffel contractions; this lemma kills the pure-trace contraction.
proof idea
For each $l$, unfold the amplitude and apply symmetry $H_{l\mu}=H_{\mu l}$. Algebraic rearrangement (ring) yields $\Gamma^{\mathrm{amp}}{l\mu l}=-\tfrac12 k\mu, H_{ll}$. Congruence of the finite sum, then sum_neg_distrib and factoring the constant $-\tfrac12 k_\mu$ out of the sum, reduces the claim to $\sum_l H_{ll}=0$, which is exactly the traceless hypothesis. A final ring closes.
why it matters
Parent theorem ricciAmp_tt applies this identity together with the transverse contraction sum_k_chrAmp to obtain $\mathrm{ricciAmp}(H,k){\mu\nu}=\tfrac12 |k|^2 H{\mu\nu}$ on TT data. That Ricci amplitude is the continuum input to the second variation of the Einstein-Hilbert action on real cosine waves, the object compared against the discrete Regge Hessian in the normalization arc.
Without the trace cancellation the continuum side would retain a pure-trace remainder incompatible with the TT sector. The module's non-circularity guarantee (no import of coupling tables or preflight coefficients) makes this algebraic step part of an independent continuum derivation rather than a fit to the discrete answer. Framework context: continuum check of the 4D gravitational quadratic form that the Recognition lattice side packages via the eight-tick / $D=3$ forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.