phaseAverage_sin_sq
plain-language theorem explainer
The period mean of sin squared equals one half. Continuum gravity arguments that compare the quadratic-Lagrangian second-variation density to the Einstein-Hilbert face cite this elementary integral. The proof unfolds the 2π average, inserts the closed-form integral of sin squared, clears boundary sines, and finishes by field arithmetic.
Claim. The mean of $\sin^2\theta$ over one full period is one half: $\frac{1}{2\pi}\int_0^{2\pi}\sin^2\theta\,d\theta = \frac{1}{2}$.
background
In the continuum transverse-traceless second-variation setup, plane-wave densities depend on position only through the phase $\theta=k\cdot x$. Their spatial mean over a large box therefore reduces to the period mean
$$\mathrm{phaseAverage}(f)=\frac{1}{2\pi}\int_0^{2\pi} f(\theta),d\theta.$$
This module sits in Arc 2, step 7: it places the continuum face $ehFace,H,k=-(1/4)|k|^2|H|F^2$ beside the banked dictionary and isolates Regge's normalization $\rho$ in $\sum_h A_h\delta_h=\rho\int R\sqrt{g}$. Section 7 opens a second textbook route. The quadratic Lagrangian $-(1/4)\partial\lambda h_{\mu\nu}\partial^\lambda h^{\mu\nu}$ yields a density in $\sin^2$ rather than $\cos^2$. The two densities differ pointwise by a total derivative and must agree after averaging; that agreement checks A3's normalization.
Upstream, the continuum phase and its average are defined in ContinuumTTSecondVariation4D; the eight-tick foundation supplies discrete phases $k\pi/4$, but the average used here is the continuum $2\pi$ integral.
proof idea
Short term-mode proof. Record $\pi\neq 0$, unfold the period-mean definition, and rewrite by the closed-form integral of $\sin^2$ on $[0,2\pi]$ together with $\sin(2\pi)=0$ and $\sin 0=0$. Then field_simp clears the remaining factor $2\pi$, and ring reduces the expression to $1/2$. A parallel proof lives in EHSecondVariationExact4D with a slightly broader trig simp set; the algebraic content is identical.
why it matters
Direct input to lagrangian_route_same_face, which shows that averaging the quadratic-Lagrangian density recovers the same continuum face already obtained from the Einstein-Hilbert second variation. Agreement of the two independent textbook forms is the module's consistency check on A3's normalization.
In the Arc 2 narrative that check helps pin Regge's constant at $\rho=1/2$ (so the discrete bookkeeping factor is $2=1/\rho$). The historical factor-of-two gap between continuum $-(1/8)$ and the frozen $-(1/4)$ is thereby read as a difference of functionals, not an error on the Regge side. The result is pure calculus, but it sits on the continuum bridge between the simplicial ledger and the Einstein-Hilbert action that the gravity analysis uses throughout.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.