High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.TerminalCarrierIdentification

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

the large-scale C¹ slope approximation clause residue (iii): the terminal's carrier is the

row's carrier

The large-scale C¹ slope approximation clause ball terminal must exhibit one family PhiRef : Vec d → NormalizedLocalH1Carrier d that simultaneously

• pulls the pushforward marker's slope family back to the gauge frame (ExactRootGaugeTerminal's first clause), which forces PhiRef v = Root.rootJointCarrier d v (normalizedSample abar hS a), and
• carries the cube row's decay, which forces PhiRef to be the row's own Phi, the joint local limit of the identity-gauge family aIdentity.

These two are the same object, and the identification is "a rewrite, not an analytic step". This module performs it. The chain is

(selected datum).aFin  ≈ᵃᵉ  aRef   (RootCorrectorData.coeffAll + normalizedSample_ae)
aRef                   ≈ᵃᵉ  aIdentity   (rawIdentityCoeff_ae_global)

and CorrectorComposition.jointLocalLimit_eq_of_aeeq turns the composite a.e. equality into a literal equality of joint local limits; isFiniteAffineCorrectionJointLocalLimit_iff_eq pins the row's Phi to that same limit. No estimate, no measure theory beyond ae_restrict_of_ae.

theorem HCPolySupport.HighContrast.CorrectorComposition.rootJointCarrier_eq_rowCarrier (d : ℕ) [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {a : CoeffSpace d} (hev : Root.RootCorrectorEvent d (Root.normalizedSample abar hS a)) (hI : Matrix.PosDef (symmPart 1)) (aIdentity : Book.Ch03.CoeffFamily d) (hIdentity : ∀ (Q : TriadicCube d), (aIdentity.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace 1 hI (exactGaugeCoeffSpace a abar hS))) (hCauchyId : FiniteAffineCorrectionLocalCauchy aIdentity) (Phi : Vec d → NormalizedLocalH1Carrier d) (hPhi : IsFiniteAffineCorrectionJointLocalEquation aIdentity Phi) (v : Vec d) : Root.rootJointCarrier d v (Root.normalizedSample abar hS a) = Phi v

The root joint carrier is the row's carrier. Every hypothesis is one the undelayed row already returns.

theorem HCPolySupport.HighContrast.CorrectorComposition.pushforwardMarker_gaugePullback (d : ℕ) [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {a : CoeffSpace d} (ha : a ∈ Root.pushforwardCore d abar hS) (Phi : Vec d → NormalizedLocalH1Carrier d) (hcarrier : ∀ (v : Vec d), Root.rootJointCarrier d v (Root.normalizedSample abar hS a) = Phi v) (e : Vec d) : (fun (y : Vec d) => matVecMul (Selection.normalizedRoot (symmPart abar)) (e + Root.pushforwardPhysicalGradPhi d abar hS e a (matVecMul (Selection.normalizedRoot (symmPart abar)) y))) =ᵐ[MeasureTheory.volume] fun (y : Vec d) => matVecMul (Selection.normalizedRoot (symmPart abar)) e + (Phi (matVecMul (Selection.normalizedRoot (symmPart abar)) e)).globalGradientRepresentative y

The terminal's gauge-pullback clause, at the row's carrier. Under the pushforward marker the clause is definitional: pushforwardGradient_pullback_identity is a pointwise identity, and the carrier it names is the row's by rootJointCarrier_eq_rowCarrier.