denseDomain
plain-language theorem explainer
The declaration defines the dense domain for the cost operator as the entire pre-Hilbert space StateSpace of finitely supported real functions on multiplicative indices. Researchers formalizing spectral properties of the J-cost operator or Hilbert-Polya candidates would cite it to fix the domain before symmetry or extension arguments. The definition is a direct one-line assignment to the full set, using the finite-support encoding already present in StateSpace.
Claim. Let StateSpace denote the pre-Hilbert space of finitely supported functions from multiplicative indices to real numbers. The dense domain is the full set StateSpace.
background
The module sets up operator-theoretic regularity for the candidate cost operator T_J on the pre-Hilbert space. StateSpace is the free real module on MultIndex, written MultIndex →₀ ℝ, so every element already has finite support. The dense domain is introduced as the subspace on which symmetry and semi-boundedness will be checked before the three analytic sub-conjectures (essential self-adjointness, compact resolvent, trace-class heat kernel) are stated as hypothesis structures.
proof idea
One-line definition that directly equates denseDomain to Set.univ on the type StateSpace.
why it matters
It supplies the domain fact used by the regularity certificate theorem, which records that every state lies in the dense domain together with the weight summability implication. This structural fact is required before the hypothesis structures for essential self-adjointness and discrete spectrum can be formulated; it closes the zero-sorry part of the operator foundations in the Recognition Science cost-operator analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.