ehSecondVariationDensity_tt
plain-language theorem explainer
For a transverse-traceless polarization H and wave covector k, the continuum Einstein-Hilbert second-variation density of the real cosine plane wave equals minus one-half times momentum-squared times the Frobenius square of H, times cos squared of the local phase. Continuum-to-Regge normalization work cites this pointwise identity. The proof substitutes the TT linearized Einstein tensor componentwise, then factors the double sum by ring algebra.
Claim. Let $H$ be a real $4\times 4$ matrix and $k$ a covector on $\mathbb{R}^4$. If $H$ is transverse-traceless relative to $k$, then at every point $x$ the Einstein-Hilbert second-variation density of the real plane wave $h(y)=H\cos(k\cdot y)$ equals $-\tfrac12\,|k|^2\,\|H\|_F^2\,\cos^2(k\cdot x)$.
background
This module (Arc 2, step 7) derives, from the Levi-Civita connection alone, the continuum second variation that the Einstein-Hilbert action assigns to a real transverse-traceless plane wave in 4D, in the same convention as the banked Regge midpoint dictionary. The discrete symbol averages $d^2/dt^2$ of the Regge action under the real perturbation $h(x)=H\cos(k\cdot x)$; the continuum object here is the phase-dependent density of that same second variation per unit volume, not the quadratic Taylor coefficient (which would differ by a further factor of 2).
Coordinates are maps $x:\mathrm{Fin},4\to\mathbb{R}$. The phase is the plane-wave pairing $k\cdot x$. The Frobenius square $|H|F^2=\sum{\mu\nu}H_{\mu\nu}^2$ is the polarization norm. The transverse-traceless hypothesis collapses the linearized Einstein tensor of the cosine wave to a pure multiple of $H$ itself (the identity used componentwise in the proof).
Structurally the module imports only Mathlib and a pure linear-algebra edge decomposition, so nothing here can have read the discrete coupling table, Bloch symbol, or norm-gate answer.
proof idea
Unfold the second-variation density, the cosine wave field, and the Frobenius square. For each index pair $(\mu,\nu)$, rewrite the summand $H_{\mu\nu}\cos(\mathrm{phase})\cdot G^{(1)}{\mu\nu}$ by the TT linearized-Einstein identity, which replaces $G^{(1)}$ by $\tfrac12|k|^2\cos(\mathrm{phase}),H{\mu\nu}$. A ring step yields the monomial $\tfrac12|k|^2\cos^2(\mathrm{phase}),H_{\mu\nu}^2$ on every component. Congruence of the double finite sum, factoring the common scalar out of both sums, and a final ring calculation produce the global formula $-\tfrac12|k|^2|H|_F^2\cos^2(\mathrm{phase})$.
why it matters
This is the algebraic core of the continuum TT density in §5 of the module. Downstream, the theorem that the density factors through phase is a one-line rephrasing of this identity, packaging the right-hand side as a pure function of the phase so the period average can be taken. That average is the derived continuum Einstein-Hilbert face: the phase-averaged per-unit-volume second variation of $\int R\sqrt{g}$ on a real TT cosine wave.
The face is the continuum number against which the Regge discrete Hessian is compared in the separate normalization module. The discrete side had bridged a computed $-1/8$ to a frozen preflight $-1/4$ by an underived bookkeeping factor of 2; deriving the continuum coefficient independently is what makes that comparison non-circular. Within Recognition Science gravity this supports the continuum side of the discrete quantum-gravity dictionary, not the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.