ActiveFamily

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

The active family 𝒜_R, its multiplicity bound, and the superposed competitor

GlobalSuperposition.lean builds the multi-component competitor ℓ̂_p = ℓ_p + Σ_𝒞 (ℓ̂_p^𝒞 − ℓ_p) and proves the three sum_of_a_decomp clauses for its field, with no finiteness of the component family. Its Scope section names the gap that this module fills:

• the active family is finite, with a cardinality bounded by a dimensional constant M(d), uniformly in the Whitney cube.

The active family and the constant

For a Whitney cube R writes

𝒜_R := {𝒞 : R ∈ 𝒩(𝒞)}

which is activeComponents m hn ℐ R below (the components of ℐ whose touching collar contains R). Here it is

M(d) = 3 · 11^d ,

3 for the three layers n−1, n, n+1 a cube touching a layer-n cube can occupy (BoundaryDistance.whitneyLayer_index_close_of_cubeTouch, the adjacency clause alone) and 11^d for the per-layer packing at the cubewise touch relation of e.neighborhood.def (Multiscale.CollarMass.card_le_eleven_pow_of_forall_cubeTouch), the two generations of scale slack being's ±2 depth window (Multiscale.CollarMass.layerDepth_sub_le_two).

Inactive components and the cell slope

The active family is what the superposed cell constants actually see. The Whitney cubes touching one Whitney cube form a finite family (finite_setOf_mem_whitneyPartition_cubeTouch), each of them activating at most M(d) components; and a component that is inactive at the Whitney cube Q carrying a cell T — one whose touching collar misses Q — leaves the competitor's cell constant on T equal to the ambient p, so it contributes nothing to the sum of superposedCompetitorCellSlope_eq_sum. That is globalCompetitorCellSlope_eq_of_notMem_activeComponents, proved from the predecessor's globalCompetitorSlope_eq_cellSlope. Together with the multiplicity bound it caps at M(d) the number of summands that can be nonzero on any single cell.

Scope: what this module does NOT do

• No gradient estimate.'s summed bound |∇ℓ̂_p − p| ≤ C(d)|p| Σ_{𝒞 ∈ 𝒜_R} diam(𝒞)/ρ_𝒞 is read and not consumed: no diameter, no interpolation scale ρ_𝒞 and no constant C(d) occurs below. This module supplies the two inputs that estimate needs and nothing else — the finite index set 𝒜_R over which the sum runs, and |𝒜_R| ≤ M(d) for the squared/Cauchy--Schwarz form.
• No weak gradient, no H¹₀. The cell constants read below are those of the defined piecewise-constant field superposedCompetitorCellSlope, and nothing identifies them with a distributional gradient; no a.e. statement, no MemVectorL2, no H10Function and no zero-trace statement occurs. e.hat.linear.1 and the hF/hG binders of Multiscale.sum_of_a_decomp remain untouched.
• No continuity and no compact support. The counting below is confined to the open root cube, and that is sharp for this route: the Whitney cubes accumulate at ∂□_m, so the finiteness argument has no analogue there. As the predecessor recorded, compact support must come from the cutoff/truncation, not from the collar.
• No disjointness of collars is asserted or used, exactly as in GlobalSuperposition.lean; the overlap is counted, not removed. Merging overlapping components is not attempted — rules it unsafe.
• No three-layer window and no face-to-face property of SW(□_m) is used.

References

• ABK26, (𝒲(□_m), e.W.n.def, the boundary distance), (ℐ, e.neighborhood.def), (the components), (the adjacency clause), (e.SW.def), (l.piecewise.affine.approx, e.hat.linear.properties), (the false disjointness), (Step 1, "well-defined and continuous"), (the gradient estimate — not consumed), (ℓ_e).
• Two ideas were taken: bound the touching cubes layerwise over Icc (n-1) (n+1) and sum the per-layer packing; and choose one bad cube per active component, recovering the component from it for injectivity. Everything is restated at this repository's carriers (CubeTouch, whitneyNeighborhood, badComponent, KuhnCell, globalCompetitor) and reproved from this repository's proved inputs.

Main results

• card_le_three_mul_eleven_pow_of_forall_cubeTouch, finite_setOf_mem_whitneyPartition_cubeTouch — the Whitney cubes touching one Whitney cube, counted and bounded.
• activeComponents, activeComponents_finite, card_le_multiplicityBound_of_forall_mem_activeComponents — the deliverable |𝒜_R| ≤ M(d) = 3·11^d, the bound being multiplicityBound d = 3·11^d.
• globalCompetitorCellSlope_eq_of_notMem_activeComponents — a component that is inactive at the Whitney cube of a cell leaves the competitor's slope on that cell equal to p.

The Whitney cubes touching one Whitney cube

theorem Algsuperdiff.Section3.Provider.Affine.mem_Icc_of_cubeTouch_of_mem_whitneyLayer {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} (hn1 : ∀ (j : ℕ), 1 ≤ hn j) {n k : ℕ} {Q R : HCPolySupport.TriadicCube d} (hQ : Q ∈ Whitney.whitneyLayer m hn k) (hR : R ∈ Whitney.whitneyLayer m hn n) (htouch : Whitney.CubeTouch Q R) : k ∈ Finset.Icc (n - 1) (n + 1)

The three-layer window of the touch relation. A Whitney cube touching a layer-n cube occupies one of the layers n-1, n, n+1 — the adjacency clause, which consequence 2 needs no percolation input and no largeness of k₀, only h_n ≥ 1.

