HomSeamGaugeCongruence #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The multiscale clause's `∀ G` slot: the gauge is an a.e. functional #

What this file supplies #

The energy residue's multiscale conjunct is quantified over EVERY field G that agrees with ∇u − ∇v on the open cube:

  ∀ G, (∀ x ∈ □_m, G x = ∇u x − ∇v x) → CoarseGrainingFinitePMultiscale … G F.

The quantifier is FREE. The multiscale clause reads its gradient slot only through the depth gauge, which reads it only through the cell averages (G)_R of the grid descendants R ⊆ □_m, and the cube average is an a.e. functional of its integrand. So the whole ∀ G family collapses onto ONE representative — the canonical fun x => u.grad x - v.grad x.

The congruence below is that collapse, stated in exactly the shape the supply's clause slot asks for.

1. The cube average is an a.e. functional #

source

theorem Algsuperdiff.Section4.Provider.Homogenization.cubeAverageVec_congr_of_eqOn_openCube {d : ℕ} {Q R : HCPolySupport.TriadicCube d} {j : ℕ} (hR : R ∈ HCPolySupport.descendantsAtDepth Q j) {G G' : HCPolySupport.Vec d → HCPolySupport.Vec d} (hG : ∀ x ∈ HCPolySupport.openCubeSet Q, G x = G' x) :

HCPolySupport.cubeAverageVec R G = HCPolySupport.cubeAverageVec R G'

THE CELL AVERAGE OF A DESCENDANT IS BLIND TO THE PARENT'S NULL SETS.

If two fields agree pointwise on the OPEN parent cube, then every grid descendant's cell average agrees. This is the only way the finite-p gauge touches its field.