hWave
plain-language theorem explainer
Defines the metric perturbation component as a real cosine standing wave: h_ab(x) = H_ab cos(k·x). Anyone deriving the continuum Einstein-Hilbert second variation on a TT plane wave in the discrete Regge convention cites this. Pure definitional product of constant polarization amplitude and plane-wave phase cosine.
Claim. For a constant $4\times 4$ polarization matrix $H$, wavevector $k\in\mathbb{R}^4$, indices $a,b\in\{0,1,2,3\}$, and point $x\in\mathbb{R}^4$, set $h_{ab}(x)=H_{ab}\cos(k\cdot x)$, where $k\cdot x=\sum_i k_i x_i$.
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, from the Levi-Civita connection alone. It deliberately imports only Mathlib and edge TT linear algebra, so the continuum coefficient cannot have read the discrete answer.
Coordinates are Pt := Fin 4 → ℝ. The plane-wave phase is $k\cdot x=\sum_i k_i x_i$. The discrete Regge Bloch symbol uses the real perturbation $h(x)=H\cos(k\cdot x)$; the continuum side must match that convention (not a complex exponential, and not the pure quadratic Taylor coefficient, which differs by a further factor of 2 from the phase average).
The shifted cost $H(x)=J(x)+1$ from the Recognition cost algebra is unrelated name collision; here $H$ is only the constant polarization matrix.
proof idea
Definitional one-liner: multiply the constant matrix entry $H_{ab}$ by $\cos(\mathrm{phase}(k,x))$. No lemmas, no tactics.
why it matters
This is the seed field for the whole continuum derivation. Linearized Christoffel (A1) differentiates it via partials of the cosine; the Einstein-Hilbert second-variation density (A3) contracts it against the linearized Einstein tensor. Downstream, ehSecondVariationDensity_tt evaluates the TT case to $-\frac12 |k|^2|H|_F^2\cos^2(k\cdot x)$, and linChristoffel_eq closes the Christoffel amplitude to a sine wave.
The module exists because the discrete-to-continuum norm gate previously inserted an underived bookkeeping factor 2. Deriving the continuum number independently (same real-cosine convention) is the honest comparison path into ReggeNormalizationDerived4D. No T0–T8 forcing step is claimed here; this is classical GR linearization staged for that comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.