IndisputableMonolith.NumberTheory.CostOperatorRegularity
The module defines the dense domain of finitely supported states for the cost operator on the Hilbert-Pólya candidate space and assembles regularity lemmas including potential bounds, weight decay, essential self-adjointness, compact resolvent, and trace-class heat kernel. Researchers modeling the Riemann hypothesis via Recognition Science cost operators would cite these results to justify spectral analysis on the algebraic skeleton. The module proceeds by direct definitions of the domain followed by a chain of elementary lemmas on summability,
claim$D = StateSpace = (MultIndex →₀ ℝ)$ is the dense subspace of finitely supported states. The cost operator on $D$ satisfies CostPotentialBound, WeightSquareSummable, EssentialSelfAdjointness, CompactResolvent, TraceClassHeatKernel, and the assembled regularity_chain.
background
The module sits inside the Recognition Science treatment of the Hilbert-Pólya conjecture. It imports the Cost module for the underlying cost functional and the HilbertPolyaCandidate module, whose doc-comment states that it constructs the algebraic skeleton of a candidate operator whose eigenvalues would realize the imaginary parts of the non-trivial zeta zeros. StateSpace is defined as MultIndex →₀ ℝ, which already encodes finite support, so the dense domain D coincides with the full space. The sibling declarations introduce CostPotentialBound (linear growth control), WeightDecayPolynomial, EssentialSelfAdjointness, CompactResolvent, and TraceClassHeatKernel as the concrete regularity statements needed for the operator.
proof idea
This is a definition module whose core is the identification of denseDomain with the full StateSpace. The remaining declarations are one-line wrappers or direct constructions: denseDomain_nonempty and denseDomain_mem are immediate from the finite-support definition; CostPotentialBound, CostPotentialLinearGrowth, WeightSquareSummable, weight_polynomial_decay_summable, EssentialSelfAdjointness, CompactResolvent, and TraceClassHeatKernel are stated as separate lemmas; regularity_chain collects them into a single composite statement.
why it matters in Recognition Science
The module supplies the regularity infrastructure required by the Hilbert-Pólya candidate constructed in the upstream HilbertPolyaCandidate module. It ensures the cost operator meets the analytic conditions (essential self-adjointness, compact resolvent, trace-class heat kernel) that allow the algebraic skeleton to be treated as a candidate self-adjoint operator on a Hilbert space. No downstream uses are recorded, but the regularity_chain closes the technical prerequisites for spectral analysis within the Recognition framework.
scope and limits
- Does not prove existence of the full Hilbert-Pólya operator beyond the algebraic skeleton.
- Does not compute or bound any eigenvalues of the candidate operator.
- Does not address convergence of the heat kernel outside the trace-class regime.
- Does not import or invoke analytic continuation or explicit formulas from classical number theory.
depends on (2)
declarations in this module (13)
-
def
denseDomain -
theorem
denseDomain_nonempty -
theorem
denseDomain_mem -
structure
CostPotentialBound -
def
CostPotentialLinearGrowth -
def
WeightSquareSummable -
def
WeightDecayPolynomial -
theorem
weight_polynomial_decay_summable -
structure
EssentialSelfAdjointness -
structure
CompactResolvent -
structure
TraceClassHeatKernel -
theorem
regularity_chain -
theorem
cost_operator_regularity_certificate