phaseAverage_const
plain-language theorem explainer
The wavelength (phase) average of a constant real function equals that constant. Gravity analysts cite it when reducing exact second-variation densities that happen to be constant in the phase variable. The proof unfolds the mean-over-[0,2π] definition, applies the constant-integral rule, and clears the normalizing factor 1/(2π).
Claim. For every real constant $c$, the phase average $\frac{1}{2\pi}\int_0^{2\pi} c\,d\theta$ equals $c$.
background
In the continuum TT second-variation analysis, densities along a monochromatic wave depend on position only through the phase $\theta = k\cdot x$. The spatial mean over a large box therefore collapses to the one-period mean
$$\mathrm{phaseAverage}(f) := \frac{1}{2\pi}\int_0^{2\pi} f(\theta),d\theta.$$
This module sits in the exact Einstein-Hilbert second-variation check for step 7's coefficient A3: after an off-Lean symbolic computation produces closed-form densities (TT, pure trace, longitudinal), Lean only has to average those closed forms and compare them to the derived face $-\frac14|k|^2|H|_F^2$. Constant densities appear as the longitudinal case (identically zero) and as intermediate reductions.
proof idea
Unfold phaseAverage. The integrand is the constant function $c$, so intervalIntegral.integral_const gives $\int_0^{2\pi} c,d\theta = (2\pi-0)\cdot c$. After rewriting scalar multiplication as ordinary multiplication and simplifying $2\pi-0$, field_simp cancels the prefactor $1/(2\pi)$ against $2\pi$, using $\pi\neq 0$. The result is $c$.
why it matters
Feeds exactDensityLongitudinal_average, which shows that the exact longitudinal second-variation density averages to zero. That zero is part of the module's comparison suite: TT averages match the Einstein-Hilbert face, while non-TT witnesses (pure trace opposite sign, longitudinal vanishing) confirm the face is TT-specific and that A3 is not an artefact of the TT reduction. In the broader Recognition gravity arc, this is bookkeeping on the coefficient chain that pins the continuum EH face used downstream of the forcing landmarks (eight-tick structure, $D=3$), not a new physical input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.