High-contrast homogenization: Provider.Regularity.PrintOrderRoundedGenerationOneStepAffineExcess

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

Rounded one-step affine-excess recurrence at the common scale

This file combines the rounded harmonic comparison on the first child with direct regularity for the rounded constant operator. It implements the printed step at HC (5.65)--(5.66).

theorem HCPolySupport.HighContrast.exists_printOrderRoundedGenerationOneStepAffineExcess (d : ℕ) [NeZero d] (g : ℝ) (geom : RoundedGenerationAnalyticGeometry d) (hg : g ∈ Set.Ico 0 1) (hdual : PrintOrderRoundedReferenceDualRegularityAtGeneration d g geom.generation) : ∃ (N : ℕ), 0 < N ∧ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (aRounded : Book.Ch03.CoeffFamily d), (∀ (R : TriadicCube d), (aRounded.coeffOn R).toCoeffField = ↑↑(geom.centeredCoeffSpace abar hS a)) → ∀ (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) aRounded) (k : ℤ) (hkm : k ≤ m), finiteCenteredCubeBestFitErrorAt aRounded m u (k - ↑N) ⋯ ≤ 1 / 8 * finiteCenteredCubeBestFitErrorAt aRounded m u k hkm + C * geom.spatialWeakError a abar hS (printCertificateOrder g) k * finiteCenteredCubeSolutionEnergy aRounded m u k

At every order below one half, the selected-generation dual comparison supplies the complete affine-excess one-step estimate.