exactDensityTrace
plain-language theorem explainer
Closed-form exact second-variation density for a transverse pure-trace metric perturbation of Frobenius square 2: mass times sin-squared of the wave phase. Gravity analysts cite it when checking that the Einstein-Hilbert face is TT-specific, not a mass-2 artefact. The declaration is a one-line algebraic definition, not a derived identity.
Claim. For a mass parameter $m\in\mathbb{R}$ and wave phase $\theta\in\mathbb{R}$, the exact second-variation density of $\int\sqrt{g}\,R$ on a transverse pure-trace perturbation of Frobenius square 2 is $m\sin^2\theta$.
background
This module sits in the continuum check of step 7's coefficient chain for the Einstein-Hilbert second variation. 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 in ContinuumTTSecondVariation4D without a Lean derivation. Off-Lean symbolic algebra supplies exact densities for the family $g_{\mu\nu}(t)=\delta_{\mu\nu}+t H_{\mu\nu}\cos(\kappa z)$ in 4D Euclidean signature.
The transverse-traceless plus and cross polarizations average to the derived face $-(1/4)|k|^2|H|_F^2$. A transverse pure trace carries the same Frobenius square 2 and the same wavevector, but different physics: its exact density is the present formula. Wavelength averages are taken via the module's phase-average operator over one period of the standing wave.
proof idea
Pure definition: the body is the closed form $m\sin^2\theta$ taken from the external exact-curvature computation. No tactics, no lemmas, no expansion in the deformation parameter. Downstream theorems unfold this name and rewrite against the affine phase-average identity for $\sin^2$.
why it matters
Parent results are exactDensityTrace_average (wavelength mean equals $m/2$) and trace_decoy_misses_the_face, whose doc states that the pure-trace average has the opposite sign from the EH face, so agreement of exact averages with the face is a TT statement, not a claim about every mass-2 perturbation. That decoy is the module's main conceptual payoff: it shows the face formula cannot be an accidental fit to Frobenius mass alone. Within the broader RS gravity arc this pins the normalization of the continuum second-variation density used when matching discrete recognition weights to continuum GR, without claiming a formalized proof of A3 itself (still tagged DERIVED-UNFORMALIZED).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.