High-contrast homogenization: Provider.Quenched.AnnealedToQuenchedTransfer

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

The coupled annealed-to-quenched step

The polynomial entry theorem fixes the first small annealed scale. The annealed endpoint transports it through the rebased law, and one coupled quenched witness then supplies both the optimal marginal tail and the all-later bad-event certificate. This module composes those three outputs without separating the selected random scale from its certificate.

theorem HCPolySupport.HighContrast.Quenched.exists_quenched_minimal_scale_of_coupled_providers (d : ℕ) (hd : 2 ≤ d) (hcontrastCore : ∀ g ∈ Set.Ico 0 1, ∃ (cSc : ℝ), 0 < cSc ∧ ∃ (alpha : ℝ) (Cdelay : ℝ), 0 < alpha ∧ 0 ≤ Cdelay ∧ ∀ (cStar gBase : ℝ) (Pbase : MeasureTheory.Measure (CoeffSpace d)) (Ebase : BlockMat d) (PsiBase : ℝ → ℝ) (Kbase : ℝ) (Sbase : CoeffSpace d → ℝ), cStar ∈ Set.Ioo 0 cSc → gBase = (1 + g) / 2 → MeasureTheory.IsProbabilityMeasure Pbase → IsStationaryLaw Pbase → IsUnitRangeLaw Pbase → CoarseEllipticityDagger Pbase gBase Ebase PsiBase Kbase Sbase → annealedContrast Pbase 0 - 1 ≤ cStar → blockContrast Ebase ≤ 1 + cSc → ∃ (m0 : ℕ), 3 ^ m0 ≤ (2 + aspectRatio Ebase * Kbase) ^ Cdelay ∧ ∀ (j : ℕ), annealedContrast Pbase ↑(m0 + j) - 1 ≤ 3 ^ (-alpha * ↑j)) (hRebase : ∀ {cSc g cStar Centry : ℝ}, cStar ∈ Set.Ioo 0 cSc → g ∈ Set.Ico 0 1 → 0 < Centry → ∃ (Crebase : ℝ), 0 < Crebase ∧ Centry ≤ Crebase ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Psi : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P g E Psi K S → (∃ (mEnt : ℕ), ↑mEnt ≤ ⌈Centry * Real.logb 3 (2 + aspectRatio E * K)⌉ ∧ annealedContrast P ↑mEnt - 1 ≤ cStar ∧ 3 ^ mEnt ≤ 3 * (2 + aspectRatio E * K) ^ Centry) → ∃ (nBase : ℕ) (Pbase : MeasureTheory.Measure (CoeffSpace d)) (gBase : ℝ) (Ebase : BlockMat d) (PsiBase : ℝ → ℝ) (Kbase : ℝ) (Sbase : CoeffSpace d → ℝ), gBase = (1 + g) / 2 ∧ MeasureTheory.IsProbabilityMeasure Pbase ∧ IsStationaryLaw Pbase ∧ IsUnitRangeLaw Pbase ∧ CoarseEllipticityDagger Pbase gBase Ebase PsiBase Kbase Sbase ∧ annealedContrast Pbase 0 - 1 ≤ cStar ∧ blockContrast Ebase ≤ 1 + cSc ∧ (∀ (j : ℕ), annealedContrast Pbase ↑j = annealedContrast P ↑(nBase + j)) ∧ (∀ (j : ℕ), annealedBlock Pbase (centeredCube d ↑j) = annealedBlock P (centeredCube d ↑(nBase + j))) ∧ 3 ^ nBase ≤ (2 + aspectRatio E * K) ^ Crebase ∧ 2 + aspectRatio Ebase * Kbase ≤ (2 + aspectRatio E * K) ^ Crebase) (hCoupled : ∃ (cd : ℝ), 0 < cd ∧ ∀ g ∈ Set.Ico 0 1, ∀ (alpha : ℝ), 0 < alpha → ∃ (Cmix : ℝ) (cMix : ℝ) (kappa : ℝ) (delta : ℝ), 0 < Cmix ∧ 0 < cMix ∧ 0 < kappa ∧ delta ∈ Set.Ioo 0 1 ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Psi : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (Abar : BlockMat d) (Nann : ℕ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P g E Psi K S → IsSymmetricBlockMat Abar → Book.Ch02.BlockPosDef Abar → (∀ (j : ℕ), annealedContrast P ↑(Nann + j) - 1 ≤ 3 ^ (-alpha * ↑j)) → (∀ (j : ℕ), BlockMatLoewnerLE Abar (annealedBlock P (centeredCube d ↑(Nann + j))) ∧ BlockMatLoewnerLE (annealedBlock P (centeredCube d ↑(Nann + j))) (blockScale (1 + 6 * 3 ^ (-alpha * ↑j)) Abar)) → ∃ (W : CoupledMixingScaleWitness P (fun (m : ℕ) (a : CoeffSpace d) => quenchedBlockRow ((1 + 3 * g) / 4) Abar (max 1 (S a / 3 ^ Nann)) (physicalScaleCoefficient Nann a) m) cMix cd (↑d - 2 * g) kappa delta), W.normalization ≤ (2 + aspectRatio E * K) ^ Cmix) : ∃ (cd : ℝ), 0 < cd ∧ ∀ g ∈ Set.Ico 0 1, ∃ (C : ℝ) (cSrc : ℝ) (kappa : ℝ) (delta : ℝ), 0 < C ∧ 0 < cSrc ∧ 0 < kappa ∧ delta ∈ Set.Ioo 0 1 ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Psi : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P g E Psi K S → ∃ (Abar : BlockMat d) (Nann : ℕ) (alpha : ℝ) (Lpoly : ℝ) (Ssrc : CoeffSpace d → ℝ) (X : CoeffSpace d → ℝ), 0 < alpha ∧ IsSymmetricBlockMat Abar ∧ Book.Ch02.BlockPosDef Abar ∧ (∀ (m : ℕ), BlockMatLoewnerLE Abar (annealedBlock P (centeredCube d ↑m))) ∧ (∀ (m : ℕ), BlockMatLoewnerLE (blockSharp (annealedBlock P (centeredCube d ↑m))) Abar) ∧ (∀ (j : ℕ), annealedContrast P ↑(Nann + j) - 1 ≤ 3 ^ (-alpha * ↑j)) ∧ (∀ (a : CoeffSpace d), Ssrc a = max 1 (S a / 3 ^ Nann)) ∧ 1 ≤ Lpoly ∧ Lpoly ≤ (2 + aspectRatio E * K) ^ C ∧ Measurable Ssrc ∧ (∀ (a : CoeffSpace d), 1 ≤ Ssrc a) ∧ Measurable X ∧ (∀ (a : CoeffSpace d), 1 ≤ X a) ∧ (∀ (a : CoeffSpace d), S a ≤ X a) ∧ (∀ (t : ℝ), 1 ≤ t → P.real {a : CoeffSpace d | C * Lpoly * t ≤ X a} ≤ Real.exp (-cd * t ^ (↑d - 2 * g)) + (Psi (cSrc * t))⁻¹) ∧ ∃ (OmegaEnd : Set (CoeffSpace d)), MeasurableSet OmegaEnd ∧ P.real OmegaEnd = 1 ∧ (∀ (z : Fin d → ℤ), translateCoeff z ⁻¹' OmegaEnd = OmegaEnd) ∧ ∀ a ∈ OmegaEnd, HasAllLaterPhysicalBlockRow ((1 + 3 * g) / 4) kappa delta Abar S X a

The polynomial entry theorem, the annealed contrast endpoint, the triadic rebase, and one coupled quenched witness produce the physical quenched minimal scale. The row coefficient is the small threshold delta, rather than the larger constant used to combine the two tails.