High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.RealScaleTriadicBracket

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

Triadic bracket for a physical scale

If a positive physical parameter has inverse at least the common effective scale, its inverse can be rounded upward to one triadic generation. The rounded generation is still active for the common scale, and the remaining dimensionless dilation lies between one and three.

theorem HCPolySupport.HighContrast.RowSupply.exists_triadicScaleBracket_of_commonScale_le_inv {epsilon x : ℝ} (hEpsilon : 0 < epsilon) (hX : 1 ≤ x) (hScale : x ≤ epsilon⁻¹) : ∃ (N : ℕ), x ≤ 3 ^ N ∧ epsilon⁻¹ ≤ 3 ^ N ∧ 3 ^ N ≤ 3 * epsilon⁻¹ ∧ 1 ≤ epsilon * 3 ^ N ∧ epsilon * 3 ^ N ≤ 3

Upward triadic rounding of epsilon⁻¹ preserves activation above x and leaves the residual factor epsilon * 3^N in the interval [1,3].