exactDensityTrace_average
plain-language theorem explainer
The wavelength average of the exact second-variation density on a transverse pure-trace perturbation of mass parameter m equals m/2. Gravity analysts cite it to show that the Einstein-Hilbert face formula is TT-specific: the pure-trace decoy has the same Frobenius square 2 yet averages to the opposite sign. The proof rewrites the density as an affine sin-squared profile and applies the elementary phase-average identity.
Claim. For every real mass parameter $m$, the one-period phase average of the exact second-variation density on a transverse pure-trace perturbation equals $m/2$. Explicitly, if the density is $\theta \mapsto m\sin^2\theta$, then $\frac{1}{2\pi}\int_0^{2\pi} m\sin^2\theta\,d\theta = m/2$.
background
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)\cdot|k|^2\cdot|H|F^2$ from four inputs; A3 (that $d^2/dt^2\int\sqrt{g}R=-\int h{\mu\nu}G^{(1)\mu\nu}$) was used but not derived in Lean. Off-Lean symbolic algebra supplies closed-form exact densities for three base polarizations; this file proves everything downstream of those closed forms.
phaseAverage is the mean of a phase function over one period $[0,2\pi]$, the continuum stand-in for a large-box spatial average when the density depends on position only through the wave phase. exactDensityTrace m is the exact second-variation density on a transverse pure-trace perturbation of Frobenius square 2: $\theta\mapsto m\sin^2\theta$. Same mass and wave as the TT plus mode, different physics.
The elementary identity phaseAverage_sin_sq_affine states that the average of $a\sin^2\theta+b$ is $a/2+b$; every exact density in the module has that shape.
proof idea
Rewrite exactDensityTrace m pointwise as the affine profile $\theta\mapsto m\sin^2\theta+0$ by unfolding the definition and ringing. Substitute into phaseAverage and apply phaseAverage_sin_sq_affine with coefficients $a=m$, $b=0$, which yields $m/2+0$. A final ring closes the equality. No integration is redone; the work is the affine reduction plus the already-proved sin-squared average.
why it matters
Feeds trace_decoy_misses_the_face, which shows that a transverse pure-trace perturbation with the same Frobenius square 2 and the same wave has exact average of opposite sign from the Einstein-Hilbert face. Downstream doc: the face equality is therefore a statement about transverse-traceless data, not about every perturbation of mass 2. Without this average, the decoy comparison cannot fire.
In the broader arc, the module confirms that the continuum face coefficient used in the gravity chain is not an artefact of a hidden normalization in A3: the exact density averages match the derived face on TT modes and deliberately miss it on the pure-trace decoy. That pins the overall factor in the continuum second-variation density before it is handed to discrete or Recognition-side gravity arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.