ehFace_eq_average_of_density
plain-language theorem explainer
On a real transverse-traceless plane wave, the continuum Einstein-Hilbert second-variation density at a point equals the phase-density evaluated at the local wave phase, and the face value is exactly the average of that phase-density over the circle. Anyone matching continuum EH to the banked Regge midpoint dictionary cites this factorization. The proof is a two-conjunct term pairing existing density-through-phase and face-as-phase-average lemmas.
Claim. Let $H$ be a $4\times 4$ polarization matrix and $k$ a wave covector on $\mathbb{R}^4$. If $(H,k)$ is transverse-traceless, then for every spacetime point $x$ the continuum Einstein-Hilbert second-variation density at $x$ equals the phase-density of $(H,k)$ evaluated at the plane-wave phase $k\cdot x$, and the EH face value of $(H,k)$ equals the circle average of that phase-density.
background
This module (Arc 2, step 7) derives, from the linearized Levi-Civita connection alone, the number that the Einstein-Hilbert action assigns to a real transverse-traceless plane wave $h(x)=H\cos(k\cdot x)$, in the same convention as the banked Regge midpoint dictionary. Coordinates are $Pt:=\mathrm{Fin},4\to\mathbb{R}$. The discrete Bloch symbol averages $d^2/dt^2$ of the Regge action under that real cosine; the continuum object is therefore the phase average of the second variation density of $\int R\sqrt{g}$ per unit volume, not the bare quadratic Taylor coefficient (which differs by another factor of 2).
Named classical input A1 is the linearized Christoffel symbol $\Gamma^{(1)}{\lambda\mu\nu}=\tfrac12(\partial\mu h_{\lambda\nu}+\partial_\nu h_{\lambda\mu}-\partial_\lambda h_{\mu\nu})$. The module imports only Mathlib and a linear-algebra edge decomposition, so it cannot have read the discrete answer. The comparison against the dictionary lives elsewhere (ReggeNormalizationDerived4D).
proof idea
Term-mode pair constructor. The left conjunct is the already-proved statement that, under the TT hypothesis, the second-variation density at $x$ factors through the scalar phase $k\cdot x$ (so it equals densityOfPhase at that phase). The right conjunct is the already-proved identification of the EH face with the circle average of that same phase-density. No new algebra is done here; the theorem only packages the two facts as a single conjunction.
why it matters
The continuum face value is the independent number that must be compared to the discrete Regge Hessian entry (and to the frozen preflight $-1/4$ bridged by an underived bookkeeping factor 2). Packaging density-through-phase with face-as-average makes precise that ehFace is a single scalar per $(H,k)$, not a free family: the next section uses exactly this rigidity to kill decoy T3 (scaling the density by $c\neq 1$ changes the face). In the broader Recognition gravity arc this is the continuum half of the normalization match that decides whether the discrete dictionary coefficient is forced or conventional. No downstream consumers are wired yet in the graph; the natural landing site is the separate normalization-derived comparison module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.