CompactResolvent

formal source

 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 :