High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.FixedParentResponsePriceAlgebra

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

Fixed-parent response-price normalization

The square root in the all-depth response estimate is rewritten as the product of the filling constant, the parent-to-cell growth, and the converted power tail. This is the exact form consumed by the physical-frame algebra.

theorem HCPolySupport.HighContrast.RowSupply.sqrt_observationParent_powerPrice_eq {d : ℕ} {s epsilon amplitude kappa : ℝ} (abar : Mat d) {N K M : ℤ} (hKM : K ≤ M) (hAmplitude : 0 ≤ amplitude) (hs : s ≤ 1 / 2) : √(observationParentConvolutionFactor d s epsilon abar M K * (amplitude * (3 ^ M / 3 ^ N) ^ (-kappa)) ^ 2) = √(observationFillingCoefficient d epsilon abar * (Book.Ch02.geometricDiscount (1 - 2 * s) 1)⁻¹) * Real.rpow 3 (s * (↑M - ↑K)) * amplitude * Real.rpow 3 (-kappa * (↑M - ↑N))

The explicit all-depth response price factors into its three nonnegative components when the observation generation is below the fixed parent.