TraceClassHeatKernel
plain-language theorem explainer
The TraceClassHeatKernel structure encodes sub-conjecture C.3 by bundling essential self-adjointness and compact resolvent of the cost operator T_J for given prime weights, with the trace-class property of the heat kernel left as a trivial placeholder. Researchers establishing spectral properties of T_J in Recognition Science cite this when assembling the full regularity implications. It is realized as a structure definition that composes the two antecedent sub-conjectures directly.
Claim. Let $T_J$ be the cost operator on the negative Hilbert space with prime weights $lamP : Nat.Primes → ℝ$. Then $e^{-t T_J}$ is trace-class for all $t > 0$ whenever $T_J$ is essentially self-adjoint on the dense domain of finite-support states (under square-summable weights) and possesses compact resolvent (under polynomial weight decay and linear cost growth).
background
The module formalizes operator-theoretic foundations for the cost operator $T_J$ derived from the J-functional. It introduces the dense domain of finite-support multiplicative states, establishes symmetry on that domain, and encodes three regularity sub-conjectures as hypothesis structures with precise assumptions on the prime weights. EssentialSelfAdjointness requires square-summability of weights together with the existence of a self-adjoint extension. CompactResolvent assumes polynomial decay of weights and linear growth of the cost potential, asserting compactness of the resolvent. TraceClassHeatKernel combines these to guarantee trace-class membership of the semigroup.
proof idea
The declaration is a structure definition. Its first field imports EssentialSelfAdjointness lamP, its second imports CompactResolvent lamP, and its third field is the constant True serving as placeholder for the trace-class statement.
why it matters
This structure supplies the final member of the regularity trio and is invoked by the regularity_chain theorem, which produces TraceClassHeatKernel from the self-adjointness and compact-resolvent hypotheses. It supports the cost_operator_regularity_certificate that collects the structural facts for T_J. In the framework it closes the analytic requirements needed to treat T_J as a spectral object with discrete spectrum, consistent with spectral emergence and the phi-forcing derivation of the cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.