Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.Corrector.PrintOrderLipschitzFiniteDelayWrapper

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.Corrector.PrintOrderLipschitzFiniteDelayWrapper

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

Root certificate to printed finite-delay data #

The printed-order certificate produces the selected-generation terminal surface, and its recurrence start differs from the root start by one deterministic delay.

source
theorem HCPolySupport.HighContrast.Root.exists_printOrderRootFiniteDelaySurface (d : ℕ) [NeZero d] (g : ℝ) :
g ∈ Set.Ico 0 1 → ∃ (C : ℝ) (c : ℝ) (Cid : ℝ), 1 ≤ C ∧ c = (2 * C)⁻¹ ∧ c ∈ Set.Ioo 0 1 ∧ ∀ (kappa : ℝ) (abar : Mat d) (a : CoeffSpace d) (x : ℝ), PrintOrderRateBearingCommonAffineGoodScale d g c kappa abar a x → ∃ (surface : Certificate.PrintOrderDecoupledFiniteTerminalSurface d g c kappa Cid abar a x), Quenched.triadicCeilingIndex (printOrderCommonQuantitativeAffineScale d g surface.sourceAmplitude (correctorTargetAmplitude c kappa) kappa abar surface.X a) ≤ Quenched.triadicCeilingIndex x + Quenched.triadicCeilingIndex (printOrderToBaseResponseScaleFactor d g kappa)

A root-facing printed certificate supplies one selected-generation finite terminal and a law-free comparison of its start index with the root index.

source
theorem HCPolySupport.HighContrast.Root.exists_decoupledRootFiniteDelaySurface (d : ℕ) [NeZero d] (g : ℝ) :
g ∈ Set.Ico 0 1 → ∃ (C : ℝ) (c : ℝ) (Cid : ℝ), 1 ≤ C ∧ c = (2 * C)⁻¹ ∧ c ∈ Set.Ioo 0 1 ∧ ∀ (kappa : ℝ) (abar : Mat d) (a : CoeffSpace d) (x : ℝ), DecoupledRootGoodScale d g c kappa abar a x → ∃ (surface : Certificate.PrintOrderDecoupledFiniteTerminalSurface d g c kappa Cid abar a x), Quenched.triadicCeilingIndex (printOrderCommonQuantitativeAffineScale d g surface.sourceAmplitude (correctorTargetAmplitude c kappa) kappa abar surface.X a) ≤ Quenched.triadicCeilingIndex x + Quenched.triadicCeilingIndex (printOrderToBaseResponseScaleFactor d g kappa)

The same finite-delay package is available from the root's paired qualitative and printed-order certificate.