High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.C1SlopeBoundedDecay

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

The simultaneous-slope row, with its slope norm exported

One datum the simultaneous-slope row discards is needed here: a bound on the Euclidean norm of the slope it returns. The bound is already derived inside Root.exists_scalarIdentityInfiniteCorrectorC1Constants — the block

euclideanNorm e ≤ 2 * euclideanNorm (P e) = 2 * euclideanNorm bBase
              ≤ 2 * K * h1EnergyNormOnCube (originCube d m) a u.toH1

from exists_canonicalFiniteCorrectorProjectionInverseControlThreshold and exists_baseExactMinimizerSlopeEnergyConstants — and is used there only to absorb euclideanNorm e into the reverse comparison. This module exports it.

Why it is needed: the large-scale C¹ slope approximation's ball terminal must hold at every radius r ∈ Icc rStart R, including the near-terminal band r > R / (108 √d) where the canonical outer cube of r overshoots every triadic cube contained in the ball of radius R. There the cube row says nothing, and the only route is to bound the corrector's own energy, ‖e + ∇Φ_e‖ ≤ B ‖e‖ (exists_scalarIdentityGoodTailJointWeightedGradientBoundConstant), and then ‖e‖ by the solution's energy — which is exactly this export.

The statement below is the infinite-corrector C¹ constants statement with two additions: a second constant Cslope, and the conjunct euclideanNorm e ≤ Cslope * h1EnergyNormOnCube (originCube d m) a u.toH1. The proof is the one byte for byte, with the already-present slope block moved ahead of the refine that returns e; it is generated by an assert-guarded exact-match script, never retyped.

theorem HCPolySupport.HighContrast.Root.exists_scalarIdentityInfiniteCorrectorC1ConstantsWithSlope (d : ℕ) [NeZero d] (s eta : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) (hetaHalf : 1 / 2 ≤ eta) (heta1 : eta < 1) : ∃ (C : ℝ) (Cslope : ℝ) (c : ℝ), 0 < C ∧ 0 < Cslope ∧ c ∈ Set.Ioo 0 1 ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n0 : ℤ), delta ∈ Set.Ioc 0 c → ScalarIdentityGoodTail a s delta n0 → FiniteAffineCorrectionLocalCauchy a → ∀ (Phi : Vec d → NormalizedLocalH1Carrier d), IsFiniteAffineCorrectionJointLocalEquation a Phi → ∀ (n m : ℕ), n0 ≤ ↑n → n + 2 ≤ m → ∀ (u : Book.Ch03.CubeSolution (originCube d ↑m) a), ∃ (e : Vec d), euclideanNorm e ≤ Cslope * Book.Ch03.h1EnergyNormOnCube (originCube d ↑m) a u.toH1 ∧ ∀ q ∈ Finset.Icc n m, (weightedGradNorm (a.coeffOn (originCube d ↑q)).toCoeffField (openCubeSet (originCube d ↑q)) fun (x : Vec d) => u.toH1.grad x - (e + (Phi e).globalGradientRepresentative x)) ≤ ENNReal.ofReal (C * Real.rpow 3 (-eta * ↑(m - q))) * weightedGradNorm (a.coeffOn (originCube d ↑m)).toCoeffField (openCubeSet (originCube d ↑m)) u.toH1.grad

A scalar-identity cube solution admits one infinite-corrector slope which works simultaneously on every intermediate centered cube.