regularity_chain
plain-language theorem explainer
regularity_chain asserts that essential self-adjointness of the cost operator together with compact resolvent imply the heat kernel is trace-class. Researchers formalizing the spectral theory of T_J in Recognition Science cite this to couple the three regularity sub-conjectures. The proof is a direct term-mode construction that assembles the target structure from the two input hypotheses and a trivial witness.
Claim. If EssentialSelfAdjointness($λ_p$) and CompactResolvent($λ_p$) hold for weights $λ_p$ on the primes, then TraceClassHeatKernel($λ_p$) holds, so that $e^{-t T_J}$ is trace-class on $ℋ_-$ for all $t>0$.
background
The module formalizes operator foundations for the cost operator $T_J$ tied to the J-functional, constructing the dense domain of finite-support states and stating three sub-conjectures as hypothesis structures. EssentialSelfAdjointness (C.1) requires WeightSquareSummable weights and posits essential self-adjointness on denseDomain. CompactResolvent (C.2) requires polynomial weight decay plus CostPotentialLinearGrowth and posits compact resolvent. TraceClassHeatKernel (C.3) requires the prior two and posits trace-class heat kernel. Upstream results include the definition of Nat.Primes and the structures for C.1 and C.2, quoted as 'Sub-conjecture C.1: essential self-adjointness of the cost operator on the dense domain denseDomain, given the bandwidth constraint.'
proof idea
The proof is a one-line term-mode wrapper that constructs the TraceClassHeatKernel structure by pairing the EssentialSelfAdjointness hypothesis into the selfadjoint field, the CompactResolvent hypothesis into the resolvent field, and trivial for the trace_class_holds field.
why it matters
This theorem closes the implication chain among the regularity sub-conjectures and feeds directly into the downstream cost_operator_regularity_certificate that collects the module's structural facts. It fills the step showing C.1 plus C.2 imply C.3 in the operator foundations for T_J. Within Recognition Science it supports the spectral requirements for the phi-ladder and eight-tick octave; the analytic discharge of the True placeholders in each structure remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.