High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.DecoupledRootPhysicalLipschitz

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

Root-facing physical Lipschitz wrapper

The recurrence constant and the finite homothetic prefix are selected before the coefficient sample. Their finite product is absorbed into one real constant at the root surface.

theorem HCPolySupport.HighContrast.Root.exists_decoupledRootPhysicalLipschitz (d : ℕ) [NeZero d] (g : ℝ) : g ∈ Set.Ico 0 1 → ∃ (Crec : ℝ) (c : ℝ), 1 ≤ Crec ∧ c = (2 * Crec)⁻¹ ∧ c ∈ Set.Ioo 0 1 ∧ ∀ (kappa : ℝ), ∃ (Clip : ℝ), 0 < Clip ∧ ∀ (abar : Mat d) (a : CoeffSpace d) (x : ℝ), 1 ≤ x → DecoupledRootGoodScale d g c kappa abar a x → ∀ (R : ℝ), x ≤ R → ∀ (u : Vec d → ℝ) (Du : Vec d → Vec d), MemH1a (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) u Du → IsWeakSolutionOn (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) Du → ∀ r ∈ Set.Icc x R, weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar r) Du ≤ ENNReal.ofReal Clip * weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) Du

The decoupled root certificate supplies the exact physical Lipschitz row. After the rate is fixed, the estimate constant is independent of the matrix, coefficient sample, exposed scale, and solution.