High-contrast homogenization: Provider.Quenched.SmallContrastAlignedGeometry

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

Aligned-cell enclosure for the cap geometry

Every aligned adapted cell read by the row and weak caps sits inside the generation cube after one further enlargement: the center lies in the parent cell, hence in the parent's enlarged cube, and the cell itself adds at most one more cell radius. This discharges the hgeom hypotheses of the small-contrast row and weak caps at the account's grid-norm witness ‖q‖·√d ≤ 3^G, with the cap enlargement G + 1.

theorem HCPolySupport.HighContrast.Quenched.adaptedCellAt_subset_centeredCube_succ {d : ℕ} (hd : 1 ≤ d) {q : Mat d} (hq : Matrix.PosDef q) {G : ℕ} (hqnorm : ‖q‖ * √↑d ≤ 3 ^ G) {k p t : ℤ} (hkp : k ≤ p) (hpt : p ≤ t) {w : Fin d → ℤ} (hw : w ∈ Response.alignedIndex q k p) : adaptedCellAt q k w ⊆ centeredCube d (t + ↑(G + 1))

The aligned-cell enclosure. An aligned adapted cell at scale k ≤ p ≤ t whose center lies in the parent cell ⋄_p^q is contained in the centered cube at generation t enlarged by G + 1.

theorem HCPolySupport.HighContrast.Quenched.aligned_hgeom_of_grid_norm {d : ℕ} (hd : 1 ≤ d) {q : Mat d} (hq : Matrix.PosDef q) {G : ℕ} (hqnorm : ‖q‖ * √↑d ≤ 3 ^ G) {p t : ℤ} (hpt : p ≤ t) (k : ℤ) : k ≤ p → ∀ w ∈ Response.alignedIndex q k p, adaptedCellAt q k w ⊆ centeredCube d (t + ↑(G + 1))

The enclosure in the exact hgeom shape consumed by the small-contrast row and weak caps, at the cap enlargement G + 1.