EssentialSelfAdjointness
plain-language theorem explainer
The structure EssentialSelfAdjointness records the hypothesis that the cost operator T_J is essentially self-adjoint on the dense domain of finite-support states when prime weights are square-summable. Spectral theorists investigating the cost operator as a candidate for the Hilbert-Polya operator would reference this sub-conjecture C.1. It is implemented as a structure definition that asserts the WeightSquareSummable condition and defers the extension property to a trivial placeholder.
Claim. Let weights $lambda_p : Nat.Primes to R$ satisfy $sum_p lambda_p^2 < infty$. The cost operator $T_J$ is essentially self-adjoint on the dense domain $D$ of finite-support multiplicative states.
background
The module develops operator-theoretic regularity for the cost operator $T_J$ derived from the Recognition Composition Law. The dense domain consists of finite-support states on multiplicative indices. WeightSquareSummable requires that the sum of squared prime weights is finite, serving as the operator-level bandwidth constraint. Upstream, the shifted cost satisfies $H(xy) + H(x/y) = 2 H(x) H(y)$ with $H(x) = J(x) + 1 = 1/2(x + x^{-1})$, as defined in CostAlgebra.
proof idea
The declaration is a structure definition with two fields: the summability condition WeightSquareSummable and a placeholder proposition for the self-adjoint extension.
why it matters
This sub-conjecture C.1 initiates the regularity chain that couples essential self-adjointness, compact resolvent, and trace-class heat kernel. It supports the construction of $T_J$ as a spectral object in Recognition Science, building on J-uniqueness from the forcing chain. The analytic content awaits discharge, as noted in the module's hypothesis structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.