High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.CenteredIndicatorExtensionBasic

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

The centered one-step indicator extension

The child test is extended by zero to its centered parent and multiplied by the parent-to-child volume ratio. This module proves the exact pairing identity and the local square-integrability part of the parent test carrier.

theorem HCPolySupport.HighContrast.RowSupply.originCube_mem_childCubes_succ (d : ℕ) (m : ℤ) : originCube d m ∈ childCubes (originCube d (m + 1))

The centered scale-m cube is the middle child of the centered scale-m+1 cube.