High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.CeilingInterface

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

the ceiling-exporting smallness interface The ceiling-exporting corrector-smallness interface

The root's single exported length forces a single corrector smallness c, and the certificate is increasing in c (so no uniform downward choice exists). The fix is a ceiling-exporting interface:

• GoodScale : ℝ → ℝ → ℝ → Mat d → CoeffSpace d → ℝ → Prop, read GoodScale g c κ abar a x;
• each hole exports ∃ cMax ∈ Ioo 0 1, ∀ c ∈ Ioo 0 1, c ≤ cMax → …;
• the assembly instantiates at the minimum of the five ceilings;
• hhomogenized gains ∀ c ∈ Ioo 0 1 → before its ∃ kappaRate Lcert pCert, with Lcert allowed to depend on c — and it must, because Lcert contains certAmplitudeBase … / correctorTargetAmplitude c κ.

This module implements that interface. rootGoodScaleAt is the c-parameterised certificate; exists_rootGoodScaleAt_of_quenchedRow is the c-parameterised hhomogenized, obtained from the RootInterface proof by replacing its fixed c := 1/2 with the bound variable; and minCeiling_mem / le_minCeiling_* are the arithmetic the assembly needs to instantiate at the minimum of five ceilings.

The body of exists_rootGoodScaleAt_of_quenchedRow is the fixed-threshold argument with 1 / 2 generalised to a leading binder.

def HCPolySupport.HighContrast.CorrectorComposition.rootGoodScaleAt (d : ℕ) [NeZero d] (g c kappaRate : ℝ) (abar : Mat d) (a : CoeffSpace d) (x : ℝ) : Prop

The c-parameterised root certificate. Identical to RootInterface.RootGoodScale except that the corrector smallness is a binder rather than an existential, so a consumer can demand its own ceiling.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.CorrectorComposition.rootGoodScale_of_rootGoodScaleAt {d : ℕ} [NeZero d] {g c kappaRate : ℝ} {abar : Mat d} {a : CoeffSpace d} {x : ℝ} (h : rootGoodScaleAt d g c kappaRate abar a x) : RootInterface.RootGoodScale d g kappaRate abar a x

Forgetting the smallness parameter recovers the RootInterface certificate, so every consumer of the unparameterised interface still applies.

theorem HCPolySupport.HighContrast.CorrectorComposition.exists_rootGoodScaleAt_of_quenchedRow (d : ℕ) [NeZero d] {g : ℝ} (hg : g ∈ Set.Ico 0 1) {c kappa delta : ℝ} (hc : c ∈ Set.Ioo 0 1) (hkappa : 0 < kappa) (hdelta : delta ∈ Set.Ioo 0 1) : ∃ (kappaRate : ℝ) (Lcert : ℝ) (pCert : ℝ), 0 < kappaRate ∧ kappaRate ≤ (1 + g) / 4 ∧ 1 ≤ Lcert ∧ 0 ≤ pCert ∧ ∀ (abar : Mat d), Matrix.PosDef (symmPart abar) → ∀ (S X : CoeffSpace d → ℝ) (a : CoeffSpace d), Quenched.HasAllLaterPhysicalBlockRow ((1 + 3 * g) / 4) kappa delta (Book.Ch02.constantBlockMatrix abar) S X a → 1 ≤ X a → S a ≤ X a → rootGoodScaleAt d g c kappaRate abar a (X a * (Lcert * RowSupply.eccentricityFoldFactor abar pCert))

hhomogenized, at every corrector smallness. The exported length factor Lcert depends on c; the exported exponent pCert does not.

The five-ceiling minimum

theorem HCPolySupport.HighContrast.CorrectorComposition.minCeiling_mem {c₁ c₂ c₃ c₄ c₅ : ℝ} (h₁ : c₁ ∈ Set.Ioo 0 1) (h₂ : c₂ ∈ Set.Ioo 0 1) (h₃ : c₃ ∈ Set.Ioo 0 1) (h₄ : c₄ ∈ Set.Ioo 0 1) (h₅ : c₅ ∈ Set.Ioo 0 1) : min c₁ (min c₂ (min c₃ (min c₄ c₅))) ∈ Set.Ioo 0 1

The minimum of five ceilings is a ceiling.

theorem HCPolySupport.HighContrast.CorrectorComposition.minCeiling_le_one {c₁ c₂ c₃ c₄ c₅ : ℝ} : min c₁ (min c₂ (min c₃ (min c₄ c₅))) ≤ c₁

theorem HCPolySupport.HighContrast.CorrectorComposition.minCeiling_le_two {c₁ c₂ c₃ c₄ c₅ : ℝ} : min c₁ (min c₂ (min c₃ (min c₄ c₅))) ≤ c₂

theorem HCPolySupport.HighContrast.CorrectorComposition.minCeiling_le_three {c₁ c₂ c₃ c₄ c₅ : ℝ} : min c₁ (min c₂ (min c₃ (min c₄ c₅))) ≤ c₃

theorem HCPolySupport.HighContrast.CorrectorComposition.minCeiling_le_four {c₁ c₂ c₃ c₄ c₅ : ℝ} : min c₁ (min c₂ (min c₃ (min c₄ c₅))) ≤ c₄

theorem HCPolySupport.HighContrast.CorrectorComposition.minCeiling_le_five {c₁ c₂ c₃ c₄ c₅ : ℝ} : min c₁ (min c₂ (min c₃ (min c₄ c₅))) ≤ c₅