density_factors_through_phase
plain-language theorem explainer
For a transverse-traceless polarization matrix H and wavevector k, the continuum Einstein-Hilbert second-variation density at spacetime point x equals that density read as a function of the plane-wave phase k·x alone. Continuum-vs-Regge normalizers cite this when reducing the EH face to a phase average. The proof is a one-line application of the TT-specialized density identity.
Claim. Let $H$ be a $4\times 4$ real matrix and $k,x\in\mathbb{R}^4$. If $H$ is transverse-traceless relative to $k$, then the Einstein-Hilbert second-variation density of the real cosine wave $h(y)=H\cos(k\cdot y)$ at the point $x$ equals the phase-only density of $(H,k)$ evaluated at phase $k\cdot x$.
background
This module (Arc 2, step 7) derives the continuum number that the Einstein-Hilbert action assigns to a real transverse-traceless plane wave, in the same convention as the banked Regge midpoint dictionary. Coordinates are points $x\in\mathbb{R}^4$ (abbrev Pt), and the plane-wave phase is the scalar $k\cdot x$. The discrete side averages $d^2/dt^2$ of the Regge action under $h(x)=H\cos(k\cdot x)$; the continuum object matched here is the phase average, per unit volume, of $d^2/dt^2\int R\sqrt{g}$ under that same real cosine wave (not the quadratic Taylor coefficient, which differs by another factor of 2).
The second-variation density is built from the linearized Levi-Civita connection $\Gamma^{(1)}{\lambda\mu\nu}=\tfrac12(\partial\mu h_{\lambda\nu}+\partial_\nu h_{\lambda\mu}-\partial_\lambda h_{\mu\nu})$. Under the transverse-traceless hypothesis on $(k,H)$, that density depends on $x$ only through the phase $k\cdot x$. The companion map packages the same expression as a function of a single real phase variable, so pointwise evaluation and phase-only evaluation can be identified.
proof idea
One-line term proof: apply the already-proved TT identity that rewrites the second-variation density under IsTT k H as the phase-only density at phase k x. No further algebraic expansion is done here; the work lives in that upstream TT reduction.
why it matters
This factorization is the first conjunct of ehFace_eq_average_of_density, which states both the pointwise equality and that the continuum EH face equals the phase average of the phase-only density. That pair is the bridge from local curvature calculus to the single number compared against the Regge dictionary in the separate non-circular module ReggeNormalizationDerived4D.
The module exists because the frozen preflight factor of 2 in the discrete bookkeeping had no derivation; step 6 ruled out the cheap Frobenius-square explanation, so the continuum side must be derived independently from Levi-Civita alone. Factoring density through phase is the structural step that lets the face become a pure phase average with no leftover $x$-dependence, which is what the discrete unit-cell average is measuring. It sits in the gravity analysis chain that pins the continuum TT second variation before any coupling-table or Bloch-symbol import can bias the answer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.