PartitionCovering

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

d.whitney.bad-set.definitions, the partition contract: covering and boundary geometry

This module proves local versions of two clauses of ABK26's sss.whitney.partition that the definition module BadSetDefinitions states but does not prove:

• the covering / partition property (: "a Whitney-type partition of □_m"): the half-open realizations of the cubes of 𝒲(□_m) are pairwise disjoint (whitneyPartition_pairwiseDisjoint_cubeSet) and their union is exactly the open root cube (openCubeSet_originCube_eq_iUnion_whitneyPartition), so every point of the open root lies in exactly one Whitney cube;
• the geometric meaning of TouchesBoundary claimed in the docstring of BadSetDefinitions: for a triadic descendant of □_m, failing the extreme-index test puts the closed cube --- which is the closed ball closure_cubeSet_eq_closedBall --- inside the open root (closedBall_subset_openCubeSet_of_not_touchesBoundary), and the test is controlled quantitatively by the ℓ^∞ distance to ∂□_m (boundaryMargin_le_of_touchesBoundary and its contrapositive not_touchesBoundary_of_lt_boundaryMargin).

Why the open root cube

Homogenization.cubeSet is the half-open realization ∏ᵢ [·, ·); this is the realization for which triadic subdivision is an exact partition. The manuscript's termination clause says that no element of 𝒲(□_m) touches ∂□_m, so no Whitney cube can contain a point of ∂□_m, while the half-open cubeSet (originCube d m) does contain its own "lower" faces. The exact identity is therefore with openCubeSet (originCube d m), and this is the honest reading of "partition of □_m" here; it is also the form the simplicial refinement iUnion_carrier_simplexPartition composes with. Stronger still: the manuscript's root cube is literally open — defines □_m:= (−½·3^m, ½·3^m)^d — so the open form is not merely forced by the termination clause, it is the printed carrier itself.

Provider hypotheses

• The covering needs [NeZero d]. This is not a convenience: for d = 0 no cube satisfies TouchesBoundary (the predicate is an ∃ i : Fin 0), so every whitneyLayer is empty while openCubeSet (originCube 0 m) is the whole one-point space. [NeZero d] is the standing dimension hypothesis of the manuscript, and it enters exactly once, through touchesBoundary_originCube — the seed □_m of the recursion.
• Pairwise disjointness needs no hypothesis on the depth profile hn: it is proved from the exit-depth structure of whitneyLayer alone. (The variant SimplexPartition.disjoint_cubeSet_of_mem_whitneyPartition is now a delegation to the theorem here, likewise hypothesis-free —.)
• The covering needs no hypothesis on hn either.

References

• ABK26, sss.whitney.partition (the construction, its termination clause, and e.W.n.def).

Boundary-index arithmetic

theorem Algsuperdiff.Section3.Provider.Whitney.extremeIdx_mul_zpow (m : ℤ) (t : ℕ) : ↑(extremeIdx t) * 3 ^ (m - ↑t) + 3 ^ (m - ↑t) / 2 = 3 ^ m / 2

The extreme index of a depth-t descendant sits exactly one half-cube inside ∂□_m: E_t · 3^{m-t} + 3^{m-t}/2 = 3^m/2.

theorem Algsuperdiff.Section3.Provider.Whitney.abs_index_le_extremeIdx_sub_one {d : ℕ} {m : ℤ} {t : ℕ} {C : HCPolySupport.TriadicCube d} (hCmem : C ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d m) t) (hCnt : ¬TouchesBoundary m C) (j : Fin d) : |C.index j| ≤ extremeIdx t - 1

A non-touching depth-t descendant of □_m has strictly sub-extreme index in every coordinate.

theorem Algsuperdiff.Section3.Provider.Whitney.touchesBoundary_originCube {d : ℕ} [NeZero d] (m : ℤ) : TouchesBoundary m (HCPolySupport.originCube d m)

□_m touches its own boundary: the seed of the Whitney recursion. This is the single place where the dimension hypothesis enters.

Closed cubes, open cubes and the frontier of □_m

theorem Algsuperdiff.Section3.Provider.Whitney.mem_closedBall_cubeCenter_iff {d : ℕ} {Q : HCPolySupport.TriadicCube d} {x : HCPolySupport.Vec d} : x ∈ Metric.closedBall (HCPolySupport.cubeCenter Q) (HCPolySupport.cubeRadius Q) ↔ ∀ (i : Fin d), (↑(Q.index i) - 1 / 2) * HCPolySupport.cubeScaleFactor Q ≤ x i ∧ x i ≤ (↑(Q.index i) + 1 / 2) * HCPolySupport.cubeScaleFactor Q

Coordinatewise membership in the closed realization of a triadic cube.

theorem Algsuperdiff.Section3.Provider.Whitney.closure_cubeSet_eq_closedBall {d : ℕ} (Q : HCPolySupport.TriadicCube d) : closure (HCPolySupport.cubeSet Q) = Metric.closedBall (HCPolySupport.cubeCenter Q) (HCPolySupport.cubeRadius Q)

The closure of a half-open triadic cube is its closed realization.

The geometric characterization of TouchesBoundary

