exactDensityLongitudinal
plain-language theorem explainer
The exact second-variation density of the Einstein-Hilbert integrand on a unit-Frobenius longitudinal metric perturbation is identically zero at every wave number and phase. Analysts comparing the continuum EH face against non-TT decoys cite this closed form. It is a constant definition that records the off-Lean symbolic result that pure longitudinal modes contribute nothing at second order.
Claim. The exact second-variation density of $\int \sqrt{g}\,R$ on a longitudinal perturbation of Frobenius square $1$ is the zero function of wave number and phase: $\rho_{\mathrm{long}}(m,\theta)=0$ for all real $m$ and $\theta$.
background
This module records closed-form exact second-variation densities of the Einstein-Hilbert integrand $\int\sqrt{g},R$ in four Euclidean dimensions, for the metric family $g_{\mu\nu}(t)=\delta_{\mu\nu}+t H_{\mu\nu}\cos(\kappa z)$. The densities come from a full (unexpanded) curvature computation off Lean; the module then proves, in Lean, what those closed forms imply for wavelength averages and for the continuum face formula.
Step 7 of the continuum chain derived the Einstein-Hilbert face $-(1/4)\cdot|k|^2\cdot|H|F^2$ under four inputs. Three are formalized; the fourth (A3: $d^2/dt^2\int\sqrt{g},R=-\int h{\mu\nu}G^{(1)\mu\nu}$) fixes overall normalization and was only stated in ContinuumTTSecondVariation4D. Exact checks show A3 holds on TT and non-TT witnesses alike, while the face itself is TT-specific.
A longitudinal polarization (momentum-aligned, Frobenius square 1) is the purest non-TT decoy: same wave support as the TT cases, but no transverse-traceless content. Its exact density vanishes pointwise.
proof idea
Definitional constant: the body is the real zero, independent of the unused wave-number and phase arguments. No lemma applications and no tactics; the mathematical content is the assertion that the exact density is the zero function.
why it matters
The definition is the longitudinal witness in the exact-density triple (TT, pure trace, longitudinal). Its wavelength average is immediately zero via the constant-average lemma, and that average feeds longitudinal_decoy_misses_the_face: for any matrix with Frobenius square 1 and any nonzero momentum, the phase average of this density is not equal to the continuum EH face. Downstream doc-comment: "The longitudinal perturbation has vanishing exact second variation, which the face formula does not report for a nonzero polarization."
Together with the pure-trace decoy (average $+\kappa^2/2$, opposite sign to the face), this pins that the face $-(1/4)\cdot|k|^2\cdot|H|_F^2$ is TT-specific rather than a universal second-variation identity. That specificity is required if A3 and the face are both to survive as the normalization step in arc 2's coefficient chain. The underlying curvature algebra remains DERIVED-UNFORMALIZED; Lean only consumes the closed form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.