High-contrast homogenization: Provider.Quenched.ThresholdCalibration

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

Threshold calibration for the quenched endgame

This is the numerical choice behind the small-contrast threshold of ss.algebraic.convergence. Once a positive small-contrast threshold has been fixed, the two remaining thresholds can be chosen before any exponent or probability law.

theorem HCPolySupport.HighContrast.Quenched.exists_threshold_calibration_below (cSc : ℝ) (hcSc : 0 < cSc) : ∃ (delta₀ : ℝ) (cEnd : ℝ), delta₀ ∈ Set.Ioo 0 1 ∧ 0 < cEnd ∧ (1 + delta₀) ^ 2 * (1 + cEnd) ≤ 1 + cSc

Given a positive small-contrast threshold, there are positive rebasing and entry thresholds satisfying the endgame calibration.