  54theorem denseDomain_nonempty : denseDomain.Nonempty := ⟨0, trivial⟩
  55
  56/-- The dense domain contains every finitely-supported state. -/
  57theorem denseDomain_mem (f : StateSpace) : f ∈ denseDomain := trivial
  58
  59/-! ## Cost potential growth bound
  60
  61For the cost operator to have a discrete spectrum, the diagonal cost
  62potential `D(v) = J(toRat v)` must grow as `|v| → ∞`.  Since `J(p) ~ p/2`
  63and `c(v) = Σ_p v_p J(p)`, the growth rate depends on the multiplicative
  64index norm.
  65-/
  66
  67/-- A growth bound for the cost potential at a multiplicative index `v`
  68    with respect to a chosen norm `‖v‖`.  We state the abstract bound
  69    rather than fixing a specific norm. -/
  70structure CostPotentialBound (norm : MultIndex → ℝ) (R : ℝ) (α : ℝ) : Prop where
  71  growth : ∀ v : MultIndex, R * norm v ^ α ≤ costAt v
  72
  73/-- Sub-conjecture C.2 (precondition): the cost potential grows linearly
  74    in the L¹-norm of the multiplicative index.
  75
  76    Specifically: there exists `R > 0` such that
  77    `costAt v ≥ R * Σ_p |v_p|`
  78    for every `v : MultIndex`.
  79
  80    This holds because `J(p) ≥ J(2) = 1/4` for all primes `p ≥ 2`, so
  81    `c(v) = Σ_p v_p J(p) ≥ Σ_p v_p · J(2)` when all `v_p ≥ 0`.  The
  82    general case (allowing negative `v_p`) requires the symmetry
  83    `J(1/p) = J(p)`. -/
  84def CostPotentialLinearGrowth : Prop :=
  85  ∃ R : ℝ, 0 < R ∧ ∀ v : MultIndex,
  86    R * (v.support.sum (fun p => |(v p : ℝ)|)) ≤ costAt v
  87

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.