phaseAverage_const_mul
plain-language theorem explainer
Constants factor out of the continuum phase average of a real scalar density on the circle. Anyone matching Einstein-Hilbert second-variation faces to discrete Regge symbols under real cosine waves cites this linearity. The proof unfolds the average to an interval integral, applies Mathlib's constant-factor rule, and finishes by ring.
Claim. For every real constant $c$ and every real function $f$ of phase, the phase average obeys $\langle \theta \mapsto c\, f(\theta)\rangle = c\,\langle f\rangle$.
background
This module (Arc 2, step 7) derives the continuum transverse-traceless second variation of $\int R\sqrt{g}$ in 4D from the linearized Levi-Civita connection alone, in the same real-cosine convention the banked Regge midpoint dictionary uses. The discrete symbol averages $d^2/dt^2$ of the Regge action under $h(x)=H\cos(k\cdot x)$; the continuum object is therefore the phase average of the corresponding EH density per unit volume, not the bare quadratic Taylor coefficient.
The phase average is the normalized integral of a real scalar function of the wave phase over one full period. Densities built from linearized Christoffel symbols, Frobenius squares of polarizations, and momentum squares are then averaged under that measure. Linearity in an overall real prefactor is the elementary integral identity needed before any cosine-square evaluation.
proof idea
Term-mode proof in three steps. Unfold the definition of the phase average to its interval-integral form. Rewrite by Mathlib's intervalIntegral.integral_const_mul, which pulls a real constant through the integral. Close with ring to match the scalar factor on the right-hand side.
why it matters
Feeds the local identity that the derived EH face equals the phase average of the derived density, and the rigidity lemma that any constant rescaling of that density must be $1$ if the face is to match. The same pull-out is used in the exact-density rigidity statement (rescaling the exact TT density by $c\neq 1$ breaks agreement with $-(m/2)$) and in the Lagrangian-route face comparison in the Regge normalization module.
Those parents sit on the continuum side of Arc 2's bookkeeping problem: the discrete gate had inserted an underived factor $2$ between a computed $-(1/8)$ and a frozen $-(1/4)$. Deriving the continuum face independently, with every average step proved, is what lets the comparison module decide which number is forced rather than chosen.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.