High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.CeilingReconciliation

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

Reconciling the five ceilings

Under the ceiling-exporting smallness interface ceiling-exporting interface the assembly instantiates at the minimum of the five ceilings. This module proves that this is always possible: from five holes each exporting its own g-indexed ceiling, one function cStar : ℝ → ℝ is produced that satisfies all five simultaneously at every admissible g, together with hhomogenized at that same smallness.

Threading a function rather than a constant is what makes the interface compatible with the assembly's binder order: its GoodScale is bound before g, so the smallness cannot be a constant chosen after g — but it can be cStar g for a cStar bound before GoodScale.

theorem HCPolySupport.HighContrast.CorrectorComposition.exists_commonCeiling (Q₁ Q₂ Q₃ Q₄ Q₅ : ℝ → ℝ → Prop) (h₁ : ∀ g ∈ Set.Ico 0 1, ∃ cMax ∈ Set.Ioo 0 1, ∀ c ∈ Set.Ioo 0 1, c ≤ cMax → Q₁ g c) (h₂ : ∀ g ∈ Set.Ico 0 1, ∃ cMax ∈ Set.Ioo 0 1, ∀ c ∈ Set.Ioo 0 1, c ≤ cMax → Q₂ g c) (h₃ : ∀ g ∈ Set.Ico 0 1, ∃ cMax ∈ Set.Ioo 0 1, ∀ c ∈ Set.Ioo 0 1, c ≤ cMax → Q₃ g c) (h₄ : ∀ g ∈ Set.Ico 0 1, ∃ cMax ∈ Set.Ioo 0 1, ∀ c ∈ Set.Ioo 0 1, c ≤ cMax → Q₄ g c) (h₅ : ∀ g ∈ Set.Ico 0 1, ∃ cMax ∈ Set.Ioo 0 1, ∀ c ∈ Set.Ioo 0 1, c ≤ cMax → Q₅ g c) : ∃ (cStar : ℝ → ℝ), ∀ g ∈ Set.Ico 0 1, cStar g ∈ Set.Ioo 0 1 ∧ Q₁ g (cStar g) ∧ Q₂ g (cStar g) ∧ Q₃ g (cStar g) ∧ Q₄ g (cStar g) ∧ Q₅ g (cStar g)

The five-ceiling reconciliation. Each Qᵢ is a hole's obligation at a given smallness; each hole exports a ceiling below which its obligation holds. One g-indexed smallness serves all five.