FiniteComponentPotential

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

Zero-trace potential for finite bad-component sums

This file packages the one-component result from ComponentPotentialBadFamily under finite summation. It is the finite approximation input for the closed-L² construction of the full superposed competitor.

theorem Algsuperdiff.Section3.Provider.Affine.potentialZeroTraceFieldOn_sum_globalCompetitorSlope_sub_badComponents {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) (A : Finset (Set (HCPolySupport.TriadicCube d))) (hA : ∀ C ∈ A, C ∈ badComponents (Whitney.badFamily M m (Whitney.whitneyScale M m E b k₀ omega) omega)) (p : HCPolySupport.Vec d) : HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (x : HCPolySupport.Vec d) => ∑ C ∈ A, (globalCompetitorSlope m (Whitney.simplexScale m (Whitney.whitneyScale M m E b k₀ omega) (componentWindowLayer m (Whitney.whitneyScale M m E b k₀ omega) C)) C p x - p)

A finite sum of actual bad-component slope defects is a zero-trace potential field on the open root cube. The nonzero-dimension instance needed by the component theorem is derived there from M.