High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.FrozenWitnessClassBRows

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

Composed rows of the Dirichlet clause, from the frozen surface

Eight rows of the clause are compositions of existing producers. Three of them are pure compositions from the frozen witness geometry, and are built here:

• hUhat, hUhatMeas, hUhat0 — the gauge domain is the translate of an open triadic cube, and IsOpenBoundedConvexDomain.translateSet is upstream, so no matrix-image convexity lemma is needed at all, since the physical domain's own convexity is never available on surface, only its cube presentation.
• system, hU, hUnonempty, hRad — the ruled carrier at the gauge domain, from exists_enlargedMarginRuledTriadicWhitneySystem and the frozen ball sandwich. 0 < Rad is derived from the sandwich itself.
• the two Hardy premises — the ruled Hardy selector, whose conclusion is definitionally PrintFaithfulPositiveTestRow.

hGauge was already supplied in HCPoly.Provider.PolynomialHomogenization.Root.Dirichlet.WitnessCubeEnclosure (gaugeDomain_subset_normalizedSublevel), so four of the nine rows of are now discharged.

The gauge domain is a bounded open convex domain

theorem HCPolySupport.HighContrast.RowSupply.frozenWitness_gaugeDomain_isOpenBoundedConvexDomain {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) : IsOpenBoundedConvexDomain (matImage (matSqrt (symmPart abar))⁻¹ U)

Row hUhat/hUhatMeas/hUhat0. The gauge domain of the frozen witness is a bounded open convex domain.

theorem HCPolySupport.HighContrast.RowSupply.frozenWitness_gaugeDomain_nonempty {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) : (matImage (matSqrt (symmPart abar))⁻¹ U).Nonempty

The gauge domain of the frozen witness is nonempty.

theorem HCPolySupport.HighContrast.RowSupply.frozenWitness_gaugeDomain_volume_ne_zero {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) : MeasureTheory.volume (matImage (matSqrt (symmPart abar))⁻¹ U) ≠ 0

The gauge domain of the frozen witness has positive volume.

The outer sandwich radius is positive

theorem HCPolySupport.HighContrast.RowSupply.rad_pos_of_hasBallSandwich {d : ℕ} {V : Set (Vec d)} {rho Rad : ℝ} (hsandwich : HasBallSandwich V rho Rad) : 0 < Rad

Row hRad. A ball sandwich with a positive inner radius forces a positive outer radius.

The ruled carrier at the gauge domain

theorem HCPolySupport.HighContrast.RowSupply.exists_frozenWitnessRuledCarrier {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} {rho Rad : ℝ} (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) (hsandwich : HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ U) rho Rad) : Nonempty (EnlargedMarginRuledTriadicWhitneySystem (matImage (matSqrt (symmPart abar))⁻¹ U) rho Rad) ∧ IsOpenBoundedConvexDomain (matImage (matSqrt (symmPart abar))⁻¹ U) ∧ (matImage (matSqrt (symmPart abar))⁻¹ U).Nonempty ∧ 0 < Rad

Row system/hU/hUnonempty/hRad. The frozen surface produces the ruled Whitney carrier at the gauge domain, together with the three companion facts that module asks for.

The Hardy row