High-contrast homogenization: Provider.Quenched.Prop42Tilt.CorrectedTiltConsumer

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

Consumption by the corrected halfway transfer

The native additive adapter is put in the exact scalar shape consumed by the corrected halfway-scale arithmetic. The only remaining estimates are the hatted tail and the numerical adapter-error bound.

theorem HCPolySupport.HighContrast.Quenched.corrected_tilt_base_transfer {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P g E Ψ K S) {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) {n₀ : ℕ} (hfin : HasFiniteAdaptedMean P q ↑(Prop42Scalar.correctedTiltScale n₀ (2 * n₀))) {cStar A : ℝ} (hentry : annealedContrast P 0 - 1 ≤ cStar) (hcStarA : cStar ≤ A) : annealedContrast P ↑(2 * n₀) - 1 ≤ 9 / 2 * (↑d * (adaptedHattedContrast P q ↑(Prop42Scalar.correctedTiltScale n₀ (2 * n₀)) - 1)) + A * Real.rpow 3 (-↑(2 * n₀ - Prop42Scalar.correctedTiltScale n₀ (2 * n₀)))

At the single boundary scale where the corrected halfway index equals the outer index, entry smallness supplies the scalar transfer directly. Thus the strict scale inequality required by the geometric adapter is needed only after this base case.