denseDomain
plain-language theorem explainer
The dense domain for the cost operator is defined as the entire state space of finitely supported real functions on multiplicative indices. Spectral theorists working on the Hilbert-Polya candidate or regularity of the J-cost operator would cite this fact to anchor the domain of T_J. The definition is a direct abbreviation that uses the built-in finite support of the StateSpace type.
Claim. Let $D$ be the dense domain of the cost operator on the pre-Hilbert space $H$ of finitely supported functions $f : M →_0 ℝ$, where $M$ denotes the multiplicative indices. Then $D := H$.
background
The module constructs the operator-theoretic setting for the candidate cost operator $T_J$ on the state space of the Hilbert-Polya approach. StateSpace is the free ℝ-module on MultIndex, equivalently the space of finitely supported real-valued functions on multiplicative indices. The dense domain is introduced to serve as the common domain for symmetry and semi-boundedness statements before the analytic conjectures on essential self-adjointness and compact resolvent are stated as hypothesis structures.
proof idea
One-line definition that sets denseDomain equal to the universal set on StateSpace, exploiting that every element of StateSpace already has finite support by construction of the Finsupp type.
why it matters
This definition supplies the first structural fact in the regularity certificate theorem, which records that the dense domain coincides with the full state space and that polynomial weight decay implies square-summability. It feeds directly into denseDomain_mem, denseDomain_nonempty, and the overall cost_operator_regularity_certificate. In the Recognition framework it clears the way for the spectral analysis of the J-cost operator that underpins the phi-ladder mass formula and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.