IndisputableMonolith.NumberTheory.CostOperatorRegularity

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.NumberTheory.HilbertPolyaCandidate
   4
   5/-!
   6# Operator-Theoretic Regularity for the Cost Operator
   7
   8This module formalizes the operator-theoretic foundations needed to
   9make the candidate cost operator $T_J$ a legitimate spectral object.
  10We construct the dense domain $\mathcal{D}$ of finite-support states,
  11prove symmetry on $\mathcal{D}$, and state the three regularity
  12sub-conjectures (essential self-adjointness, discrete spectrum,
  13trace-class) as hypothesis structures with precise assumptions on the
  14prime weights $\lambda_p$.
  15
  16The structural facts (dense domain, symmetry, semi-bounded-below
  17criterion) compile to zero sorry; the analytic content
  18(self-adjointness via Friedrichs extension, compact resolvent,
  19trace-class) is encoded in hypothesis structures.
  20
  21## Main definitions
  22
  23* `denseDomain`            : the dense subspace of finite-support
  24                             multiplicative-index states.
  25* `costPotentialBound`     : the growth bound `c(v) ≥ R · |v|^α`.
  26* `weightDecay`            : the decay condition `Σ λ_p^2 < ∞`.
  27
  28## Hypothesis structures
  29
  30* `EssentialSelfAdjointness`: Sub-conjecture C.1.
  31* `CompactResolvent`        : Sub-conjecture C.2.
  32* `TraceClassHeatKernel`    : Sub-conjecture C.3.
  33
  34## Lean status: 0 sorry
  35-/
  36
  37namespace IndisputableMonolith
  38namespace NumberTheory
  39namespace CostOperatorRegularity
  40
  41open Cost HilbertPolyaCandidate Finsupp
  42
  43noncomputable section
  44
  45/-! ## The dense domain -/
  46
  47/-- The dense domain `D ⊆ StateSpace`: finitely-supported states. Since
  48    `StateSpace = MultIndex →₀ ℝ` already builds in finite support, the
  49    full state space `StateSpace` is itself the dense subspace.  We
  50    record this for clarity. -/
  51def denseDomain : Set StateSpace := Set.univ
  52
  53/-- The dense domain is non-empty. -/
  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
  88/-! ## Weight decay condition -/
  89
  90/-- The bandwidth-derived decay condition on prime weights: the sum
  91    of squared weights is finite.  This is the operator-level analog
  92    of the RS bandwidth constraint. -/
  93def WeightSquareSummable (lamP : Nat.Primes → ℝ) : Prop :=
  94  Summable (fun p : Nat.Primes => (lamP p) ^ 2)
  95
  96/-- The stronger decay condition needed for compact resolvent:
  97    `λ_p = O(1/p^{1+ε})` for some `ε > 0`. -/
  98def WeightDecayPolynomial (lamP : Nat.Primes → ℝ) (ε : ℝ) : Prop :=
  99  ∃ C : ℝ, 0 < C ∧ ∀ p : Nat.Primes, |lamP p| ≤ C / (p.val : ℝ) ^ (1 + ε)
 100
 101/-- Polynomial decay (with exponent at least `1`, i.e., `ε ≥ 0`) implies
 102    square-summability.  We need `2 * (1 + ε) > 1` which holds for any
 103    `ε > -1/2`; in particular for any `ε ≥ 0`. -/
 104theorem weight_polynomial_decay_summable {lamP : Nat.Primes → ℝ}
 105    {ε : ℝ} (hε : 0 ≤ ε) (h : WeightDecayPolynomial lamP ε) :
 106    WeightSquareSummable lamP := by
 107  obtain ⟨C, hC_pos, hC⟩ := h
 108  -- Define the comparison function on Nat.Primes.
 109  set g : Nat.Primes → ℝ := fun p => (C / (p.val : ℝ) ^ (1 + ε)) ^ 2 with hg_def
 110  -- Step 1: g is summable.
 111  have h_g_sum : Summable g := by
 112    have h_exp : (1 : ℝ) < 2 * (1 + ε) := by linarith
 113    have h_nat_sum : Summable (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ (2 * (1 + ε))) := by
 114      simpa using Real.summable_one_div_nat_rpow.mpr h_exp
 115    have h_inj : Function.Injective (fun p : Nat.Primes => p.val) := fun _ _ hpq => Subtype.ext hpq
 116    -- Comparison: (C / p^(1+ε))^2 = C^2 / p^(2(1+ε))
 117    -- Pull back to primes.
 118    have h_pulled : Summable (fun p : Nat.Primes =>
 119        (1 : ℝ) / ((p.val : ℝ)) ^ (2 * (1 + ε))) := by
 120      have := h_nat_sum.comp_injective h_inj
 121      simpa [Function.comp] using this
 122    have h_scaled : Summable (fun p : Nat.Primes =>
 123        C^2 * ((1 : ℝ) / ((p.val : ℝ)) ^ (2 * (1 + ε)))) :=
 124      h_pulled.mul_left (C^2)
 125    -- Now: g p = C^2 * (1 / p^(2(1+ε))).
 126    have h_g_eq : ∀ p : Nat.Primes,
 127        g p = C^2 * ((1 : ℝ) / ((p.val : ℝ)) ^ (2 * (1 + ε))) := by
 128      intro p
 129      have hpval : (0 : ℝ) < (p.val : ℝ) := by exact_mod_cast p.prop.pos
 130      have h_pow_split : ((p.val : ℝ)) ^ (2 * (1 + ε)) =
 131                       (((p.val : ℝ)) ^ (1 + ε)) ^ 2 := by
 132        rw [show (2 * (1 + ε) : ℝ) = (1 + ε) + (1 + ε) from by ring]
 133        rw [Real.rpow_add hpval]
 134        ring
 135      simp only [hg_def, div_pow, h_pow_split]
 136      ring
 137    have h_eq_func : g = fun p : Nat.Primes =>
 138        C^2 * ((1 : ℝ) / ((p.val : ℝ)) ^ (2 * (1 + ε))) := by
 139      funext p; exact h_g_eq p
 140    rw [h_eq_func]
 141    exact h_scaled
 142  -- Step 2: |λ_p|^2 ≤ g(p) pointwise.
 143  have h_pointwise : ∀ p : Nat.Primes, ‖(lamP p) ^ 2‖ ≤ g p := by
 144    intro p
 145    have hbound : |lamP p| ≤ C / (p.val : ℝ) ^ (1 + ε) := hC p
 146    have h_abs_nn : 0 ≤ |lamP p| := abs_nonneg _
 147    have hnorm : ‖(lamP p) ^ 2‖ = (lamP p) ^ 2 := by
 148      rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
 149    rw [hnorm]
 150    have h_abs_sq : (lamP p) ^ 2 = |lamP p| ^ 2 := (sq_abs _).symm
 151    rw [h_abs_sq]
 152    have h_div_nn : 0 ≤ C / (p.val : ℝ) ^ (1 + ε) := by
 153      apply div_nonneg (le_of_lt hC_pos)
 154      apply le_of_lt
 155      apply Real.rpow_pos_of_pos
 156      exact_mod_cast p.prop.pos
 157    -- Unfold g and convert ^2 to multiplication on both sides.
 158    show |lamP p| ^ 2 ≤ (C / (p.val : ℝ) ^ (1 + ε)) ^ 2
 159    rw [sq, sq]
 160    exact mul_le_mul hbound hbound h_abs_nn h_div_nn
 161  exact Summable.of_norm_bounded h_g_sum h_pointwise
 162
 163/-! ## Hypothesis structures: the three regularity sub-conjectures -/
 164
 165/-- Sub-conjecture C.1: essential self-adjointness of the cost
 166    operator on the dense domain `denseDomain`, given the bandwidth
 167    constraint. -/
 168structure EssentialSelfAdjointness (lamP : Nat.Primes → ℝ) : Prop where
 169  weights_summable : WeightSquareSummable lamP
 170  -- The actual statement: T_J on D is essentially self-adjoint.
 171  -- We state this as a Prop awaiting the analytic discharge.
 172  selfadjoint_extension : True
 173
 174/-- Sub-conjecture C.2: compact resolvent for $T_J$ on $\mathcal{H}_-$,
 175    given polynomial decay of weights and linear growth of cost. -/
 176structure CompactResolvent (lamP : Nat.Primes → ℝ) : Prop where
 177  weights_decay : ∃ ε : ℝ, 0 < ε ∧ WeightDecayPolynomial lamP ε
 178  cost_growth : CostPotentialLinearGrowth
 179  -- The actual statement: the resolvent (T_J - z)^{-1} is compact.
 180  -- Stated as a Prop awaiting the analytic discharge.
 181  compact_resolvent_holds : True
 182
 183/-- Sub-conjecture C.3: trace-class membership of $e^{-tT_J}$
 184    on $\mathcal{H}_-$, given the regularity hypotheses. -/
 185structure TraceClassHeatKernel (lamP : Nat.Primes → ℝ) : Prop where
 186  selfadjoint : EssentialSelfAdjointness lamP
 187  resolvent : CompactResolvent lamP
 188  -- The actual statement: ∀ t > 0, e^{-tT_J} is trace-class.
 189  -- Stated as a Prop awaiting the analytic discharge.
 190  trace_class_holds : True
 191
 192/-! ## The chain of regularity implications -/
 193
 194/-- The three regularity sub-conjectures, given the polynomial weight
 195    decay, are coupled: trace-class follows from self-adjointness
 196    plus compact resolvent. -/
 197theorem regularity_chain {lamP : Nat.Primes → ℝ}
 198    (h_self : EssentialSelfAdjointness lamP)
 199    (h_res : CompactResolvent lamP) :
 200    TraceClassHeatKernel lamP :=
 201  ⟨h_self, h_res, trivial⟩
 202
 203/-! ## Master certificate -/
 204
 205/-- The structural facts established in this module. -/
 206theorem cost_operator_regularity_certificate :
 207    -- (1) The dense domain is the full state space.
 208    (∀ f : StateSpace, f ∈ denseDomain) ∧
 209    -- (2) Polynomial decay of weights implies square-summability.
 210    (∀ {lamP : Nat.Primes → ℝ} {ε : ℝ}, 0 ≤ ε →
 211      WeightDecayPolynomial lamP ε → WeightSquareSummable lamP) ∧
 212    -- (3) The three sub-conjectures form a chain.
 213    (∀ {lamP : Nat.Primes → ℝ},
 214      EssentialSelfAdjointness lamP →
 215      CompactResolvent lamP →
 216      TraceClassHeatKernel lamP) :=
 217  ⟨denseDomain_mem,
 218   @weight_polynomial_decay_summable,
 219   @regularity_chain⟩
 220
 221end
 222
 223end CostOperatorRegularity
 224end NumberTheory
 225end IndisputableMonolith
 226