High-contrast homogenization: Entry.Source.Subdivision

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Source subdivision support

This file starts the source-multiplier construction near e.source.multiplier, l.source.whitney by exposing two reusable facts needed before the stopping minimum is built: integer-stationary transport of the z = 0 dagger event, and the corresponding coarse-block translation identity for the qualitative coefficient carrier.

No source multiplier, radius, or new definition is introduced here.

theorem HCPolySupport.HighContrast.Source.coarseBlock_translateCoeff_eq_translateSet {d : ℕ} (U : Set (Vec d)) (z : Fin d → ℤ) (a : CoeffSpace d) : coarseBlock U (translateCoeff z a) = coarseBlock (translateSet (Source.AKL.intTranslation z) U) a

Translating a coefficient field is the same as translating the coarse-block domain. This is the general form of the adapted-cell covariance used by the S2 locality support, made public in the source namespace for standard-cell applications.

theorem HCPolySupport.HighContrast.Source.stationary_all_integer_dagger_event {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P g E Ψ K S) : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (z : Fin d → ℤ) (m : ℤ), S (translateCoeff z a) ≤ 3 ^ m → ∀ k ≤ m, ∀ (w : Fin d → ℤ), standardCellCenter k w ∈ centeredCube d m → BlockMatLoewnerLE (coarseBlock (standardCell d k w) (translateCoeff z a)) (blockScale (3 ^ (g * (↑m - ↑k))) E)

The dagger bound, transported from the z = 0 event to all integer translates. The conclusion is intentionally still written on translateCoeff z a; later source files may rewrite domains with coarseBlock_translateCoeff_eq_translateSet when a geometric cell identity is available.

theorem HCPolySupport.HighContrast.Source.sourceCenter_mem_iff (d jStar r : ℕ) (w : Fin d → ℤ) (b : ℕ) (hb : 3 ^ jStar = 2 * b + 1) : standardCellCenter (↑(jStar + r)) w ∈ centeredCube d ↑(2 * jStar + r) ↔ ∀ (i : Fin d), -↑b ≤ w i ∧ w i ≤ ↑b

The source index condition is a product of integer intervals.

theorem HCPolySupport.HighContrast.Source.sourceCenterSet_finite_card (d jStar r : ℕ) : {w : Fin d → ℤ | standardCellCenter (↑(jStar + r)) w ∈ centeredCube d ↑(2 * jStar + r)}.Finite ∧ {w : Fin d → ℤ | standardCellCenter (↑(jStar + r)) w ∈ centeredCube d ↑(2 * jStar + r)}.ncard = 3 ^ (d * jStar)

Exactly 3^(d*jStar) source indices, independently of the offset.

theorem HCPolySupport.HighContrast.Source.intTranslation_sourceCenter {d : ℕ} (jStar r : ℕ) (w : Fin d → ℤ) : (Source.AKL.intTranslation fun (i : Fin d) => 3 ^ (jStar + r) * w i) = standardCellCenter (↑(jStar + r)) w

The real source center is the image of the literal integer translation in the minimum.

theorem HCPolySupport.HighContrast.Source.exists_standardCell_ancestor {d : ℕ} {k m : ℤ} (hkm : k ≤ m) (w : Fin d → ℤ) : ∃ (v : Fin d → ℤ), standardCell d k w ⊆ standardCell d m v

Every aligned cube has an aligned ancestor at every coarser integer generation.

theorem HCPolySupport.HighContrast.Source.standardCell_eq_adapted_identity {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : standardCell d k w = adaptedCellTranslate 1 k (standardCellCenter k w)

A standard cube is the identity-metric adapted cube at its actual center.

theorem HCPolySupport.HighContrast.Source.standardCell_subdivision_null {d : ℕ} {k m : ℤ} (hkm : k ≤ m) (v : Fin d → ℤ) : MeasureTheory.volume (standardCell d m v \ ⋃ (w : ↑{w : Fin d → ℤ | standardCell d k w ⊆ standardCell d m v}), standardCell d k ↑w) = 0

The fixed-generation standard subcubes partition a standard parent a.e.

theorem HCPolySupport.HighContrast.Source.translate_standardCell_by_coarser_center {d : ℕ} (k : ℤ) (n : ℕ) (v w : Fin d → ℤ) : translateSet (standardCellCenter (k + ↑n) v) (standardCell d k w) = standardCell d k fun (i : Fin d) => w i + 3 ^ n * v i

Aligned translation by a coarser center preserves the finer standard grid.