High-contrast homogenization: Provider.Quenched.SmallContrastNormalizedGauge

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

The gauge normalization at the frozen witness

The dagger admits the free renormalization Ψ ↦ max 1 (Ψ/Ψ(1)) at the SAME growth witness: the tail weakens legally since Ψ(1) ≥ 1, the growth condition transfers unchanged, and admissibility survives the flooring. After normalization the gauge's unit value is one, so the burn-split witness K' is polynomial in K and the burn depth alone — no Ψ(1) content reaches any scale threshold.

noncomputable def HCPolySupport.HighContrast.Quenched.normalizedGauge (Ψ : ℝ → ℝ) : ℝ → ℝ

The normalized gauge.

Equations

• HCPolySupport.HighContrast.Quenched.normalizedGauge Ψ t = max 1 (Ψ t / Ψ 1)

theorem HCPolySupport.HighContrast.Quenched.normalizedGauge_one {Ψ : ℝ → ℝ} (hΨ1 : 0 < Ψ 1) : normalizedGauge Ψ 1 = 1

theorem HCPolySupport.HighContrast.Quenched.coarseEllipticityDagger_normalizedGauge {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) : CoarseEllipticityDagger P g E (normalizedGauge Ψ) K S

The dagger at the normalized gauge.