High-contrast homogenization: Provider.PolynomialHomogenization.Root.Dirichlet.AnchoredProduct

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

The anchored product

Anchoring the response bound at the observation cell multiplies it by the cell's own scale factor. In the parent-anchored response formula the cell index enters only through the difference M - K_i, so the anchoring cancels it exactly: the anchored product does not depend on the cell at all, and its whole scale content is the frame exponent (s - kappa) M + kappa L.

That cancellation is what makes the frame exponent the only place the eccentricity can enter, and hence what makes the fold of the previous modules the whole of the repair.

theorem HCPolySupport.HighContrast.RowSupply.printCellScaleFactor_mul_responseBound_eq {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) {s deltaScaled Cresponse kappaRate : ℝ} {M : ℤ} {L : ℕ} (responseBound : system.CellIndex → ℝ) (hresponseFormula : ∀ (i : system.CellIndex), responseBound i = Cresponse * Real.rpow 3 (s * (↑M - ↑(ruledObservationCube system i).scale)) * √deltaScaled * Real.rpow 3 (-kappaRate * (↑M - ↑L))) (i : system.CellIndex) : printCellScaleFactor (ruledObservationCube system i) s * responseBound i = Cresponse * √deltaScaled * Real.rpow 3 ((s - kappaRate) * ↑M + kappaRate * ↑L)

The anchored product is cell-free. The observation cell's scale factor cancels the cell index in the parent-anchored response formula, leaving the frame exponent.