ehFace_eq_phaseAverage
plain-language theorem explainer
On a real transverse-traceless cosine wave in 4D, the continuum Einstein-Hilbert face equals the phase average of the second-variation density. Anyone matching continuum EH to the Regge midpoint dictionary cites this identity as P1. The proof unfolds both sides and reduces via constant-factor and cos-squared averaging lemmas plus ring arithmetic.
Claim. For any $4\times 4$ polarization matrix $H$ and wave covector $k\in\mathbb{R}^4$, the continuum Einstein-Hilbert face equals the one-period phase average of the second-variation density: $\mathrm{ehFace}(H,k)=\frac{1}{2\pi}\int_0^{2\pi}\rho_{H,k}(\theta)\,d\theta$, where $\rho_{H,k}(\theta)=-\tfrac12\,|k|^2\|H\|_F^2\cos^2\theta$ and $\mathrm{ehFace}(H,k)=-\tfrac14\,|k|^2\|H\|_F^2$.
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, in the same convention as the banked Regge midpoint dictionary. It deliberately imports only Mathlib and edge TT linear algebra, so the continuum coefficient cannot have read the discrete answer.
The discrete Bloch symbol averages $d^2/dt^2$ of the Regge action under the real perturbation $h(x)=H\cos(k\cdot x)$. Matching that convention, the continuum object is the phase average of the second variation of $\int R\sqrt{g}$ per unit volume under the same real cosine wave (not the quadratic Taylor coefficient, which differs by another factor of 2).
densityOfPhase packages the §5 density as a function of phase alone: $-\tfrac12,|k|^2|H|_F^2\cos^2\theta$. ehFace is defined as $-\tfrac14,|k|^2|H|_F^2$. phaseAverage is the mean of a phase function over $[0,2\pi]$.
proof idea
Short algebraic identification. Unfold densityOfPhase and ehFace so the goal is that the phase average of $c\cos^2\theta$ equals $-\tfrac14,|k|^2|H|_F^2$ with $c=-\tfrac12,|k|^2|H|_F^2$. Pull the constant out with phaseAverage_const_mul, replace the average of $\cos^2$ by $1/2$ via phaseAverage_cos_sq, and finish with ring: $(-1/2)\cdot(1/2)=-1/4$.
why it matters
Doc-comment labels this P1: the derived face is the average of the derived density, with every step from Levi-Civita already proved upstream. It is the hinge that turns the explicit density formula into the single continuum number used for dictionary comparison.
Downstream, ehFace_eq_average_of_density packages P1 with the pointwise density factorization; ehFace_rigid uses it to show no free multiplicative constant can sit in front of the density without changing the face (rigidity of the derivation). In EHSecondVariationExact4D, a3_agrees_with_exact rewrites through this identity to confirm that step 7's assumed RHS and the exact LHS share the same wavelength average, so the assumption did not move the coefficient.
In the larger gravity arc this closes the continuum side of the Regge normalization problem that forced an underived discreteBookkeepingFactor := 2 in the flat Hessian norm gate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.