High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Certificate.PrintOrderDecoupledTerminalSurface

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

Root surface of the order-decoupled rounded spine

The printed stochastic order controls the weak-error row. The private Dirichlet response keeps its independently selected deterministic order, and the two constructions meet only through the selected coefficient family and the finite energy recurrence.

structure HCPolySupport.HighContrast.Certificate.PrintOrderDecoupledFiniteTerminalSurface (d : ℕ) [NeZero d] (g c kappa Cid : ℝ) (abar : Mat d) (a : CoeffSpace d) (x : ℝ) : Type

Complete pointwise output of the decoupled spine. It retains the source certificate, the selected rounded generation, all recurrence inputs, and the closed finite terminal induction.

• sourceAmplitude : ℝ

  Source amplitude in the initial quantitative normalized reference certificate.

• X : CoeffSpace d → ℝ

  Coefficient-dependent scale function used by the initial and final reference certificates.

• sourceCertificate : PrintOrderQuantitativeNormalizedReferenceCertificate abar g self.sourceAmplitude kappa (self.X a) a
• rootScale_eq : x = commonQuantitativeAffineScale self.sourceAmplitude (correctorTargetAmplitude c kappa) kappa (Transport.roundedOuterResponseAffineConstant d) (specBound (symmPart abar) * specBound (symmPart abar)⁻¹) kappa self.X a
• spine : PrintOrderToleranceSelectedRoundedSpine d Cid

  Rounded spine selected at the tolerance determined by Cid.

• join : PrintOrderParametricRoundedResponseJoin d g a abar self.sourceAmplitude (correctorTargetAmplitude c kappa) kappa Cid self.X

  Rounded response application joining the source amplitude to the target amplitude.

• generation_eq : self.join.application.generation = self.spine.generation
• finalCertificate : PrintOrderQuantitativeNormalizedReferenceCertificate abar g (correctorTargetAmplitude c kappa) kappa (printOrderCommonQuantitativeAffineScale d g self.sourceAmplitude (correctorTargetAmplitude c kappa) kappa abar self.X a) a
• recurrenceInputs : PrintOrderParametricFiniteRecurrenceInputs d g a abar self.sourceAmplitude (correctorTargetAmplitude c kappa) kappa Cid self.X self.join

  Finite recurrence estimates for the selected rounded response join.

• recurrenceConstant : ℝ

  Constant in the terminal finite induction and the inverse target relation.

• recurrenceConstant_ge : 1 ≤ self.recurrenceConstant
• target_eq_inverse : c = (2 * self.recurrenceConstant)⁻¹
• recurrence (n m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) self.join.application.aRounded) : n ≤ m → RoundedGenerationSpatialGoodMaxOnInterval self.join.application.generation a abar ⋯ (printCertificateOrder g) 1 n m → ∀ h ∈ Finset.Icc n m, finiteCenteredCubeSolutionEnergy self.join.application.aRounded m u h ≤ self.recurrenceConstant * finiteCenteredCubeSolutionEnergy self.join.application.aRounded m u m + self.recurrenceConstant * ∑ j ∈ Finset.Ioc h m, roundedGenerationSpatialWeakError self.join.application.generation a abar ⋯ (printCertificateOrder g) j * finiteCenteredCubeSolutionEnergy self.join.application.aRounded m u j
• terminal : let n := ↑(Quenched.triadicCeilingIndex (printOrderCommonQuantitativeAffineScale d g self.sourceAmplitude (correctorTargetAmplitude c kappa) kappa abar self.X a)); ∀ (m : ℤ), n ≤ m → ∀ (u : Book.Ch03.CubeSolution (originCube d m) self.join.application.aRounded), ∀ h ∈ Finset.Icc n m, finiteCenteredCubeSolutionEnergy self.join.application.aRounded m u h ≤ 2 * self.recurrenceConstant * finiteCenteredCubeSolutionEnergy self.join.application.aRounded m u m

theorem HCPolySupport.HighContrast.Certificate.exists_printOrderDecoupledFiniteTerminalSurface (d : ℕ) [NeZero d] (g Cid : ℝ) (hg : g ∈ Set.Ico 0 1) (hidentity : PrintOrderIdentityCubeDualRegularityWithConstant d g Cid) : ∃ (C : ℝ) (c : ℝ), 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 → Nonempty (PrintOrderDecoupledFiniteTerminalSurface d g c kappa Cid abar a x)

The constructor selected from the identity estimate gives a pointwise terminal surface for every rate-bearing certificate. The contraction amplitude is selected after g, because the printed-order analytic constant depends on that order, but before the coefficient sample and certificate.