High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.PushforwardNormalizedSupply

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

The normalized-gauge supply, from the certificate's own block row

The stationary corrector family clause reduces to RootNormalizedSupply. This module supplies it from the same physical block row that hhomogenized consumes, through the available converter exists_shiftedNormalizedReferencePowerTail_of_hasAllLaterPhysicalBlockRow.

Three things make the reduction work, and each is worth naming.

• The gauge matches. The converter's reference family satisfies (aRef.coeffOn Q).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) _ ↑↑(normalizedCenteredCoeff a abar hS), which is definitionally gaugeCoeff a abar hS — the two sides are the same affineCoefficient application, so the identification is rfl — hence almost everywhere ⇑(normalizedSample abar hS a).1. This is exactly the identity the identity-gauge demand cannot have.
• No smallness on the certificate's delta is needed. The converter returns a power tail, and ScalarIdentityPowerTail.rebase trades reference scale for amplitude: pushing the base scale out drives the amplitude below any prescribed tolerance. That is why the identity-gauge row was stated ∀ eps > 0 and why nothing here demands delta below a private constant.
• The translates are covered by the certificate itself. hquenched produces the row on a set OmegaEnd with ∀ z, translateCoeff z ⁻¹' OmegaEnd = OmegaEnd, so a certified sample and all of its integer translates carry the row. No per-z certificate is assumed.

The one exponent condition is rho < 2 * s, where s is the good-tail order the supply itself chooses. s is not a frozen constant: it is carried by the block-row supply and consumed only here, because the corrector datum records its order as a field rather than an index. At the certificate's rho = (1 + 3 g) / 4 a per-g order s := (1 + g) / 4 satisfies both 0 < s < 1/2 and rho < 2 * s for every g ∈ [0, 1), so the admitted range is the whole of [0,1); the frozen order would have forced g < 1/6.

Trading reference scale for amplitude

theorem HCPolySupport.HighContrast.Root.exists_goodTail_of_powerTail {d : ℕ} {aFin : Book.Ch02.TriadicCoeffFamily d} {s A kappa x eps : ℝ} (h : ScalarIdentityPowerTail aFin s A kappa x) (hA : 0 ≤ A) (hkappa : 0 < kappa) (hx : 1 ≤ x) (heps : 0 < eps) : ∃ (n : ℤ), ScalarIdentityGoodTail aFin s eps n

A power tail is a good tail at every prescribed tolerance. Rebasing to a larger reference scale divides the amplitude by a positive power, and the geometric sum of the rebased tail is below any eps > 0 once the base is far enough out.

The certificate-side block row

def HCPolySupport.HighContrast.Root.RootBlockRowSupply (d : ℕ) (GoodScale : Mat d → CoeffSpace d → ℝ → Prop) : Prop

The certificate-side input, in the shape hquenched produces it. A certified sample lies in a translation-invariant set on which the physical block row at the comparison matrix abar holds, with the row exponent below twice the private order.

Every field is on RootAssembly's own binder surface: Omega is OmegaEnd together with its ∀ z, translateCoeff z ⁻¹' OmegaEnd = OmegaEnd; rho is (1 + 3 g) / 4; kappa, delta, S, X are the interface's; 1 ≤ X b and S b ≤ X b are hquenched's own (∀ a, 1 ≤ X a) and (∀ a, S a ≤ X a); and the row itself is the hypothesis hhomogenized consumes, at the same Book.Ch02.constantBlockMatrix abar. Nothing new is introduced.

The good-tail order s is supplied here together with the row, subject only to the corrector cone 0 < s < 1/2 and the window rho < 2 * s. It is not a global constant, so the provider may choose it after the contrast exponent g — and nothing downstream of the supply ever sees it.

Equations

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

The supply

theorem HCPolySupport.HighContrast.Root.rootNormalizedSupply_of_blockRow {d : ℕ} [NeZero d] {GoodScale : Mat d → CoeffSpace d → ℝ → Prop} (hblock : RootBlockRowSupply d GoodScale) : RootNormalizedSupply d GoodScale

The normalized-gauge datum, from the block row. The single input correctorFamilyHole_of_normalizedSupply needs is produced by the certificate's own row, in the certificate's own gauge.

The hole, from the certificate's row alone

theorem HCPolySupport.HighContrast.Root.correctorFamilyHole_of_blockRow (d : ℕ) [NeZero d] (GoodScale : Mat d → CoeffSpace d → ℝ → Prop) (hblock : RootBlockRowSupply d GoodScale) (abar : Mat d) : Matrix.PosDef (symmPart abar) → ∃ (Phi : Vec d → CoeffSpace d → Vec d → ℝ) (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d), RootPushCorrectorFamilyPredicate d abar Phi gradPhi ∧ (∀ (c : ℝ) (e e' : Vec d) (a : CoeffSpace d), gradPhi (c • e + e') a =ᵐ[MeasureTheory.volume] fun (x : Vec d) => c • gradPhi e a x + gradPhi e' a x) ∧ (∀ (z : Fin d → ℤ) (e : Vec d) (a : CoeffSpace d), gradPhi e (translateCoeff z a) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => gradPhi e a (x + Source.AKL.intTranslation z)) ∧ ∀ (a : CoeffSpace d) (x : ℝ), GoodScale abar a x → ∀ (e : Vec d), HasWeakGradientOn Set.univ (Phi e a) (gradPhi e a) ∧ IsWeakSolutionOn (fun (y : Vec d) => ↑↑a y) Set.univ fun (y : Vec d) => e + gradPhi e a y

the stationary corrector family clause of the root assembly, from the certificate's own block row. This composes the inhabitant with the supply: no gauge change, no per-z certificate, no smallness beyond the exponent window rho < 2 * s at the supply's own order s.