LowerSmallScale

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The deterministic small-scale branch of the lower coarse-ellipticity bound

This file proves the m <= mStar M branch used inside the proof of the lower half of Frozen.Section3.coarse_ellipticity_bounds. It is an internal branch theorem, not a replacement for that frozen theorem and not a closed source node. In the eventual source-facing proof, m <= mStar M is introduced by a case split and 8 <= C is discharged by the dimension-only choice of the single outer constant; neither becomes a premise of the frozen declaration.

The argument is deterministic. Uniform ellipticity bounds every inverse starred descendant norm by nu^-1. The normalized geometric depth weights then give the same bound for every finite exponent, while the infinity endpoint follows from its decaying weights. Below mStar, the annealed plateau is at most 2 * nu, so the whole lower observable is at most 2. The frozen lower profile is at least 2 once its common constant is at least 8; hence the zero random witness supplies the exact lower-family carrier.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.lambdaSqFinite_inv_le_of_forall_maxDescendant_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {s q B : ℝ} (hs : 0 < s) (hq : 0 < q) (hB : 0 ≤ B) (hmax : ∀ (n : ℕ), HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) a ≤ B) : (HCPolySupport.Book.Ch02.lambdaSqFinite Q s q a)⁻¹ ≤ B

A uniform bound on all inverse starred descendant norms bounds the finite multiscale inverse ellipticity by the same constant.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cutoffLowerEllipticityInv_le_nu_inv {d : ℕ} (M : ABKModel d) (domainScale cutoffScale : ℤ) {s : ℝ} (hs : 0 < s) (q : CoarseEllipticityExponent) (omega : Cutoff.CutoffSample d) : Observable.cutoffLowerEllipticityInv M domainScale cutoffScale s hs q omega ≤ M.nu⁻¹

Every lower coarse-ellipticity observable of the cutoff is bounded by nu^-1, uniformly in both admissible exponent endpoints and both scales.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cutoffLowerEllipticityInv_mul_sigmaBar_le_two_of_le_mStar {d : ℕ} (M : ABKModel d) (m : ℤ) (hm : m ≤ mStar M) {s : ℝ} (hs : 0 < s) (q : CoarseEllipticityExponent) (L : ℤ) (omega : Cutoff.CutoffSample d) : Observable.cutoffLowerEllipticityInv M m L s hs q omega * ↑(Annealed.sigmaBar M (m - 1)) ≤ 2

Below mStar, the lower observable normalized by the previous annealed diffusivity is bounded pointwise by 2, uniformly in the cutoff level.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.two_le_lowerEllipticityProfile_of_eight_le {C gamma s : ℝ} (hC : 8 ≤ C) (hgamma : 0 < gamma) (hhalf : gamma / 2 < s) (q : CoarseEllipticityExponent) : 2 ≤ lowerEllipticityProfile C gamma s q

On the frozen source window, the lower deterministic profile is at least 2 whenever its common constant is at least 8.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.coarse_ellipticity_lower_of_le_mStar_of_eight_le {d : ℕ} (M : ABKModel d) (m : ℤ) (hm : m ≤ mStar M) {C : ℝ} (hC : 8 ≤ C) (E : { E : ℝ // 1 ≤ E }) (sigma : ℝ) (hsigma : sigma ∈ Set.Ioc 0 (1 / 2)) (q : CoarseEllipticityExponent) (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(C⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1) : Probability.IsLowerIntegerFamilyOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) (fun (L : ℤ) (omega : Cutoff.CutoffSample d) => Observable.cutoffLowerEllipticityInv M m L s ⋯ q omega * ↑(Annealed.sigmaBar M (m - 1))) (m - 1) (lowerEllipticityProfile C M.gamma s q) (Real.exp (-(C⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))

The exact lower-family conclusion in the m <= mStar M branch. The witness is identically zero; no induction-state or gate proposition is assumed or hidden in this result.