densityOfPhase
plain-language theorem explainer
Phase-only continuum density of the Einstein–Hilbert second variation on a real transverse-traceless cosine wave: −½ |k|² ‖H‖_F² cos²θ. Gravity analysts cite it when forming the continuum face by phase average or when comparing continuum and Regge densities pointwise. It is a pure definitional rewrite of the §5 density in phase coordinates.
Claim. For a $4\times 4$ polarization matrix $H$, wave covector $k\in(\mathbb{R}^4)^*$, and phase $\theta\in\mathbb{R}$, define the phase-only density $$\rho(H,k,\theta)=-\tfrac12\,|k|^2\,\|H\|_F^2\cos^2\theta,$$ where $|k|^2=\sum_i k_i^2$ and $\|H\|_F^2=\sum_{ij}H_{ij}^2$.
background
This module (Arc 2, step 7) derives, from the linearized Levi-Civita connection alone, the continuum second variation of $\int R\sqrt{g}$ on a real transverse-traceless plane wave in 4D, in the same convention as the banked Regge midpoint dictionary. It imports only Mathlib and edge TT linear algebra, so the continuum coefficient is independent of the discrete side.
The discrete Bloch symbol averages $d^2/dt^2$ of the Regge action under $h(x)=H\cos(k\cdot x)$. Matching that convention, the continuum object is the phase average of the second-variation density per unit volume under the same real cosine wave (not the quadratic Taylor coefficient, which differs by another factor of 2).
Here $k$ is a point of type $\mathrm{Pt}=\mathrm{Fin},4\to\mathbb{R}$, $\mathrm{momentumSq},k=\sum_i k_i^2$, and $\mathrm{frobSq},H=\sum_{ij}H_{ij}^2$ is the Frobenius square restated locally so the module never imports the Regge side.
proof idea
Definitional. The body is the closed-form expression $-\tfrac12,(\mathrm{momentumSq},k),(\mathrm{frobSq},H),\cos^2\theta$, packaging the §5 density as a function of phase alone. No lemmas or tactics.
why it matters
This is the density that the continuum face averages. Downstream, density_factors_through_phase identifies the spacetime density with this phase form under the TT hypothesis; ehFace_eq_phaseAverage (P1) proves the derived face equals the phase average of this density, with every step from Levi-Civita proved above; ehFace_rigid shows no free constant can rescale it and still match the face.
Cross-module, a3_agrees_with_exact checks that the exact TT density and this phase density share the same wavelength average (so the step-7 RHS did not move the coefficient), while two_routes_differ_pointwise shows the continuum and Lagrangian/Regge phase densities disagree at $\theta=0$ and agree only after averaging—making that agreement informative rather than tautological. Together they close the non-circular continuum half of the Regge normalization comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.