CutoffBaseTailArithmetic

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

Scalar amplitudes for the cutoff base-case tails

This module puts the plateau-plus-mass response estimate into the exact scalar forms consumed by the three corrected Section 3.2 base-case error clauses. It first extracts dimension-only square-root constants for the deterministic plateau and the weighted Gamma_1 mass tail. It then proves their all-scale normal forms and specializes the common scale core at m** and m*.

Main results

• cutoffMassSqrtConst, cutoffPlateauSqrtConst, and cutoffBaseSqrtConst are positive dimension-only constants.
• sqrt_cutoffMassTailScale_le_allScale and sqrt_cutoffPlateauAmplitude_le_allScale give the two all-scale square-root amplitudes.
• The corresponding _le_mStarStar results give the exact m <= m** amplitudes.
• sqrt_cutoffMassTailScale_le_mStar and sqrt_cutoffPlateauAmplitude_le_one_of_le_mStar give the random and deterministic parts of the shifted m <= m* estimate.

Dimension-only constants

noncomputable def Algsuperdiff.Section3.Provider.Base.cutoffMassSqrtConst (d : ℕ) : ℝ

Dimension-only square-root coefficient of the weighted Gamma_1 mass tail.

Equations

• Algsuperdiff.Section3.Provider.Base.cutoffMassSqrtConst d = √(HCPolySupport.IndependentSums.gammaTriangleConst 1 * Algsuperdiff.Section3.Provider.Stream.cutoffFrobeniusMassFiniteConst d)

theorem Algsuperdiff.Section3.Provider.Base.cutoffMassSqrtConst_pos (d : ℕ) : 0 < cutoffMassSqrtConst d

The weighted-mass square-root coefficient is strictly positive.

noncomputable def Algsuperdiff.Section3.Provider.Base.cutoffPlateauSqrtConst (d : ℕ) : ℝ

Dimension-only square-root envelope for the deterministic plateau.

Equations

• Algsuperdiff.Section3.Provider.Base.cutoffPlateauSqrtConst d = √(Algsuperdiff.Section3.Provider.Disorder.cstarPlusUpperBound d)

theorem Algsuperdiff.Section3.Provider.Base.cutoffPlateauSqrtConst_pos (d : ℕ) : 0 < cutoffPlateauSqrtConst d

The deterministic-plateau square-root envelope is strictly positive.

noncomputable def Algsuperdiff.Section3.Provider.Base.cutoffBaseSqrtConst (d : ℕ) : ℝ

Common dimension-only coefficient before the universal probabilistic square-root conversion.

Equations

• Algsuperdiff.Section3.Provider.Base.cutoffBaseSqrtConst d = Algsuperdiff.Section3.Provider.Base.cutoffPlateauSqrtConst d + Algsuperdiff.Section3.Provider.Base.cutoffMassSqrtConst d

theorem Algsuperdiff.Section3.Provider.Base.cutoffBaseSqrtConst_pos (d : ℕ) : 0 < cutoffBaseSqrtConst d

The common cutoff base coefficient is strictly positive.

Scalar square-root normal forms

theorem Algsuperdiff.Section3.Provider.Base.sqrt_cutoffMassTailScale_le_allScale {d : ℕ} (M : ABKModel d) (m : ℤ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) : √(HCPolySupport.IndependentSums.gammaTriangleConst 1 * cutoffMassLinearWeightedScale M m s) ≤ cutoffMassSqrtConst d * M.nu⁻¹ * (√M.gamma)⁻¹ * 3 ^ (M.gamma * ↑m) * √(baseLoss d s)

The square root of the weighted Gamma_1 tail scale has the exact all-scale nu⁻¹ gamma⁻¹⁄² 3^(gamma m) sqrt(baseLoss) form.

theorem Algsuperdiff.Section3.Provider.Base.sqrt_cutoffPlateauAmplitude_le_allScale {d : ℕ} (M : ABKModel d) (m : ℤ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) : √(cutoffPlateauAmplitude M m) ≤ cutoffPlateauSqrtConst d * M.nu⁻¹ * (√M.gamma)⁻¹ * 3 ^ (M.gamma * ↑m) * √(baseLoss d s)

The deterministic plateau has the same all-scale core as the weighted mass, with a dimension-only coefficient.

Landmark specializations

theorem Algsuperdiff.Section3.Provider.Base.sqrt_cutoffMassTailScale_le_mStarStar {d : ℕ} (M : ABKModel d) (m : ℤ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) (hm : m ≤ mStarStar M) : √(HCPolySupport.IndependentSums.gammaTriangleConst 1 * cutoffMassLinearWeightedScale M m s) ≤ cutoffMassSqrtConst d * (√(Disorder.cstarPlus M))⁻¹ * √M.gamma * √(baseLoss d s)

Below m**, the weighted-mass square root has the corrected base-case cstarPlus⁻¹⁄² gamma¹⁄² sqrt(baseLoss) scale.

theorem Algsuperdiff.Section3.Provider.Base.sqrt_cutoffPlateauAmplitude_le_mStarStar {d : ℕ} (M : ABKModel d) (m : ℤ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) (hm : m ≤ mStarStar M) : √(cutoffPlateauAmplitude M m) ≤ cutoffPlateauSqrtConst d * (√(Disorder.cstarPlus M))⁻¹ * √M.gamma * √(baseLoss d s)

Below m**, the deterministic plateau obeys the same corrected base-case scale as the weighted mass.

theorem Algsuperdiff.Section3.Provider.Base.sqrt_cutoffMassTailScale_le_mStar {d : ℕ} (M : ABKModel d) (m : ℤ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) (hm : m ≤ mStar M) : √(HCPolySupport.IndependentSums.gammaTriangleConst 1 * cutoffMassLinearWeightedScale M m s) ≤ cutoffMassSqrtConst d * (√(Disorder.cstarPlus M))⁻¹ * √(baseLoss d s)

Below m*, the weighted-mass square root has the corrected shifted base-case scale.

theorem Algsuperdiff.Section3.Provider.Base.sqrt_cutoffPlateauAmplitude_le_one_of_le_mStar {d : ℕ} (M : ABKModel d) (m : ℤ) (hm : m ≤ mStar M) : √(cutoffPlateauAmplitude M m) ≤ 1

Below m*, the deterministic plateau has square root at most one, which fits inside the frozen deterministic shift 2.