ComponentPotentialBadFamily #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Zero-trace potential for an actual bad-family component #
This file specializes the generic finite-root-mesh potential theorem to one
component of the Section 3 bad family. All window hypotheses are discharged
by badComponents_window_badFamily, and the standing nonzero-dimension
instance is derived internally from the model.
theorem
Algsuperdiff.Section3.Provider.Affine.potentialZeroTraceFieldOn_globalCompetitorSlope_sub_badComponent
{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)
{C : Set (HCPolySupport.TriadicCube d)}
(hCmem : 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) =>
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
One actual bad component supplies a public zero-trace potential field.
The [NeZero d] instance used by the finite Kuhn analysis is derived from the
model's standing dimension assumption and is not a theorem binder.