High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.ExactRootTerminalCube

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

The exact-root terminal cube solution — the large-scale C¹ slope approximation clause residue (b1)

The large-scale C¹ slope approximation terminal ExactRootGaugeTerminal splits into four items, of which exactly one, (b1), is new content:

a terminal CubeSolution on originCube d m for the exact-root reference family, from MemH1a + IsWeakSolutionOn on the ball [the exact-root analogue of the rounded ellipsoid terminal cube solution]

The obstruction is a strict negative consumer: the terminal's corrector-family premise is ∀ Q, (aRounded.coeffOn Q).toCoeffField =ᵐ[volume] roundedCenteredCoefficient abar hS ⇑a.1, and the exact-root family satisfies the exact-root identity instead.

That mismatch is the whole of it. The proof never uses any property of baseRoundedGrid beyond invertibility and symmetry, both of which the exact root has (CorrectorComposition.isUnit_det_exactRoot, CorrectorComposition.matTranspose_exactRoot). This module runs the same proof at Selection.normalizedRoot (symmPart abar) and yields the terminal cube solution for the exact-root family, so (b1) is discharged.

Two deliberate differences from the statement:

• the terminal generation m is a parameter together with the geometric premise matImage (Selection.normalizedRoot (symmPart abar)) (openCubeSet (originCube d m)) ⊆ ellipsoid abar R, rather than the fixed roundedEllipsoidTerminalGeneration. The large-scale C¹ slope approximation clause packaging needs to choose m against the inner-cube side of the volume comparison, so pinning the generation inside the constructor would be the wrong interface. Nothing is weakened: the generation is one admissible choice.
• the corrector-family premise is stated against the exact-root coefficient affineCoefficient (Selection.normalizedRoot (symmPart abar)) _ ⇑(normalizedCenteredCoeff a abar hS).1, which is literally the large-scale C¹ slope approximation clause terminal's bRef.

No estimate is used and no hypothesis is added: the premise list is the one with roundedCenteredCoefficient replaced by bRef and the generation exposed.

theorem HCPolySupport.HighContrast.CorrectorComposition.exists_exactRootTerminalCubeSolution {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (aRef : Book.Ch03.CoeffFamily d) (hRefAE : ∀ (Q : TriadicCube d), (aRef.coeffOn Q).toCoeffField =ᵐ[MeasureTheory.volume] affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ↑↑(normalizedCenteredCoeff a abar hS)) {R : ℝ} (m : ℤ) (hm : matImage (Selection.normalizedRoot (symmPart abar)) (openCubeSet (originCube d m)) ⊆ ellipsoid abar R) (u : Vec d → ℝ) (Du : Vec d → Vec d) (hu : MemH1a (↑↑a) (ellipsoid abar R) u Du) (hweak : IsWeakSolutionOn (↑↑a) (ellipsoid abar R) Du) : ∃ (w : Book.Ch03.CubeSolution (originCube d m) aRef), w.toH1.grad = fun (y : Vec d) => matVecMul (Selection.normalizedRoot (symmPart abar)) (Du (matVecMul (Selection.normalizedRoot (symmPart abar)) y))

The exact-root terminal cube solution. A physical MemH1a weak solution on the radius-R ellipsoid gives a Chapter 3 cube solution, for the exact-root reference family, on any origin cube whose exact-root image sits inside the ellipsoid; its gradient is the exact-root pullback of the physical one.