High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.WitnessCubeEnclosure

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

The witness-cube enclosure

The λ-route composition at the frozen witness reduces to one named geometric lemma: the witness-cube analogue of residualObservationTarget_subset_matImage. The ruled analogue proves that a ruled observation cube of a Whitney system, pushed into residual affine coordinates, lies inside the affine image of the gauge domain. At the frozen witness there is no Whitney system: the domain is a single affine cube,

U = (fun x => z + matSqrt (symmPart abar) x) '' openCubeSet (originCube d j)

and the target cube is the same cube at the same generation j, centred at the gauge centre matSqrt (symmPart abar)⁻¹ z. The gauge image of U is then the translate of the open triadic cube by that centre (RowSupply.matImage_inv_affineImage), and the enclosure is an identity rather than a Whitney margin estimate.

After it, exists_anchored_common_matImage_enclosingParent composes and the hEnclose binder of observationHomogenizationError_le_referencePowerTail_fixedParent is discharged, at a parent generation chosen above both the reference tail shift and the witness generation itself.

theorem HCPolySupport.HighContrast.RowSupply.witnessObservationTarget_subset_matImage {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (lambda : ℝ) {j : ℤ} {z : Vec d} {U : Set (Vec d)} (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) : adaptedCellTranslate (epsilonAffineGrid lambda abar) j (lambda⁻¹ • matVecMul (matSqrt (symmPart abar)) (matVecMul (matSqrt (symmPart abar))⁻¹ z) + adaptedCellCenter (epsilonAffineGrid lambda abar) j 0) ⊆ matImage (epsilonAffineGrid lambda abar) (matImage (matSqrt (symmPart abar))⁻¹ U)

The witness-cube enclosure. In residual affine coordinates the frozen witness target at generation j, anchored at the gauge centre, is contained in the affine image of the gauge domain. This is the witness analogue of residualObservationTarget_subset_matImage.

theorem HCPolySupport.HighContrast.RowSupply.gaugeDomain_subset_normalizedSublevel {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} (hUsub : U ⊆ ellipsoid abar 1) : matImage (matSqrt (symmPart abar))⁻¹ U ⊆ {y : Vec d | vecNormSq y ≤ specBound (symmPart abar)⁻¹}

The gauge domain of the frozen witness sits inside the normalized Euclidean sublevel set, from the inner-ellipsoid normalization outer premise U ⊆ ellipsoid abar 1 alone.

theorem HCPolySupport.HighContrast.RowSupply.exists_witnessEnclosingParent {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {lambda : ℝ} (hlambda : lambda ∈ Set.Icc 1 3) {j : ℤ} {z : Vec d} {U : Set (Vec d)} (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) (hUsub : U ⊆ ellipsoid abar 1) (n : ℤ) : ∃ (M : ℤ), M = max (max n j) 1 ∧ n ≤ M ∧ j ≤ M ∧ 1 ≤ M ∧ adaptedCellTranslate (epsilonAffineGrid lambda abar) j (lambda⁻¹ • matVecMul (matSqrt (symmPart abar)) (matVecMul (matSqrt (symmPart abar))⁻¹ z) + adaptedCellCenter (epsilonAffineGrid lambda abar) j 0) ⊆ adaptedCell (Selection.normalizedRoot (symmPart abar)) M

The composed hEnclose at the frozen witness. The anchored selector's common parent, taken above both a requested generation n and the witness generation j, encloses the witness target. This is exactly the last hypothesis of observationHomogenizationError_le_referencePowerTail_fixedParent at epsilon := lambda, K := j, center := matVecMul (matSqrt (symmPart abar))⁻¹ z.