exactDensityLongitudinal_average
plain-language theorem explainer
The wavelength average of the exact second-variation density for a longitudinal metric perturbation is identically zero, for any real mass/momentum parameter. Gravity analysts cite it when separating TT Einstein-Hilbert face behaviour from pure-gauge or longitudinal decoys. The proof unfolds the density to the zero function and applies constant-phase averaging.
Claim. For every real parameter $m$, the one-wavelength phase average of the exact second-variation density of a longitudinal perturbation equals $0$.
background
This module sits in the gravity analysis arc that checks step 7's continuum Einstein-Hilbert face $-(1/4)\cdot|k|^2\cdot|H|F^2$. Three inputs (linearized connection, linearized Ricci, Regge normalization) are formalized; A3, equating $d^2/dt^2\int\sqrt{g}R$ to $-\int h{\mu\nu}G^{(1)\mu\nu}$, was used without derivation and fixes overall density normalization.
An external exact (non-linearized) computation of $\sqrt{\det g},R$ for $g_{\mu\nu}(t)=\delta_{\mu\nu}+t H_{\mu\nu}\cos(\kappa z)$ supplies closed-form densities. Those densities are banked here as functions of phase; phaseAverage is their mean over one wavelength. The longitudinal density is the constant zero function of phase (unlike TT, whose average is $-\kappa^2/2$, or pure trace, whose average is $+\kappa^2/2$).
Sibling averages (exactDensityTT_average, exactDensityTrace_average) and the constant-average lemma phaseAverage_const are the local toolkit. The face itself depends on the polarization only through Frobenius square.
proof idea
Term-mode, two steps. Unfold exactDensityLongitudinal to expose that it is the constant function $0$ of phase. Then simpa applies phaseAverage_const at $0$, so the wavelength average is $0$. No curvature identities are re-proved here; the closed form is taken as given from the external exact script and only averaged.
why it matters
Feeds longitudinal_decoy_misses_the_face, which shows that a longitudinal polarization with nonzero Frobenius square and nonzero wave covector has vanishing exact average, while the derived EH face is nonzero. That mismatch is intentional: the face formula is TT-specific, and a formula that also fit longitudinal or pure-trace witnesses would be fitting nothing.
In the module's arc, this closes the longitudinal half of the decoy pair (with the trace decoy) that certifies A3's right-hand side and the face coefficient against non-TT probes. It does not formalize the exact curvature algebra itself (still tagged DERIVED-UNFORMALIZED); it only propagates the banked longitudinal closed form into the average that the face comparison needs. Framework role: coefficient hygiene on the continuum EH face used in the gravity side of the Recognition chain, not a T0-T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.