exactDensityTT_average

This module closes the normalization gap left by step 7 of the continuum TT second-variation analysis. Step 7 derived the Einstein–Hilbert face $-(1/4),|k|^2|H|F^2$ from four inputs; three are formalized, but A3 (that $d^2/dt^2\int\sqrt{g},R=-\int h{\mu\nu}G^{(1)\mu\nu}$) was only stated. Off-Lean symbolic algebra produced a closed-form exact density on the metric family $g(t)=\delta+t H\cos(\kappa z)$.

The exact TT density (plus and cross polarizations, Frobenius square 2) is $m(7\sin^2\theta-4)$, with $m$ standing for the squared wave covector. The phase average is the mean of a phase function over one period: $(1/(2\pi))\int_0^{2\pi}f(\theta),d\theta$. Because every exact density below is affine in $\sin^2\theta$, the lemma that averages $a\sin^2\theta+b$ to $a/2+b$ is the computational engine.

Rewrite the exact TT density pointwise as $(7m)\sin^2\theta+(-4m)$ by unfolding the definition and ringing. Substitute into the phase average and apply the affine sin-square average lemma, which returns $(7m)/2+(-4m)$. A final ring step collapses that expression to $-m/2$.

This is the arithmetic hinge between the exact closed-form density and the continuum face. The parent theorem exact_average_eq_ehFace rewrites with this identity, unfolds the face, inserts Frobenius square 2, and rings to equality: the wavelength average of the exact second variation equals step 7's derived Einstein–Hilbert face, with no linearization on the left-hand side. The rigidity theorem then uses the same average to show that any constant rescaling $c\neq 1$ of the exact density breaks the match, so the normalization is forced rather than free. Within the gravity arc this pins A3's overall coefficient for TT waves and feeds the claim that the continuum face is not an artefact of linearization.