ehFace
plain-language theorem explainer
The continuum Einstein-Hilbert face maps a 4×4 polarization H and wavevector k to −(1/4)|k|²‖H‖_F². It is the phase-averaged second variation, per unit volume, of ∫√g R on a real transverse-traceless cosine wave, derived from linearized Levi-Civita alone. Gravity analysts matching continuum EH to the Regge midpoint dictionary cite it. The body is a one-line algebraic product of momentum square and Frobenius square.
Claim. For a $4\times 4$ polarization matrix $H$ and wavevector $k\in\mathbb{R}^4$, the continuum Einstein-Hilbert face is $-\frac14\,|k|^2\,\|H\|_F^2$. By design this equals the phase average, per unit volume, of $\frac{d^2}{dt^2}\int\sqrt{g}\,R$ on the real transverse-traceless plane wave $h(x)=H\cos(k\cdot x)$.
background
Arc 2, step 7 of the continuum TT second-variation program. The module derives, from the Levi-Civita connection and nothing else, the number that the Einstein-Hilbert action assigns to a real transverse-traceless plane wave, in the same convention the banked Regge midpoint dictionary uses.
Coordinates live on Pt := Fin 4 → ℝ. The polarization is a 4×4 matrix; frobSq is its Frobenius square. The discrete symbol averages $d^2/dt^2$ of the Regge action under the real perturbation $h(x)=H\cos(k\cdot x)$; the lattice average of $\cos\cos$ supplies an explicit $1/2$. The continuum object is therefore the phase average of $d^2/dt^2\int R\sqrt{g}$ per unit volume under that same real cosine wave, not the quadratic Taylor coefficient (which would differ by another factor of 2).
Classical input A1 is the linearized Christoffel symbol $\Gamma^{(1)}{\lambda\mu\nu}=\frac12(\partial\mu h_{\lambda\nu}+\partial_\nu h_{\lambda\mu}-\partial_\lambda h_{\mu\nu})$. The module imports only Mathlib and a pure linear-algebra edge decomposition, so it cannot have read the discrete answer.
proof idea
Pure definition: the face is declared to be $-\frac14$ times momentum-square of $k$ times Frobenius square of $H$. No tactics, no lemmas. Downstream theorems (ehFace_eq_phaseAverage, density factorizations) then prove this closed form equals the phase average of the second-variation density built from the linearized connection.
why it matters
This is the continuum target that the whole step-7 derivation aims at. Parent results include ehFace_eq_phaseAverage (P1: face equals phase average of the derived density), ehFace_eq_average_of_density, and the rigidity lemma ehFace_rigid (any constant prefactor on the density that still averages to the face must be 1).
In EHSecondVariationExact4D, exact_average_eq_ehFace shows the wavelength average of the exact (non-linearized) second variation lands on this face when $|H|_F^2=2$. Longitudinal and trace decoys are shown to miss it. The geometric-fold comparison module also reads the face against axis-TT symbols.
Historically, the Regge norm gate bridged a computed $-1/8$ to a frozen $-1/4$ by an underived bookkeeping factor 2. Step 6 refuted the cheap Frobenius explanation; this definition supplies an independent continuum number so the comparison in ReggeNormalizationDerived4D is non-circular.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.