AveragingUniform

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Uniform-constant grid-phase averaging

The shared proof of exists_gridPhase_meanSq_le_uniform lives in Corridor/PhaseComparison/Averaging.lean. The existential interface specializes its field-independent constant. This module preserves the public import path for consumers of the uniform theorem.