phaseAverage_sin_sq
plain-language theorem explainer
The wavelength mean of sin²θ over one full period equals 1/2. Anyone reducing a phase-dependent continuum second-variation density to a constant Einstein-Hilbert face cites this identity. The proof unfolds the period mean, substitutes the closed antiderivative of sin², evaluates the trig boundary terms, and finishes by field arithmetic.
Claim. The period mean $\frac{1}{2\pi}\int_0^{2\pi}\sin^2\theta\,d\theta$ equals $\tfrac{1}{2}$.
background
In the continuum TT second-variation setup, every exact density depends on position only through a phase $\theta=\kappa z$ (or more generally $\mathrm{phase},k,x$). The spatial box average for a nonzero wave covector therefore collapses to the period mean
$$\mathrm{phaseAverage}(f)=\frac{1}{2\pi}\int_0^{2\pi} f(\theta),d\theta.$$
This module sits in the arc that checks step 7's coefficient A3 for the Einstein-Hilbert second variation: the exact $d^2/dt^2$ of $\sqrt{g},R$ along $g=\delta+t H\cos(\kappa z)$, after wavelength averaging, must match the derived face $-\tfrac14|k|^2|H|_F^2$. Every such exact density is of the affine shape $a\sin^2\theta+b$, so the pure $\sin^2$ average is the elementary building block.
Upstream, phaseAverage is defined exactly as the normalized integral above; the companion identity for constants is already available as a sibling.
proof idea
Tactic proof. Record $\pi\neq 0$, unfold the period-mean definition, rewrite by the closed-form integral of $\sin^2$ on $[0,2\pi]$, then simplify the resulting boundary values ($\sin 2\pi=\sin 0=0$, $\cos 2\pi=\cos 0=1$, zero products and cancelling differences). Finish with field_simp and ring to obtain $1/2$.
why it matters
This is the elementary average that turns every exact second-variation density of shape $a\sin^2\theta+b$ into a pure number comparable to the continuum Einstein-Hilbert face. Downstream it is applied inside lagrangian_route_same_face, which shows that the phase average of the Lagrangian density equals ehFace, and it is re-used by the parallel statement in ReggeNormalizationDerived4D. Together with the affine extension, it closes the Lean half of the A3 check: once the closed-form density is granted (still DERIVED-UNFORMALIZED off-kernel), its wavelength mean is proved equal to the face that step 7 derived from A1–A3 and Regge normalization. No Recognition forcing landmark (T5–T8, RCL) is touched; the result is pure analysis supporting the gravity coefficient chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.