High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.AnchoredCommonResidualParent

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

Anchored common residual parent

The ellipsoid premise anchors the gauge domain at the origin. After dividing by the normalized-root scale, the residual affine image lies in the fixed generation-one adapted cell. Hence the common parent can be selected with an explicit upper generation rather than by an arbitrary bounded-domain radius.

theorem HCPolySupport.HighContrast.RowSupply.matImage_epsilonAffineGrid_subset_normalizedRoot_cell_one {d : ℕ} [NeZero d] {U : Set (Vec d)} {lambda : ℝ} (hlambda : lambda ∈ Set.Icc 1 3) {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (hGauge : U ⊆ {z : Vec d | vecNormSq z ≤ specBound (symmPart abar)⁻¹}) : matImage (epsilonAffineGrid lambda abar) U ⊆ adaptedCell (Selection.normalizedRoot (symmPart abar)) 1

A normalized gauge domain is contained in the fixed generation-one normalized-root cell after the residual dilation in [1,3].

theorem HCPolySupport.HighContrast.RowSupply.exists_anchored_common_matImage_enclosingParent {d : ℕ} [NeZero d] {U : Set (Vec d)} {lambda : ℝ} (hlambda : lambda ∈ Set.Icc 1 3) {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (hGauge : U ⊆ {z : Vec d | vecNormSq z ≤ specBound (symmPart abar)⁻¹}) (n : ℤ) : ∃ (M : ℤ), M = max n 1 ∧ n ≤ M ∧ matImage (epsilonAffineGrid lambda abar) U ⊆ adaptedCell (Selection.normalizedRoot (symmPart abar)) M

The anchored selector chooses the explicit common generation max n 1. It therefore publishes both containment and its exact deterministic upper generation relative to the requested activation generation.