High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.ResidualFrameResponseRateAlgebra

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

Residual-frame response-rate algebra

Once the stochastic row has been converted before aggregation, the remaining scale bookkeeping is deterministic. The observation filling grows at the response order, while the physical dual norm contributes the larger target order. A common upper parent generation therefore gives a uniform cell coefficient.

theorem HCPolySupport.HighContrast.RowSupply.physicalFluxEpsilonFrameBound_of_residualResponsePower {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) {b r Cflux epsilon Xval kappaRate : ℝ} (hb : 0 < b) (hbr : b < r) (hkr : kappaRate ≤ r) (responseBound : system.CellIndex → ℝ) (M : system.CellIndex → ℤ) (L : ℕ) (Mmax : ℤ) (Cresponse amplitude Arate : ℝ) (hCflux : 0 ≤ Cflux) (hCresponse : 0 ≤ Cresponse) (hAmplitude : 0 ≤ amplitude) (hArate : 0 ≤ Arate) (hM : ∀ (i : system.CellIndex), (ruledObservationCube system i).scale ≤ M i) (hMmax : ∀ (i : system.CellIndex), M i ≤ Mmax) (hResponseNonneg : ∀ (i : system.CellIndex), 0 ≤ responseBound i) (hResponse : ∀ (i : system.CellIndex), responseBound i ≤ Cresponse * Real.rpow 3 (b * (↑(M i) - ↑(ruledObservationCube system i).scale)) * amplitude * Real.rpow 3 (-kappaRate * (↑(M i) - ↑L))) (hAmplitudeRate : amplitude ≤ Arate * (epsilon * Xval) ^ kappaRate) : PhysicalFluxEpsilonFrameBound system b r Cflux responseBound epsilon Xval kappaRate (Cflux * r⁻¹ * Book.Ch03.constantCoeffMatrixNormHalf (identityConstantCoeffMatrix d) * responseOneFromTwoGapFactor b r * Cresponse * Real.rpow 3 ((r - kappaRate) * ↑Mmax + kappaRate * ↑L - r) * Arate)

A common parent-generation cap and the transported row amplitude imply the uniform physical-frame premise used by RATE-AGG. This statement isolates the geometric input from the stochastic order conversion.