phaseAverage
plain-language theorem explainer
Defines the normalized mean of a real function over one full phase period [0, 2π]. Continuum gravity analysts cite it when converting a phase-dependent second-variation density into a unit-volume face coefficient under a real cosine wave. The body is the standard interval integral scaled by 1/(2π).
Claim. For $f:\mathbb{R}\to\mathbb{R}$, the phase average is $\displaystyle \langle f\rangle_{\mathrm{ph}} := \frac{1}{2\pi}\int_0^{2\pi} f(\theta)\,d\theta$.
background
This module (Arc 2, step 7) derives the continuum Einstein-Hilbert second variation on a real transverse-traceless plane wave in 4D, matched to the discrete Regge midpoint convention. The discrete side averages $d^2/dt^2$ of the Regge action under $h(x)=H\cos(k\cdot x)$; the continuum object must therefore be a phase average of the same real cosine wave, not a complex quadratic Taylor coefficient.
The second-variation density depends on position $x$ only through the scalar phase $\theta=k\cdot x$. For nonzero wave covector, the spatial mean over a large box therefore collapses to a pure average over one period in $\theta$. That average is exactly this definition: the $L^1$ mean of a phase function on $[0,2\pi]$ with the conventional $1/(2\pi)$ normalization.
Sibling objects include the phase map, the density-of-phase factorization, and the face coefficient ehFace. Classical input A1 is the linearized Levi-Civita Christoffel symbol; nothing here imports the coupling table or preflight answers.
proof idea
Pure definition: one-line abbreviation of the normalized interval integral of $f$ from $0$ to $2\pi$. No lemmas are applied at the definition site. Downstream proofs unfold it and invoke interval-integral rules (constant factor pull-out, evaluation of $\int\cos^2$).
why it matters
This is the averaging primitive that turns a phase-local continuum density into the unit-volume face number compared against the banked Regge dictionary. Parent results include ehFace_eq_phaseAverage (P1: the derived face equals the phase average of the derived density), ehFace_eq_average_of_density, and the rigidity theorem ehFace_rigid (any constant prefactor forced through the average must be 1).
It also underwrites phaseAverage_cos_sq (mean square of a real cosine is $1/2$), which the module identifies as the entire content of the discrete side's explicit $1/2$ factor and one of the two factors of two Arc 2 has been unable to account for. Exact-side comparison theorems in EHSecondVariationExact4D (a3_agrees_with_exact, exact_average_eq_ehFace) route through the same average, so the continuum coefficient is pinned without circular import of the discrete answer.
In the broader Recognition gravity program this closes the non-circular continuum half of the TT second-variation normalization before the discrete bookkeeping factor is re-examined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.