Coarse-graining support: Support.Book.Ch05.Theorems.Section57.BadScalePairCollapse

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

Deterministic fixed-pair exponent collapse

This file contains the deterministic lower bounds on the raw tail parameters from BadScalePairTwoBranch. These are the first two manuscript-facing collapses: the localized top range gives the b*q concentration scale, and the crude bottom range gives the t*q discount scale.

theorem HCPolySupport.Book.Ch05.Section57.highTop_tailParameter_lower_bound {d : ℕ} [NeZero d] {K Cfluct θ a t α : ℝ} {q m n : ℕ} (hK : 0 < K) (hCfluct : 0 < Cfluct) (hθ : 0 < θ) (ha : 0 < a) (hαt : α < t) (hαb : α < ↑d / 2) (hαharm : α * (1 + ↑d / 2 / a) < ↑d / 2) (hell : selectedBadPairScale K a t α q m n < n) (hqn : q ≤ n) (hnm : n < m) : have x := α * ↑(m - q) - t * ↑(m - n); have ell := selectedBadPairScale K a t α q m n; have b := ↑d / 2; have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); have c := min (t - α) (min (b - α) (min ((t - α) * (1 + b / a)) (b - α * (1 + b / a)))); have highScale := Cfluct * 3 ^ (-↑d / 2 * ↑(n - ell)) * θ ^ 2; have T := 3 ^ (-x); have highLam := T / (2 * K * highScale); have A := 3 ^ (b * ↑q - b * (L + 1)) / (2 * K * Cfluct * θ ^ 2); have ρ := 3 ^ c; A * ρ ^ (m - q) ≤ highLam

In the localized range with q ≤ n, the raw high-branch tail parameter dominates the manuscript b*q scale, up to a summable geometric weight in m-q.

theorem HCPolySupport.Book.Ch05.Section57.crudeBottom_tailParameter_lower_bound {K C θ a t α : ℝ} {q m n : ℕ} (hK : 0 < K) (hC : 0 < C) (hθ : 0 < θ) (ha : 0 < a) (ht : 0 < t) (hαt : α < t) (hnell : n ≤ selectedBadPairScale K a t α q m n) (hnq : n ≤ q) (hqm : q ≤ m) : have x := α * ↑(m - q) - t * ↑(m - n); have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); have crudeScale := K * (C * θ ^ 2); have T := 3 ^ (-x); have crudeLam := T / crudeScale; have A := 3 ^ (t * ↑q - t * (L + 1)) / (K * C * θ ^ 2); have ρ := 3 ^ (t - α); A * ρ ^ (m - q) ≤ crudeLam

In the crude bottom range, the raw crude tail parameter dominates the manuscript t*q scale, up to a summable geometric weight in m-q.

theorem HCPolySupport.Book.Ch05.Section57.highBottom_tailParameter_interpolation_lower_bound {d : ℕ} [NeZero d] {K Cfluct θ a t α : ℝ} {q m n : ℕ} (hK : 0 < K) (hCfluct : 0 < Cfluct) (hθ : 0 < θ) (ha : 0 < a) (ht : 0 < t) (hαt : α < t) (hell : selectedBadPairScale K a t α q m n < n) (hnq : n ≤ q) (hqm : q ≤ m) : have x := α * ↑(m - q) - t * ↑(m - n); have ell := selectedBadPairScale K a t α q m n; have b := ↑d / 2; have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); have highScale := Cfluct * 3 ^ (-↑d / 2 * ↑(n - ell)) * θ ^ 2; have T := 3 ^ (-x); have highLam := T / (2 * K * highScale); have A := 3 ^ (b * ↑q - (b - t) * ↑(q - n) + (t - α) * ↑(m - q) - b * (L + 1)) / (2 * K * Cfluct * θ ^ 2); A ≤ highLam

In the mixed range n <= q where the localized scale is available, the localized tail parameter has the exact interpolating exponent between the concentration gain at scale n and the discount gain from q - n. This is kept separate from theorem-facing tails so that no weakened leading exponent is exposed as a public endpoint.

