DimensionFloor

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

The dimension-floor normalization of the coarse-ellipticity constant

The constant of p.cg.ellipticity.bounds may be raised to satisfy 1 ≤ Ccg. The Section 3.4 principal-response consumers need the same constant to clear the dimension floor (d : ℝ) ^ 6 as well: the event constant they feed to the sensitivity gate is 2 * Ccg, and that gate reads 2 * (d : ℝ) ^ 6 ≤ 2 * Ccg * sensitivityConstMax d ^ 2.

An existential cannot expose any lower bound on its own hidden witness, so the floor is installed by the same monotonicity that installs 1: every slot of the statement is weaker at a larger constant, and coarse_ellipticity_bounds_body_of_legs re-derives the ∀-body at max C (max 1 ((d : ℝ) ^ 6)) from the two legs at C. Neither the frozen statement nor its proof changes.

The predecessor

Algsuperdiff.Frozen.Section3.coarse_ellipticity_bounds is applied internally here, so no premise of that shape survives on the surface below. It is proved on this branch, so this module's export is sorry-free.

References

• ABK26, p.cg.ellipticity.bounds, statement.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.coarse_ellipticity_bounds_dim_floor (d : ℕ) : ∃ (Ccg : ℝ), 1 ≤ Ccg ∧ ↑d ^ 6 ≤ Ccg ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m - 1) E → ∀ sigma ∈ Set.Ioc 0 (1 / 2), max (Real.exp (Ccg / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (q : CoarseEllipticityExponent) (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Ccg⁻¹ * (↑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 Ccg M.gamma s q) (Real.exp (-(Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) ∧ Probability.IsDeterministicShiftTwoTermOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) (fun (omega : Cutoff.CutoffSample d) => Observable.cutoffUpperEllipticity M m m s ⋯ q omega * (↑(Annealed.sigmaBar M (m - 1)))⁻¹) Ccg (Ccg * (Disorder.cstar M)⁻¹ * s * M.gamma * (2 * s - M.gamma)⁻¹ ^ 3) (Real.exp (-(Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))

The floor-normalized constant selection. The coarse-ellipticity statement holds at a constant satisfying 1 ≤ Ccg and (d : ℝ) ^ 6 ≤ Ccg, namely max C (max 1 ((d : ℝ) ^ 6)) for the constant C the frozen statement provides.