IndisputableMonolith.NumberTheory.CostOperatorRegularity
CostOperatorRegularity supplies the dense domain and auxiliary regularity results for the cost operator inside the Recognition-Cost candidate for the Hilbert-Pólya operator. Number theorists and mathematical physicists pursuing an operator realization of the Riemann zeros would cite the domain and summability lemmas. The module consists entirely of definitions and short lemmas that record the finite-support structure already present in StateSpace.
claimLet \(D\subseteq\mathcal{S}\) where \(\mathcal{S}=\mathrm{MultIndex}\to_0\mathbb{R}\) is the state space of finitely supported real functions on the multi-index set. Then \(D=\mathcal{S}\) is dense in itself and serves as the domain for the cost operator.
background
The module sits in the NumberTheory domain and imports the Cost module together with the Hilbert-Pólya candidate. The latter builds the algebraic skeleton of a candidate self-adjoint operator whose spectrum is conjectured to reproduce the imaginary parts of the non-trivial zeros of the Riemann zeta function. The supplied doc-comment states that StateSpace already encodes finite support, so the full space itself functions as the dense subspace required for operator-theoretic arguments.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The constructions feed the regularity_chain and supply the dense domain needed for EssentialSelfAdjointness, CompactResolvent and TraceClassHeatKernel inside the Hilbert-Pólya candidate. They therefore advance the Recognition Science program of realizing number-theoretic objects via the cost operator on a finitely supported state space.
scope and limits
- Does not prove the Riemann hypothesis.
- Does not exhibit explicit eigenvalues of the candidate operator.
- Does not connect the cost operator to the forcing chain T0-T8.
- Does not derive the constants c, ħ or G from this construction.
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