Coarse-graining support: Support.Book.Ch05.Theorems.Section51.SmallWidetildeEntry

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Entry into shifted small contrast

This file combines the Section 5.5 perturbative entry theorem with the shifted high-moment localization estimate to produce small contrast for the 2β shifted (P4) data at the algebraic entry scale.

theorem HCPolySupport.Book.Ch05.Section51.shiftedSmallContrastEntry_homogenizationScale {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) {delta : ℝ} (hdelta_pos : 0 < delta) : ∃ (C : ℝ), 0 < C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d}, Ch04.RestrictionLawCarrier P → Ch04.RestrictionStructuralLaw P → ∀ (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → have N := annealedAlgebraicEntryScale P hP4 C; Section55.shiftedWidetildeThetaAtScale P (↑N) hP4 (2 * Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4) - 1 ≤ delta

Section 5.1 entry into the small-contrast regime for the 2β-shifted ellipticity exponents.

The constant is selected before the law. The target smallness parameter is explicit so the final theorem can feed in the small-contrast threshold from Section 5.6.