cost_operator_regularity_certificate
plain-language theorem explainer
The declaration certifies three structural facts for the cost operator: its dense domain fills the state space, polynomial decay of prime weights yields square-summability, and the regularity sub-conjectures chain from essential self-adjointness through compact resolvent to trace-class heat kernel. Researchers formalizing spectral properties of the J-cost operator would reference this to lock down the domain and implication structure. The proof packages three sibling lemmas in a single term-mode conjunction.
Claim. The dense domain of the cost operator coincides with the full state space; for any prime-weight function $λ_p$ and $ε ≥ 0$, the polynomial decay condition $λ_p = O(p^{-(1+ε)})$ implies $∑_p λ_p² < ∞$; and for any such $λ_p$, the essential self-adjointness hypothesis implies the compact resolvent hypothesis which implies the trace-class heat kernel hypothesis.
background
The module CostOperatorRegularity develops the operator foundations for the cost operator $T_J$ associated to the J-cost functional. It defines the dense domain of finite-support multiplicative-index states and introduces three hypothesis structures that stand in for analytic regularity conjectures on the prime weights $λ_p$ (module documentation). WeightSquareSummable asserts that the sum of squared weights over primes is finite, the operator-level analog of the RS bandwidth constraint. WeightDecayPolynomial requires the stronger polynomial decay $λ_p ≤ C / p^{1+ε}$ for some $ε > 0$ (referenced definitions).
proof idea
The proof is a term-mode construction that directly assembles the conjunction from three sibling results: denseDomain_mem for the domain claim, weight_polynomial_decay_summable for the decay-to-summability implication, and regularity_chain for the sub-conjecture implication chain.
why it matters
This theorem compiles the zero-sorry structural facts of the module, providing the foundation for the hypothesis structures on the cost operator $T_J$. It supports the operator-theoretic setup needed to treat $T_J$ as a spectral object, prior to addressing the analytic sub-conjectures C.1–C.3 (module documentation). The result closes the structural portion of the regularity chain before any analytic discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.