High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.GaugeMaxPowerFluxFrameAbsorption

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

The law-free flux frame at a truncated gauge power

The response chain's filling coefficient is a truncation at one of a multiple of the absolute gauge scale, because the cross-grid matrix of the affine grid against the exact normalized root is lambda * alpha times the identity. A truncation at one is not bounded by any positive power of the gauge scale — it tends to one as the scale tends to zero, while the power tends to zero — so the absorption has to be recorded at the truncated power rather than at the bare one.

The inner-ellipsoid normalization premise gives exactly that: the gauge scale is below the ratio of the outer sandwich radius to the normalization radius, and a truncation at one is monotone, so the truncated power is absorbed exactly as the bare power was.

theorem HCPolySupport.HighContrast.RowSupply.cellAnchoredObservationRateBound_of_gaugeMaxPowerRate {d : ℕ} [NeZero d] {Uphys U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {b c epsilon Xval kappaRate q K : ℝ} (responseBound : system.CellIndex → ℝ) (hc : 0 < c) (hK : 0 ≤ K) (hq : 0 ≤ q) (hEX : 0 ≤ epsilon * Xval) (hInner : ellipsoid abar c ⊆ Uphys) (hSandwich : HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ Uphys) rho Rad) (hrate : ∀ (i : system.CellIndex), 0 ≤ responseBound i ∧ printCellScaleFactor (ruledObservationCube system i) b * responseBound i ≤ K * max 1 (√(specBound (symmPart abar)⁻¹) ^ q) * (epsilon * Xval) ^ kappaRate) : CellAnchoredObservationRateBound system b responseBound epsilon Xval kappaRate (K * max 1 ((Rad / c) ^ q))

The absorption at a truncated gauge power. The truncation at one is monotone, so the inner-ellipsoid normalization premise absorbs it unchanged.

theorem HCPolySupport.HighContrast.RowSupply.physicalFluxEpsilonFrameBound_of_gaugeMaxPowerRate {d : ℕ} [NeZero d] {Uphys U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {b r Cflux c epsilon Xval kappaRate q K : ℝ} (responseBound : system.CellIndex → ℝ) (hUopen : IsOpen U) (hRad : 0 ≤ Rad) (hb : 0 < b) (hbr : b < r) (hCflux : 0 ≤ Cflux) (hc : 0 < c) (hK : 0 ≤ K) (hq : 0 ≤ q) (hEX : 0 ≤ epsilon * Xval) (hInner : ellipsoid abar c ⊆ Uphys) (hSandwich : HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ Uphys) rho Rad) (hrate : ∀ (i : system.CellIndex), 0 ≤ responseBound i ∧ printCellScaleFactor (ruledObservationCube system i) b * responseBound i ≤ K * max 1 (√(specBound (symmPart abar)⁻¹) ^ q) * (epsilon * Xval) ^ kappaRate) : PhysicalFluxEpsilonFrameBound system b r Cflux responseBound epsilon Xval kappaRate (Real.rpow 3 (-b) * (2 * Rad).rpow (r - b) * Cflux * r⁻¹ * Book.Ch03.constantCoeffMatrixNormHalf (identityConstantCoeffMatrix d) * responseOneFromTwoGapFactor b r * (K * max 1 ((Rad / c) ^ q)))

The law-free physical flux frame at a truncated gauge power. No comparison matrix, sample, law, microscopic parameter or cell index survives in the frame constant.