CstarPlusUpperBound

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

A dimension-only upper bound on cstarPlus

The clean Section 3 convention is

cstarPlus M = E[‖j_0(0)‖_F^2] / log 3.

The value term of the J2 observable dominates the operator norm of j_0(0). The Frobenius/operator comparison therefore bounds the origin Frobenius mass by d^2 E[X^2], where X is the J2 observable. Its normalized Gaussian tail gives E[X^2] <= 1 + exp (-1). This module packages the resulting explicit dimension-only envelope, with a harmless additive 1 so that the envelope is positive even before imposing the standing model's dimension lower bound.

Sources and conventions

• ABK26, e.kn.reg.ass, ABK26: the J2 observable and its normalized Gaussian tail.
• The clean convention divides the origin Frobenius mass by log 3; this is the already-verified definition Section3.Disorder.cstarPlus.

Main results

• cstarPlusUpperBound: an explicit positive function of d only.
• cstarPlus_le_cstarPlusUpperBound: every standing ABK model obeys that bound, using no additional hypothesis.

noncomputable def Algsuperdiff.Section3.Provider.Disorder.cstarPlusUpperBound (d : ℕ) : ℝ

A positive dimension-only envelope for the normalized Frobenius origin mass.

Equations

• Algsuperdiff.Section3.Provider.Disorder.cstarPlusUpperBound d = 1 + ↑d ^ 2 * (1 + Real.exp (-1)) / Real.log 3

theorem Algsuperdiff.Section3.Provider.Disorder.cstarPlusUpperBound_nonneg (d : ℕ) : 0 ≤ cstarPlusUpperBound d

The dimension-only envelope is nonnegative.

theorem Algsuperdiff.Section3.Provider.Disorder.cstarPlusUpperBound_pos (d : ℕ) : 0 < cstarPlusUpperBound d

The harmless additive constant makes the envelope strictly positive for every natural dimension.

theorem Algsuperdiff.Section3.Provider.Disorder.cstarPlus_le_cstarPlusUpperBound {d : ℕ} (M : ABKModel d) : Disorder.cstarPlus M ≤ cstarPlusUpperBound d

J2 alone bounds the normalized Frobenius constant by the explicit dimension-only envelope.