SuperposedPotentialClosure

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

A closed-L² representative for the superposed potential field

This file passes from the Cauchy sequence of finite bad-component prefixes to the full superposed slope defect. The limit is kept in the canonical closed zero-trace potential subspace, identified almost everywhere with the raw superposition, and then represented using CoarseGraining's closed-range theorem on open cubes.

theorem Algsuperdiff.Section3.Provider.Affine.ae_tendsto_badFamilyPotentialApproximation {d : ℕ} [NeZero d] {M : ABKModel d} {m : ℤ} {E b : ℝ} {k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (hne : (Percolation.hsepSet M m E b omega).Nonempty) (p : HCPolySupport.Vec d) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)), Filter.Tendsto (fun (N : ℕ) => badFamilyPotentialApproximation M m E b k₀ omega N p x) Filter.atTop (nhds (superposedCompetitorSlope m (Whitney.whitneyScale M m E b k₀ omega) (Whitney.badFamily M m (Whitney.whitneyScale M m E b k₀ omega) omega) p x - p))

Almost every point of the open root cube eventually sees the exact full superposed slope defect in the finite Whitney-layer prefixes.

The full zero-trace potential theorem

theorem Algsuperdiff.Section3.Provider.Affine.potentialZeroTraceFieldOn_superposedCompetitorSlope_sub_badFamily {d : ℕ} {M : ABKModel d} {m : ℤ} {E b : ℝ} {k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (hne : (Percolation.hsepSet M m E b omega).Nonempty) (p : HCPolySupport.Vec d) : HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (x : HCPolySupport.Vec d) => superposedCompetitorSlope m (Whitney.whitneyScale M m E b k₀ omega) (Whitney.badFamily M m (Whitney.whitneyScale M m E b k₀ omega) omega) p x - p

The full bad-family superposed slope defect is a zero-trace potential field on the open root cube. The nonzero-dimension instance is derived from the model and is not exposed in the statement.