exact_density_rigid
plain-language theorem explainer
Any constant rescaling of the exact transverse-traceless second-variation density fails the Einstein-Hilbert face average unless the constant is exactly one. Gravity analysts auditing the A3 normalization in the continuum TT coefficient chain would cite this. The argument factors the constant out of the phase average, substitutes the known TT average, and cancels the nonzero factor.
Claim. Let $m,c\in\mathbb{R}$ with $m\neq 0$. If the one-period phase average of $\theta\mapsto c\cdot\rho_{\mathrm{TT}}(m,\theta)$ equals $-(m/2)$, where $\rho_{\mathrm{TT}}$ is the exact TT second-variation density, then $c=1$.
background
This module sits in the continuum gravity analysis that checks step 7's input A3: the claim that the second $t$-derivative of $\int\sqrt{g},R$ equals $-\int h_{\mu\nu}G^{(1)\mu\nu}$. A3 fixes the overall normalization of the density and is the one place a hidden factor could still sit in the coefficient chain. The exact curvature computation itself remains DERIVED-UNFORMALIZED (symbolic algebra off Lean); the module works downstream of the closed form.
The phase average is the mean of a real function of the wave phase over one full period $[0,2\pi]$. For a nonzero wave covector, the large-box spatial average of a density that depends on position only through that phase reduces to this mean. The exact TT density $\rho_{\mathrm{TT}}(m,\theta)$ is the closed-form second variation density on the transverse-traceless sector; its phase average is already proved equal to $-(m/2)$, which is exactly the Einstein-Hilbert face value on the base TT witnesses.
Constancy of the phase average under constant multiplication is elementary: the constant factors out of the integral.
proof idea
Rewrite the hypothesis with phaseAverage_const_mul and exactDensityTT_average to obtain $c\cdot(-(m/2))=-(m/2)$. From $m\neq 0$ deduce $-(m/2)\neq 0$ by a short linear-arithmetic contradiction. Rewrite the right-hand side as $1\cdot(-(m/2))$ via one_mul, then apply right-cancellation of the nonzero factor to conclude $c=1$.
why it matters
The doc-comment states the point directly: rescaling the exact density by any $c\neq 1$ breaks agreement with the face, so the match is not a free normalization choice. In the module narrative this seals the A3 coefficient: once the exact TT average equals the derived Einstein-Hilbert face $-(1/4)\cdot|k|^2\cdot|H|_F^2$, no residual constant can be absorbed without spoiling the equality.
That matters for arc 2's continuum coefficient chain, where A1 (linearized Levi-Civita), A2 (linearized Ricci), and Regge normalization are already formalized, and A3 was the remaining normalization gate. Sibling results show the average equals the face, that A3's RHS tracks the exact LHS even off TT, and that a pure-trace decoy misses the face with opposite sign. This rigidity lemma is the algebraic lock on the TT match itself. No downstream consumers are wired yet; the lemma stands as a referee-facing non-degeneracy statement inside the EH second-variation package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.