High-contrast homogenization: Provider.Quenched.SmallContrastCorrectedThresholds

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

The threshold caps at the canonical metric

The burn-in exponent of SmallContrastBurnInPolynomial, at a grid metric whose eccentricity is bounded by the reference aspect ratio: the adapter factor gains exactly one aspect-ratio factor over the identity-metric form, which the telescope base absorbs as one more power. This is that bridge.

theorem HCPolySupport.HighContrast.Quenched.bootstrapAdapterFactor_le_aspect_mul {d : ℕ} [Nonempty (Fin d)] {Cd g K : ℝ} {E : BlockMat d} {mAl : Mat d} {Pi : ℝ} (hecc : witnessEccentricity mAl ≤ Pi) (hfac0 : 0 ≤ (1 + K ^ 2) ^ g * euclideanReferenceRatio Cd g K E) : bootstrapAdapterFactor Cd g K E mAl ≤ Pi * bootstrapAdapterFactor Cd g K E 1

The adapter factor at an eccentricity-bounded metric is the identity form times the aspect ratio.

theorem HCPolySupport.HighContrast.Quenched.exists_burnIn_exponent_canonical (d : ℕ) [Nonempty (Fin d)] (Cd g sigma CB : ℝ) (hCd : 0 ≤ Cd) (hg1 : g ≤ 1) (hzeta : 0 ≤ zetaG g) (hsigma : 0 < sigma) (hCB : 0 ≤ CB) : ∃ (cburn : ℝ), 0 ≤ cburn ∧ ∀ (E : BlockMat d) (K : ℝ) (mAl : Mat d), 1 ≤ aspectRatio E → 1 ≤ K → 0 ≤ kappaRef E → kappaRef E ≤ 1 + 6 * sigma → witnessEccentricity mAl ≤ aspectRatio E → 0 ≤ (1 + K ^ 2) ^ g * euclideanReferenceRatio Cd g K E → ∀ (sK gap : ℤ), 3 ^ sK ≤ 3 ^ ↑(kZero d) * (3 * growthBar K) → 3 ^ gap ≤ 3 * max 1 (CB * bootstrapAdapterFactor Cd g K E mAl / sigma) → 3 ^ (sK + 1 + gap) ≤ (2 + aspectRatio E * K).rpow cburn

The burn-in exponent at an eccentricity-bounded metric.