High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.ActivationScaleEccentricity

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

The activation length in terms of the eccentricity

The certificate's activation length is a triadic power whose generation is the formulaic tail shift, the ceiling of a logarithm of the deterministic absorption prefactor. That prefactor carries the homogenized matrix only through the triadic bracket of its witness eccentricity, and it carries it as a fixed power.

The two estimates below make that quantitative: the activation length is at most three times the ceiling-free root of the prefactor, and the prefactor is at most a law-free constant times a fixed power of the eccentricity bracket. Together they exhibit the activation length as a law-free constant times a fixed power of the eccentricity, which is the form the scale fold consumes.

theorem HCPolySupport.HighContrast.RowSupply.pow_three_formulaicTailShift_le {d : ℕ} {s rho kappa : ℝ} {G : ℕ} (hkappa : 0 < kappa) (hP : 0 < Certificate.shiftedTailAbsorptionPrefactor d s rho G) : 3 ^ ↑(Certificate.formulaicNormalizedReferenceTailShift d s rho kappa G) ≤ 3 * max 1 (Certificate.shiftedTailAbsorptionPrefactor d s rho G ^ kappa⁻¹)

The activation length in terms of the absorption prefactor. The formulaic tail shift is a ceiling, so the triadic power it names is at most three times the truncated kappa-th root of the prefactor.

theorem HCPolySupport.HighContrast.RowSupply.shiftedTailAbsorptionPrefactor_le_of_bracket {d : ℕ} {s rho bracket : ℝ} {G : ℕ} (hrho : 0 ≤ rho) (hgeom : 0 < 1 - 3 ^ (-(2 * s - rho))) (hG : 3 ^ ↑G ≤ bracket) : Certificate.shiftedTailAbsorptionPrefactor d s rho G ≤ 6 * ↑d * √↑d * (bracket ^ rho * (1 / (1 - 3 ^ (-(2 * s - rho)))))

The absorption prefactor in terms of the eccentricity bracket. The only appearance of the homogenized matrix in the prefactor is the triadic bracket of its witness eccentricity, raised to the row order.