High-contrast homogenization: Provider.Regularity.OrderDecouplingBoundary

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

Boundary of the order-decoupled rounded interface

The deterministic response is selected before the stochastic exponent. This module records the joint interface and the strict direction between its two orders. In particular, the printed-order row cannot be read as a row at the private response order without an additional theorem.

theorem HCPolySupport.HighContrast.privateRoundedOrder_lt_printCertificateOrder (d : ℕ) [NeZero d] {g : ℝ} (hg : g ∈ Set.Ico 0 1) : ↑(privateRoundedPhysicalDirichletSpine d).order < printCertificateOrder g

The private order is strictly below every admissible printed order.