High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.ExactRootGaugeTerminalDefinition

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

The large-scale C¹ slope approximation clause, conditional on the exact-gauge terminal

The large-scale C¹ slope approximation clause has no unconditional provider; its exact missing provider is an exact-gauge ball terminal whose delay L and constant A are chosen before kappa, abar, Phi, gradPhi, a, x, R and the solution. This module composes that terminal with the physical return Root.exists_rangeCompletePhysicalC1_of_exactRootGaugeTerminal and the root corrector-family hypothesis, and obtains the frozen the large-scale C¹ slope approximation clause body at the reconciled-smallness certificate.

The terminal itself is not proved here. What the corrector-cone lift does buy is that the two reasons for the terminal being unreachable are gone:

• the order gap (printCertificateOrder g ≥ 1/4 against the C¹ theorem's s < 1/12) — removed, see Root.exists_printOrderInfiniteCorrectorC1Constants;
• the sample-dependent restart — removed, see Root.exists_printOrderUndelayedExactGaugeRow, which delivers the simultaneous-slope row on cubes at start triadicCeilingIndex x with constants fixed by (d, g, ϑ) alone.

What is left between that cube row and this terminal is the cube-to-ball packaging at continuous radii, together with the identification of the identity-gauge family with the normalized-root coefficient bRef. That is the exact rendered residue.

def HCPolySupport.HighContrast.CorrectorComposition.ExactRootGaugeTerminal (d : ℕ) [NeZero d] (GoodScale : Mat d → CoeffSpace d → ℝ → Prop) (CorrectorFamily : Mat d → (Vec d → CoeffSpace d → Vec d → ℝ) → (Vec d → CoeffSpace d → Vec d → Vec d) → Prop) (eta : ℝ) : Prop

The exact-gauge ball terminal: the delay L and the constant A are chosen before the rate, the matrix, the family, the sample, the scale, the radius and the solution.

Equations

• One or more equations did not get rendered due to their size.