GlobalSuperposition

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

The multi-component competitor: superposition over the components of ℐ

GlobalCompetitor.lean builds, for one bad family C, the competitor ℓ̂_p^C = globalCompetitor m s C p on the uniform scale-s Kuhn mesh of the root cube, at that family's own common coarse scale s = simplexScale m hn j, and proves the three sum_of_a_decomp clauses at C. This module supplies a local bridge from that A to the consumer's badFamily-indexed clauses: the superposition over the distinct connected components of the bad family.

Which branch this follows, and why

Define the global modified affine by assigning the vertex data once on the > full simplex complex, or superpose the component corrections while > allowing overlap on good cubes. [.] In the latter presentation one must > retain a uniform overlap multiplicity (or merge components whose collars > overlap) in the gradient and energy constants.

(The multiplicity obligation of the second sentence belongs to the summed gradient estimate and is deliberately deferred — see the Scope section; quotation expanded.)

The first branch is dissolved at the vertex-datum level by CompetitorVertexData.lean (claimedBadComponent_eq_badComponent: at most one component ever claims a vertex).

This module therefore follows the second branch (its construction clause verbatim; its multiplicity clause deferred as noted above): it superposes the per-component corrections, each built on its own component mesh at its own common coarse scale, and it allows them to overlap on good cubes. Nothing below asserts, or uses, any disjointness of the collars 𝒩(𝒞); the pointwise "at most one nonzero summand" property of the vertex datum is not lifted to the function level and is not needed.

the neighborhood of one component does not contain a bad cube belonging to another component

which is notMem_whitneyNeighborhood_of_ne below (two lines from BadChain maximality), and which is exactly what clause 1 needs. Clause 3 needs only the monotonicity 𝒞 ⊆ ℐ ⟹ 𝒩(𝒞) ⊆ 𝒩(ℐ).

Scope: what this module does NOT do

• Consequently nothing below identifies superposedCompetitorSlope with a distributional gradient; as in GlobalCompetitor.lean the field is a defined piecewise-constant object and the three clauses are statements about it. e.hat.linear.1 (the H¹₀ leg) and the hF/hG binders of sum_of_a_decomp are untouched.
• No gradient estimate. The summed active-component replacement for the false component-local gradient bound is read and not consumed: no diameter, no overlap count and no constant occurs below.
• The two-layer window per component is a hypothesis (hwin), exactly as in CommonCoarseMesh.lean and GlobalCompetitor.lean — but unlike there it is discharged in this file at the manuscript's own bad family (badComponents_window_badFamily).
• No three-layer window is used; no face-to-face property of SW(□_m) is used.

References

• ABK26, (l.piecewise.affine.approx, e.hat.linear.properties; clause 1, clause 3), (the false disjointness), (Step 1), (ℐ, 𝒩(𝒥)), (the components), (l.bad.clusters.geometry clause (1)), (ℓ_e).
• Its subtype index on the bad components, and its local-finiteness and continuity endpoints, have no counterpart here: the components are indexed by the sets themselves and no local finiteness is used.

The connected components of the bad family

def Algsuperdiff.Section3.Provider.Affine.badComponents {d : ℕ} (I : Set (HCPolySupport.TriadicCube d)) : Set (Set (HCPolySupport.TriadicCube d))

The 2-connected components of ℐ, presented as the set of subfamilies of the form badComponent ℐ □. Distinct bad cubes of one component give the same member of this set, so it is the component set, not a list with repetitions.

Equations

• Algsuperdiff.Section3.Provider.Affine.badComponents I = {C : Set (HCPolySupport.TriadicCube d) | ∃ Q ∈ I, C = Algsuperdiff.Section3.Provider.Whitney.badComponent I Q}

theorem Algsuperdiff.Section3.Provider.Affine.badComponent_mem_badComponents {d : ℕ} {I : Set (HCPolySupport.TriadicCube d)} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ I) : Whitney.badComponent I Q ∈ badComponents I

theorem Algsuperdiff.Section3.Provider.Affine.badComponents_subset {d : ℕ} {I C : Set (HCPolySupport.TriadicCube d)} (hC : C ∈ badComponents I) : C ⊆ I

theorem Algsuperdiff.Section3.Provider.Affine.badComponent_eq_of_badChain {d : ℕ} {I : Set (HCPolySupport.TriadicCube d)} {A B : HCPolySupport.TriadicCube d} (h : Whitney.BadChain I A B) : Whitney.badComponent I A = Whitney.badComponent I B

Chain-joined bad cubes have the same component.

