High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.PushCorrectorFamilyDischarge

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

The corrector-and-flux decay clause/the Liouville and C¹ clauses family corrector-family

hypothesis, discharged

The corrector-family half of the decay, Liouville and C¹ clauses reduces to a single proposition, Root.SelectedReferenceCoeffExact d: the selected corrector datum's reference family must represent the normalized-root coefficient pointwise on every triadic cube. It is not provable, because the datum is chosen by Classical.choice and the structure carried only an almost-everywhere, origin-cube-only identity.

The repair is one extra field on RootCorrectorData (coeffAll, an a.e. identity on every triadic cube), which the converter that supplies the datum proves pointwise and previously discarded. With it the residue disappears entirely, and without indexing the datum by its exact field:

• the selected family and the certificate's exact-gauge reference family exists_normalizedReferenceCoeffFamily are Book.Ch02.TriadicCoeffFamily.AEEq;
• along that a.e. equality the joint local limit is literally the same carrier family (CorrectorComposition.jointLocalLimit_eq_of_aeeq), the local Cauchy condition transfers, and so does the weak-error good tail (Book.Ch02.HomogenizationErrorOnCube_eq_ofAEEq);
• so normalizedJoint may be answered with the certificate's family, which carries the pointwise coefficient identity by construction, while the two pullback clauses stay definitional at the pushforward pair with additive constant 0.

RootPushCanonicalFamily is therefore a theorem, with the normalized supply as its only input. the decay, Liouville and C¹ clauses's corrector-family hypothesis half are unconditional.

The good tail transfers

theorem HCPolySupport.HighContrast.CorrectorComposition.scalarIdentityGoodTail_of_aeeq {d : ℕ} {a b : Book.Ch02.TriadicCoeffFamily d} (hab : a.AEEq b) {s delta : ℝ} {n : ℤ} (h : ScalarIdentityGoodTail a s delta n) : ScalarIdentityGoodTail b s delta n

The scalar identity weak-error row is an a.e.-representative invariant, so the good tail transfers along an a.e. equality of coefficient families.

The corrector-family hypothesis

theorem HCPolySupport.HighContrast.CorrectorComposition.rootPushCanonicalFamily_of_normalizedSupply {d : ℕ} [NeZero d] {GoodScale : Mat d → CoeffSpace d → ℝ → Prop} (hsupply : Root.RootNormalizedSupply d GoodScale) : Root.RootPushCanonicalFamily d GoodScale

The pushforward canonical corrector-family hypothesis, from the normalized supply alone.

The consequences