exactDensityTT

Step 7 of the continuum gravity arc derives the Einstein-Hilbert face $-(1/4)\cdot|k|^2\cdot|H|F^2$ from four inputs. Three (linearized connection, linearized Ricci, Regge normalization) are formalized; the fourth, A3, equates $d^2/dt^2\int\sqrt{g}R$ to $-\int h{\mu\nu}G^{(1)\mu\nu}$ and fixes overall density normalization. That identity was checked off Lean by exact symbolic differentiation of the full curvature for the family $g_{\mu\nu}(t)=\delta_{\mu\nu}+t H_{\mu\nu}\cos(\kappa z)$ in four Euclidean dimensions.

On plus and cross polarizations (both TT with $|H|_F^2=2$), the exact density before wavelength averaging is $\kappa^2(7\sin^2(\kappa z)-4)$. The parameter $m$ here is the squared wave momentum $\kappa^2$. The same mass and wave on a transverse pure-trace perturbation yield a different density, so the face formula is polarization-specific.

This module does not re-derive the curvature algebra in Lean; it imports the closed form and proves everything downstream of it (averages, agreement with the face, rigidity).

Bare definition: the body is the arithmetic expression $m(7\sin^2\theta-4)$. No tactics, no lemmas. Downstream theorems rewrite it into an affine combination of $\sin^2$ and a constant, then apply the phase-average lemmas for those building blocks.

This density is the left-hand side that makes the continuum coefficient chain checkable. Its wavelength average equals the derived Einstein-Hilbert face (exact_average_eq_ehFace), so A3's right-hand side matches the exact left-hand side at the TT witness (a3_agrees_with_exact). Rescaling by any $c\neq 1$ breaks the match (exact_density_rigid), so the coefficient is not a free normalization. The sibling pure-trace density has the opposite average sign, confirming the face is TT-specific rather than a universal fit. Within Recognition Science gravity, this closes the last soft spot in arc 2's continuum face before the discrete-to-continuum bridge is trusted.