theorem Algsuperdiff.Section3.Provider.Affine.finite_setOf_mem_whitneyPartition_cubeTouch {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} (hn1 : ∀ (j : ℕ), 1 ≤ hn j) {n : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ Whitney.whitneyLayer m hn n) : {Q : HCPolySupport.TriadicCube d | Q ∈ Whitney.whitneyPartition m hn ∧ Whitney.CubeTouch Q R}.Finite

Only finitely many Whitney cubes touch one Whitney cube. They are confined to three layers, and each layer is a Finset.

theorem Algsuperdiff.Section3.Provider.Affine.card_le_three_mul_eleven_pow_of_forall_cubeTouch {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} (hn1 : ∀ (j : ℕ), 1 ≤ hn j) (hmono : Monotone hn) (hgap : ∀ (j : ℕ), hn (j + 1) ≤ hn j + 1) {n : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ Whitney.whitneyLayer m hn n) {A : Finset (HCPolySupport.TriadicCube d)} (hA : ∀ Q ∈ A, Q ∈ Whitney.whitneyPartition m hn ∧ Whitney.CubeTouch Q R) : A.card ≤ 3 * 11 ^ d

The dimension-only count of the touching cubes: at most 3·11^d Whitney cubes touch a fixed Whitney cube. 3 is the layer window and 11^d is the proved per-layer packing at the cubewise touch relation (Multiscale.card_le_eleven_pow_of_forall_cubeTouch), applicable because's ±2 depth window (Multiscale.layerDepth_sub_le_two) puts the three layers within two generations of one another.

The active family 𝒜_R

def Algsuperdiff.Section3.Provider.Affine.multiplicityBound (d : ℕ) : ℕ

The multiplicity constant M(d), M(d) = 3·11^d: three layers times the cubewise per-layer packing.

Equations

• Algsuperdiff.Section3.Provider.Affine.multiplicityBound d = 3 * 11 ^ d

def Algsuperdiff.Section3.Provider.Affine.activeComponents {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (I : Set (HCPolySupport.TriadicCube d)) (R : HCPolySupport.TriadicCube d) : Set (Set (HCPolySupport.TriadicCube d))

The active family 𝒜_R = {𝒞 : R ∈ 𝒩(𝒞)}: the components of the bad family whose touching collar contains the Whitney cube R. These are exactly the components whose correction can be nonzero on R.

Equations

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

theorem Algsuperdiff.Section3.Provider.Affine.mem_activeComponents_iff {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {I : Set (HCPolySupport.TriadicCube d)} {R : HCPolySupport.TriadicCube d} {C : Set (HCPolySupport.TriadicCube d)} : C ∈ activeComponents m hn I R ↔ C ∈ badComponents I ∧ R ∈ Whitney.whitneyNeighborhood m hn C

theorem Algsuperdiff.Section3.Provider.Affine.exists_cubeTouch_and_eq_badComponent_of_mem_activeComponents {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {I : Set (HCPolySupport.TriadicCube d)} (hI : I ⊆ Whitney.whitneyPartition m hn) {R : HCPolySupport.TriadicCube d} {C : Set (HCPolySupport.TriadicCube d)} (hC : C ∈ activeComponents m hn I R) : ∃ B ∈ Whitney.whitneyPartition m hn, Whitney.CubeTouch B R ∧ C = Whitney.badComponent I B

An active component is recovered from any of its bad cubes touching R. This is the maximality fact isolates, in the form that makes the counting injective.

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

The chosen bad cube of an active component, touching R.

Equations

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

theorem Algsuperdiff.Section3.Provider.Affine.activeComponents_finite {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} (hn1 : ∀ (j : ℕ), 1 ≤ hn j) {I : Set (HCPolySupport.TriadicCube d)} (hI : I ⊆ Whitney.whitneyPartition m hn) {n : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ Whitney.whitneyLayer m hn n) : (activeComponents m hn I R).Finite

Finiteness of the active family — the input GlobalSuperposition.lean names as the operative obstruction to continuity and per-cell affineness.

theorem Algsuperdiff.Section3.Provider.Affine.card_le_multiplicityBound_of_forall_mem_activeComponents {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} (hn1 : ∀ (j : ℕ), 1 ≤ hn j) (hmono : Monotone hn) (hgap : ∀ (j : ℕ), hn (j + 1) ≤ hn j + 1) {I : Set (HCPolySupport.TriadicCube d)} (hI : I ⊆ Whitney.whitneyPartition m hn) {n : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ Whitney.whitneyLayer m hn n) {A : Finset (Set (HCPolySupport.TriadicCube d))} (hA : ∀ C ∈ A, C ∈ activeComponents m hn I R) : A.card ≤ multiplicityBound d

The multiplicity bound, Finset form. Every finite family of components active at R has at most M(d) members.

Inactive components contribute nothing

theorem Algsuperdiff.Section3.Provider.Affine.globalCompetitorCellSlope_eq_of_notMem_activeComponents {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) {n : ℕ} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ Whitney.whitneyLayer m hn n) {T : Whitney.KuhnCell d} (hT : T ∈ Whitney.whitneySimplexCells m hn n Q) {C : Set (HCPolySupport.TriadicCube d)} (hC : C ∈ badComponents I) (hCQ : C ∉ activeComponents m hn I Q) : globalCompetitorCellSlope m (Whitney.simplexScale m hn (componentWindowLayer m hn C)) C p T = p

A component inactive at the cell's Whitney cube has cell constant p — clause 3 of e.hat.linear.properties read at the active family.