theorem Algsuperdiff.Section3.Provider.Whitney.closedBall_subset_openCubeSet_of_not_touchesBoundary {d : ℕ} {m : ℤ} {t : ℕ} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d m) t) (hQnt : ¬TouchesBoundary m Q) : Metric.closedBall (HCPolySupport.cubeCenter Q) (HCPolySupport.cubeRadius Q) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

A non-touching descendant of □_m has its closed cube strictly inside the open root cube.

Every Whitney cube lies in the open root cube

theorem Algsuperdiff.Section3.Provider.Whitney.closedBall_subset_openCubeSet_of_mem_whitneyLayer {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {n : ℕ} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ whitneyLayer m hn n) : Metric.closedBall (HCPolySupport.cubeCenter Q) (HCPolySupport.cubeRadius Q) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

The termination clause, geometrically: a Whitney cube does not meet ∂□_m; its closed realization sits inside the open root cube.

theorem Algsuperdiff.Section3.Provider.Whitney.cubeSet_subset_openCubeSet_of_mem_whitneyLayer {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {n : ℕ} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ whitneyLayer m hn n) : HCPolySupport.cubeSet Q ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

theorem Algsuperdiff.Section3.Provider.Whitney.cubeSet_subset_openCubeSet_of_mem_whitneyPartition {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ whitneyPartition m hn) : HCPolySupport.cubeSet Q ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

The boundary margin of a touching ancestor

theorem Algsuperdiff.Section3.Provider.Whitney.boundaryMargin_le_of_touchesBoundary {d : ℕ} {m : ℤ} {n : ℕ} {A : HCPolySupport.TriadicCube d} (hAscale : A.scale = m - ↑n) {x : HCPolySupport.Vec d} (hxA : x ∈ HCPolySupport.cubeSet A) (hAt : TouchesBoundary m A) : 3 ^ m / 2 - ‖x‖ ≤ 3 ^ (m - ↑n)

The boundary-margin estimate (one-sided half): a boundary-touching cube of size 3^{m-n} containing x forces x to be within 3^{m-n} of ∂□_m in the ℓ^∞ sense.

theorem Algsuperdiff.Section3.Provider.Whitney.not_touchesBoundary_of_lt_boundaryMargin {d : ℕ} {m : ℤ} {n : ℕ} {A : HCPolySupport.TriadicCube d} (hAscale : A.scale = m - ↑n) {x : HCPolySupport.Vec d} (hxA : x ∈ HCPolySupport.cubeSet A) (hsmall : 3 ^ (m - ↑n) < 3 ^ m / 2 - ‖x‖) : ¬TouchesBoundary m A

Contrapositive of the margin estimate: a cube much smaller than the distance from x to ∂□_m cannot touch ∂□_m.

The covering

theorem Algsuperdiff.Section3.Provider.Whitney.exists_mem_whitneyLayer_of_mem_openCubeSet {d : ℕ} [NeZero d] (m : ℤ) (hn : ℕ → ℕ) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : ∃ (n : ℕ), ∃ Q ∈ whitneyLayer m hn n, x ∈ HCPolySupport.cubeSet Q

Every point of the open root cube exits the boundary recursion at a finite layer. This is the constructive content of the covering clause.

theorem Algsuperdiff.Section3.Provider.Whitney.openCubeSet_originCube_eq_iUnion_whitneyPartition {d : ℕ} [NeZero d] (m : ℤ) (hn : ℕ → ℕ) : HCPolySupport.openCubeSet (HCPolySupport.originCube d m) = ⋃ Q ∈ whitneyPartition m hn, HCPolySupport.cubeSet Q

𝒲(□_m) covers □_m: the half-open Whitney cubes tile the open root cube exactly.

Pairwise disjointness

theorem Algsuperdiff.Section3.Provider.Whitney.mem_descendantsAtDepth_of_mem_cubeSet_inter {d : ℕ} {m : ℤ} {p q : ℕ} {U V : HCPolySupport.TriadicCube d} (hU : U ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d m) p) (hV : V ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d m) q) (hpq : p ≤ q) {x : HCPolySupport.Vec d} (hxU : x ∈ HCPolySupport.cubeSet U) (hxV : x ∈ HCPolySupport.cubeSet V) : V ∈ HCPolySupport.descendantsAtDepth U (q - p)

Two triadic descendants of □_m sharing a point, the first not deeper than the second, are nested.

theorem Algsuperdiff.Section3.Provider.Whitney.eq_of_mem_cubeSet_of_mem_whitneyPartition {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {Q R : HCPolySupport.TriadicCube d} (hQ : Q ∈ whitneyPartition m hn) (hR : R ∈ whitneyPartition m hn) {x : HCPolySupport.Vec d} (hxQ : x ∈ HCPolySupport.cubeSet Q) (hxR : x ∈ HCPolySupport.cubeSet R) : Q = R

Whitney cubes containing a common point coincide. No hypothesis on the depth profile hn is needed.

theorem Algsuperdiff.Section3.Provider.Whitney.whitneyPartition_pairwiseDisjoint_cubeSet {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) : (whitneyPartition m hn).PairwiseDisjoint HCPolySupport.cubeSet

𝒲(□_m) is pairwise disjoint.