High-contrast homogenization: Provider.Regularity.UnitCubeDirichletContinuousKRescaling

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

Rescaled continuous K-functional bound for the unit-cube Dirichlet map

The exact lower endpoint and the finite upper endpoint are combined without collapsing their constants. Enlarging the interpolation scale by one fixed factor absorbs the upper bound while the normalized Euclidean L² residual retains constant one.

theorem HCPolySupport.HighContrast.exists_unitCubeDirichletContinuousKFunctional_rescaled (d : ℕ) [NeZero d] : ∃ (A : ℝ), 1 ≤ A ∧ ∀ (h : UnitCubeEuclideanL2Field d) (w : H10Function (openCubeSet (originCube d 0))) (t u : ↑ContinuousKScale), CubeDirichletDivergenceProblem (originCube d 0) w h.toField → ↑u = A * ↑t → continuousKFunctional t (unitCubeGradientEuclideanL2Field w) ≤ continuousKFunctional u h

There is a dimension-dependent expansion factor A ≥ 1 such that the unit-cube identity Dirichlet solution map satisfies K(t, ∇w) ≤ K(A t, h) whenever both displayed parameters belong to the source scale carrier. The factor is fixed before both scales, the datum, and the weak solution.