theorem Algsuperdiff.Section3.Provider.Affine.notMem_whitneyNeighborhood_of_ne {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {I C : Set (HCPolySupport.TriadicCube d)} (hC : C ∈ badComponents I) {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ I) (hne : C ≠ Whitney.badComponent I Q) : Q ∉ Whitney.whitneyNeighborhood m hn C

Overlap safety on the bad cubes — the fact isolates as "what does follow directly from maximality": a bad cube of one component lies off the touching neighborhood of every other component. Two cubes at distance zero are one chain step apart, so a bad cube in 𝒩(𝒞) is chain-joined to 𝒞 and therefore belongs to it.

This is the only disjointness this file uses: the good-cube collars 𝒩(𝒞) are not assumed disjoint anywhere.

theorem Algsuperdiff.Section3.Provider.Affine.whitneyNeighborhood_mono {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {J J' : Set (HCPolySupport.TriadicCube d)} (h : J ⊆ J') : Whitney.whitneyNeighborhood m hn J ⊆ Whitney.whitneyNeighborhood m hn J'

The touching neighborhood is monotone in the family.

The per-component window

noncomputable def Algsuperdiff.Section3.Provider.Affine.componentWindowLayer {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (C : Set (HCPolySupport.TriadicCube d)) : ℕ

The anchor layer of a component: the least Whitney layer met by the component's touching neighborhood — not by the component itself. The component's common coarse mesh is simplexScale m hn (componentWindowLayer m hn C).

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Affine.step_of_monotone {hn : ℕ → ℕ} (hmono : Monotone hn) (k : ℕ) : hn k ≤ hn (k + 1) + 1

Monotone hn implies the e.SW.def transcription guard of SimplexPartition.lean.

The superposed competitor and its gradient field

noncomputable def Algsuperdiff.Section3.Provider.Affine.superposedCompetitorSlope {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (I : Set (HCPolySupport.TriadicCube d)) (p : HCPolySupport.Vec d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The piecewise-constant gradient field of the superposition, p + Σ_𝒞 (∇ℓ̂_p^𝒞 − p). As in GlobalCompetitor.lean this is a defined field; its identification with a distributional gradient of superposedCompetitor is not proved and is used nowhere.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Affine.superposedCompetitorCellSlope {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (I : Set (HCPolySupport.TriadicCube d)) (p : HCPolySupport.Vec d) (T : Whitney.KuhnCell d) : HCPolySupport.Vec d

The cell constant of the superposed field on a cell of SW(□_m), read at the cell's interior point exactly as globalCompetitorCellSlope is.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Affine.superposedCompetitorCellSlope_eq_sum {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (I : Set (HCPolySupport.TriadicCube d)) (p : HCPolySupport.Vec d) (T : Whitney.KuhnCell d) : superposedCompetitorCellSlope m hn I p T = p + ∑ᶠ (C : Set (HCPolySupport.TriadicCube d)) (_ : C ∈ badComponents I), (globalCompetitorCellSlope m (Whitney.simplexScale m hn (componentWindowLayer m hn C)) C p T - p)

The sum_of_a_decomp clauses at the full bad family

theorem Algsuperdiff.Section3.Provider.Affine.superposedCompetitorSlope_eq_cellSlope {d : ℕ} [NeZero d] {m : ℤ} {hn : ℕ → ℕ} (hmono : Monotone hn) {I : Set (HCPolySupport.TriadicCube d)} (hI : I ⊆ Whitney.whitneyPartition m hn) (hwin : ∀ C ∈ badComponents I, (Whitney.whitneyNeighborhood m hn C).Finite ∧ ∀ R ∈ Whitney.whitneyNeighborhood m hn C, R ∈ Whitney.whitneyLayer m hn (componentWindowLayer m hn C) ∨ R ∈ Whitney.whitneyLayer m hn (componentWindowLayer m hn C + 1)) (p : HCPolySupport.Vec d) {T : Whitney.KuhnCell d} (hT : T ∈ Whitney.simplexPartition m hn) : (∀ x ∈ T.openCarrier, superposedCompetitorSlope m hn I p x = superposedCompetitorCellSlope m hn I p T) ∧ (Multiscale.whitneyCubeOf m hn T ∈ I → superposedCompetitorCellSlope m hn I p T = 0) ∧ (Multiscale.whitneyCubeOf m hn T ∉ Whitney.whitneyNeighborhood m hn I → superposedCompetitorCellSlope m hn I p T = p)

The three sum_of_a_decomp clauses of the superposition, at one cell.

• the field is constant on the open cell — every summand is, by the corresponding clause at its own component;
• the constant is 0 when the cell's Whitney cube □ is bad: □ belongs to exactly one component 𝒞₀, whose correction contributes 0 − p, while every other component has □ ∉ 𝒩(𝒞) by notMem_whitneyNeighborhood_of_ne and contributes p − p = 0 — this is clause 1 of e.hat.linear.properties at the full family;
• the constant is p when □ lies off 𝒩(ℐ): then □ ∉ 𝒩(𝒞) for every component, and every summand is 0 — clause 3.

No disjointness of collars, no overlap count and no finiteness of the component family is used.

theorem Algsuperdiff.Section3.Provider.Affine.superposedCompetitor_decomp_clauses_badFamily {d : ℕ} [NeZero d] {m : ℤ} {hn : ℕ → ℕ} (hmono : Monotone hn) (M : ABKModel d) (omega : Cutoff.CutoffSample d) (hwin : ∀ C ∈ badComponents (Whitney.badFamily M m hn omega), (Whitney.whitneyNeighborhood m hn C).Finite ∧ ∀ R ∈ Whitney.whitneyNeighborhood m hn C, R ∈ Whitney.whitneyLayer m hn (componentWindowLayer m hn C) ∨ R ∈ Whitney.whitneyLayer m hn (componentWindowLayer m hn C + 1)) (p : HCPolySupport.Vec d) : (∀ (T : ↑(Whitney.simplexPartition m hn)), ∀ x ∈ (↑T).openCarrier, superposedCompetitorSlope m hn (Whitney.badFamily M m hn omega) p x = superposedCompetitorCellSlope m hn (Whitney.badFamily M m hn omega) p ↑T) ∧ (∀ (T : ↑(Whitney.simplexPartition m hn)), Multiscale.whitneyCubeOf m hn ↑T ∈ Whitney.badFamily M m hn omega → superposedCompetitorCellSlope m hn (Whitney.badFamily M m hn omega) p ↑T = 0) ∧ ∀ (T : ↑(Whitney.simplexPartition m hn)), Multiscale.whitneyCubeOf m hn ↑T ∉ Whitney.whitneyNeighborhood m hn (Whitney.badFamily M m hn omega) → superposedCompetitorCellSlope m hn (Whitney.badFamily M m hn omega) p ↑T = p

The deliverable in the consumer's own binder shape. At the manuscript's bad family ℐ = badFamily M m h_n omega and over the subtype ↥(simplexPartition m hn), these are literally the hFc, hbadF and hoffF hypotheses of Multiscale.sum_of_a_decomp (SubadditiveDecomposition.lean) (and, at q, its hGc, hbadG, hoffG).

The window binder is a theorem, not an assumption

theorem Algsuperdiff.Section3.Provider.Affine.badComponents_window {d : ℕ} {M : ABKModel d} {m : ℤ} {b : ℝ} {hs k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (havoid : ∀ (h : ℕ), hs ≤ h → ∀ u ∈ Percolation.cubeFinset h, ↑(Percolation.badClusterDiam M m h omega u) < 3 ^ (b * ↑h)) {S : Set (HCPolySupport.TriadicCube d)} (hSsub : S ⊆ Whitney.whitneyPartition m (Whitney.whitneyScaleSeq b hs k₀)) (hSbad : ∀ Q ∈ S, omega ∈ BadEvents.bad M Q) (C : Set (HCPolySupport.TriadicCube d)) : C ∈ badComponents S → (Whitney.whitneyNeighborhood m (Whitney.whitneyScaleSeq b hs k₀) C).Finite ∧ ∀ R ∈ Whitney.whitneyNeighborhood m (Whitney.whitneyScaleSeq b hs k₀) C, R ∈ Whitney.whitneyLayer m (Whitney.whitneyScaleSeq b hs k₀) (componentWindowLayer m (Whitney.whitneyScaleSeq b hs k₀) C) ∨ R ∈ Whitney.whitneyLayer m (Whitney.whitneyScaleSeq b hs k₀) (componentWindowLayer m (Whitney.whitneyScaleSeq b hs k₀) C + 1)

The binders are those of whitneyNeighborhood_finite_and_mem_leastLayer_or_succ, forwarded unchanged.

theorem Algsuperdiff.Section3.Provider.Affine.badComponents_window_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) (C : Set (HCPolySupport.TriadicCube d)) : C ∈ badComponents (Whitney.badFamily M m (Whitney.whitneyScale M m E b k₀ omega) omega) → (Whitney.whitneyNeighborhood m (Whitney.whitneyScale M m E b k₀ omega) C).Finite ∧ ∀ R ∈ Whitney.whitneyNeighborhood m (Whitney.whitneyScale M m E b k₀ omega) C, R ∈ Whitney.whitneyLayer m (Whitney.whitneyScale M m E b k₀ omega) (componentWindowLayer m (Whitney.whitneyScale M m E b k₀ omega) C) ∨ R ∈ Whitney.whitneyLayer m (Whitney.whitneyScale M m E b k₀ omega) (componentWindowLayer m (Whitney.whitneyScale M m E b k₀ omega) C + 1)

Discharge of hwin at the manuscript's own bad family ℐ = badFamily M m h_n omega, with the avoidance binder supplied by the proved e.diameter.deterministic.