pith. sign in
module module high

IndisputableMonolith.NumberTheory.CostOperatorRegularity

show as:
view Lean formalization →

The CostOperatorRegularity module defines the dense domain of finitely supported states for the cost operator and derives its regularity properties in support of the Hilbert-Pólya candidate. It records that the full state space already serves as this dense subspace and chains bounds on the cost potential with weight summability to reach essential self-adjointness and trace-class heat kernel. Researchers examining operator candidates for the Riemann zeros would cite these domain and spectral facts. The module structure is a sequence of domain, b

claimLet StateSpace be the space of finitely supported functions MultIndex →₀ ℝ. The dense domain D coincides with StateSpace. The cost potential satisfies linear growth, weights are square-summable with polynomial decay, and the operator is essentially self-adjoint with compact resolvent and trace-class heat kernel.

background

The module sits inside the Recognition Science treatment of the Hilbert-Pólya conjecture. StateSpace is defined as the type of finitely supported real functions on multiset indices, so the entire space is already dense in itself for the cost operator. The Cost module supplies the underlying recognition-cost functional whose potential and weight properties are bounded here. The HilbertPolyaCandidate module supplies the algebraic skeleton of the candidate self-adjoint operator whose domain and regularity are now made precise.

proof idea

This is a definition module with supporting lemmas. It begins by declaring the dense domain as the full StateSpace, proves non-emptiness and membership, then establishes CostPotentialBound and CostPotentialLinearGrowth, followed by WeightSquareSummable and WeightDecayPolynomial. These feed weight_polynomial_decay_summable, which in turn yields EssentialSelfAdjointness, CompactResolvent, and TraceClassHeatKernel, closing the regularity_chain.

why it matters in Recognition Science

The module supplies the operator-theoretic regularity required by the Hilbert-Pólya candidate so that its spectrum can be compared with the imaginary parts of the zeta zeros. It closes the gap between the abstract cost functional and a concrete self-adjoint operator with compact resolvent, a prerequisite for any eigenvalue interpretation inside the Recognition framework.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (13)