theorem HCPolySupport.Book.Ch05.Section57.crudeBottom_tailParameter_discount_lower_bound {K C θ t α : ℝ} {q m n : ℕ} (hK : 0 < K) (hC : 0 < C) (hθ : 0 < θ) (hnq : n ≤ q) (hqm : q ≤ m) : have x := α * ↑(m - q) - t * ↑(m - n); have crudeScale := K * (C * θ ^ 2); have T := 3 ^ (-x); have crudeLam := T / crudeScale; have A := 3 ^ (t * ↑(q - n) + (t - α) * ↑(m - q)) / (K * C * θ ^ 2); A ≤ crudeLam

In the bottom range n <= q, the crude tail parameter has the exact discount exponent. This lemma does not require the complementary condition n <= ell; it is the crude half of the mixed-branch comparison.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighBottomPairEvent_quenchedProbeEnvelope_le_soft_high {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Centry : ℝ) (a : ℝ), 0 < Cfluct ∧ 0 < Centry ∧ 0 < a ∧ ∀ {t αbad : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {q m n : ℕ}, have K := quenchedProbeEnvelopeConst d; have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω; have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n); have S := Finset.univ; have b := ↑d / 2; have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); have tau := min σ 2; have pref := ↑S.card * ↑D.card; have highA := 3 ^ (b * ↑q - (b - t) * ↑(q - n) + (t - αbad) * ↑(m - q) - b * (L + 1)) / (2 * K * Cfluct * hΓ.thetaHat ^ 2); n < m → q ≤ m → 0 < t → αbad < t → MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) ≤ softPairTail pref highA tau

Direct localized estimate for the mixed bottom branch.

The conclusion keeps the exact interpolating exponent. This is stronger than the two-branch soft estimate when the localized branch is the better one, and it is used later only before the final endpoint collapse.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighBottomPairEvent_quenchedProbeEnvelope_le_soft_crude {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Ccrude : ℝ) (Centry : ℝ) (a : ℝ), 0 < Ccrude ∧ 0 < Centry ∧ 0 < a ∧ ∀ {t αbad : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {q m n : ℕ}, have K := quenchedProbeEnvelopeConst d; have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω; have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n); have S := Finset.univ; have pref := ↑S.card * ↑D.card; have crudeA := 3 ^ (t * ↑(q - n) + (t - αbad) * ↑(m - q)) / (K * Ccrude * hΓ.thetaHat ^ 2); n < m → q ≤ m → αbad < t → MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) ≤ softPairTail pref crudeA σ

Direct crude estimate for the mixed bottom branch.

This is independent of the selected localized scale: the event is a subset of the bad-pair event, and the unit-scale crude input supplies the discount parameter in the bottom range.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighBottomPairEvent_quenchedProbeEnvelope_le_soft_mixed {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Ccrude : ℝ) (Centry : ℝ) (a : ℝ), 0 < Cfluct ∧ 0 < Ccrude ∧ 0 < Centry ∧ 0 < a ∧ ∀ {t αbad : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {q m n : ℕ}, have K := quenchedProbeEnvelopeConst d; have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω; have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n); have S := Finset.univ; have b := ↑d / 2; have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1); have tau := min σ 2; have pref := ↑S.card * ↑D.card; have highA := 3 ^ (b * ↑q - (b - t) * ↑(q - n) + (t - αbad) * ↑(m - q) - b * (L + 1)) / (2 * K * Cfluct * hΓ.thetaHat ^ 2); have crudeA := 3 ^ (t * ↑(q - n) + (t - αbad) * ↑(m - q)) / (K * Ccrude * hΓ.thetaHat ^ 2); n < m → q ≤ m → 0 < t → αbad < t → MeasureTheory.Measure.real P (highBottomPairEvent Hshift K a t αbad q m n) ≤ softPairTail pref highA tau + softPairTail pref crudeA σ

Exact probability-level estimate for the mixed bottom localized branch.

This is the delicate n <= q and ell < n region. The conclusion deliberately keeps the two honest raw mechanisms visible: the localized interpolation scale and the crude discount scale. The theorem-facing bad-scale tail must still collapse these without turning the localized interpolation term into a leading c*q estimate.