phaseAverage_cos_sq

This module (Arc 2, step 7) derives, from the linearized Levi-Civita connection alone, the number that the Einstein-Hilbert action assigns to a real transverse-traceless plane wave, in the same convention as the banked Regge midpoint dictionary. The discrete Bloch symbol averages $d^2/dt^2$ of the Regge action under the real perturbation $h(x)=H\cos(k\cdot x)$; its explicit factor $1/2$ is the lattice average of $\cos(k\cdot m_e)\cos(k\cdot m_{e'})$, stated as "real-cos = (1/2) Re(complex)".

The continuum counterpart is the phase average of a density that depends on position only through the plane-wave phase $\theta=k\cdot x$. That average is defined by $$\mathrm{phaseAverage}(f)=\frac{1}{2\pi}\int_0^{2\pi} f(\theta),d\theta.$$ For a nonzero wave covector, the spatial mean over a large box reduces to this one-dimensional mean. The density of §5 is proportional to $\cos^2\theta$, so the mean square of cosine is the sole nontrivial average that must be evaluated.

Term-mode proof. Unfold the phase-average definition to expose the normalized integral over $[0,2\pi]$. Rewrite via the standard antiderivative identity for $\int\cos^2$ (Mathlib integral_cos_sq). Evaluate the resulting boundary expression at the endpoints: $\sin(2\pi)=\sin 0=0$ and $\cos(2\pi)=\cos 0=1$, so cross terms vanish. Finish with field_simp and ring to obtain the constant $1/2$. No geometric input enters; the result is pure real analysis.

This identity is the entire continuum content of the discrete side's explicit $1/2$, and one of the two factors of two that Arc 2 has been unable to account for. Downstream, ehFace_eq_phaseAverage (P1) rewrites the derived EH face as the phase average of the derived density by applying this lemma together with linearity of the average, then ringing. That step closes the chain from linearized Christoffel symbols to a single numerical face coefficient, still without importing the coupling table, Bloch symbol, or norm gate.

In the larger Arc 2 program the continuum face is later compared, in a separate non-circular module, against the frozen preflight value and the discrete bookkeeping factor of 2. Establishing that the cosine mean square really is $1/2$ pins half of that discrepancy to a classical Fourier fact rather than to a lattice artifact or a polarization-norm mismatch (already refuted at step 6).